MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpmapenlem Structured version   Unicode version

Theorem xpmapenlem 7277
Description: Lemma for xpmapen 7278. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
Hypotheses
Ref Expression
xpmapen.1  |-  A  e. 
_V
xpmapen.2  |-  B  e. 
_V
xpmapen.3  |-  C  e. 
_V
xpmapenlem.4  |-  D  =  ( z  e.  C  |->  ( 1st `  (
x `  z )
) )
xpmapenlem.5  |-  R  =  ( z  e.  C  |->  ( 2nd `  (
x `  z )
) )
xpmapenlem.6  |-  S  =  ( z  e.  C  |-> 
<. ( ( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >. )
Assertion
Ref Expression
xpmapenlem  |-  ( ( A  X.  B )  ^m  C )  ~~  ( ( A  ^m  C )  X.  ( B  ^m  C ) )
Distinct variable groups:    x, y,
z, A    x, B, y, z    x, C, y, z    y, D, z   
y, R, z    x, S, z
Allowed substitution hints:    D( x)    R( x)    S( y)

Proof of Theorem xpmapenlem
StepHypRef Expression
1 ovex 6109 . 2  |-  ( ( A  X.  B )  ^m  C )  e. 
_V
2 ovex 6109 . . 3  |-  ( A  ^m  C )  e. 
_V
3 ovex 6109 . . 3  |-  ( B  ^m  C )  e. 
_V
42, 3xpex 4993 . 2  |-  ( ( A  ^m  C )  X.  ( B  ^m  C ) )  e. 
_V
5 xpmapen.1 . . . . . . . . 9  |-  A  e. 
_V
6 xpmapen.2 . . . . . . . . 9  |-  B  e. 
_V
75, 6xpex 4993 . . . . . . . 8  |-  ( A  X.  B )  e. 
_V
8 xpmapen.3 . . . . . . . 8  |-  C  e. 
_V
97, 8elmap 7045 . . . . . . 7  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  <->  x : C
--> ( A  X.  B
) )
10 ffvelrn 5871 . . . . . . 7  |-  ( ( x : C --> ( A  X.  B )  /\  z  e.  C )  ->  ( x `  z
)  e.  ( A  X.  B ) )
119, 10sylanb 460 . . . . . 6  |-  ( ( x  e.  ( ( A  X.  B )  ^m  C )  /\  z  e.  C )  ->  ( x `  z
)  e.  ( A  X.  B ) )
12 xp1st 6379 . . . . . 6  |-  ( ( x `  z )  e.  ( A  X.  B )  ->  ( 1st `  ( x `  z ) )  e.  A )
1311, 12syl 16 . . . . 5  |-  ( ( x  e.  ( ( A  X.  B )  ^m  C )  /\  z  e.  C )  ->  ( 1st `  (
x `  z )
)  e.  A )
14 xpmapenlem.4 . . . . 5  |-  D  =  ( z  e.  C  |->  ( 1st `  (
x `  z )
) )
1513, 14fmptd 5896 . . . 4  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  D : C --> A )
165, 8elmap 7045 . . . 4  |-  ( D  e.  ( A  ^m  C )  <->  D : C
--> A )
1715, 16sylibr 205 . . 3  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  D  e.  ( A  ^m  C
) )
18 xp2nd 6380 . . . . . 6  |-  ( ( x `  z )  e.  ( A  X.  B )  ->  ( 2nd `  ( x `  z ) )  e.  B )
1911, 18syl 16 . . . . 5  |-  ( ( x  e.  ( ( A  X.  B )  ^m  C )  /\  z  e.  C )  ->  ( 2nd `  (
x `  z )
)  e.  B )
20 xpmapenlem.5 . . . . 5  |-  R  =  ( z  e.  C  |->  ( 2nd `  (
x `  z )
) )
2119, 20fmptd 5896 . . . 4  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  R : C --> B )
226, 8elmap 7045 . . . 4  |-  ( R  e.  ( B  ^m  C )  <->  R : C
--> B )
2321, 22sylibr 205 . . 3  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  R  e.  ( B  ^m  C
) )
24 opelxpi 4913 . . 3  |-  ( ( D  e.  ( A  ^m  C )  /\  R  e.  ( B  ^m  C ) )  ->  <. D ,  R >.  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )
2517, 23, 24syl2anc 644 . 2  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  <. D ,  R >.  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )
26 xp1st 6379 . . . . . . 7  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 1st `  y )  e.  ( A  ^m  C
) )
275, 8elmap 7045 . . . . . . 7  |-  ( ( 1st `  y )  e.  ( A  ^m  C )  <->  ( 1st `  y ) : C --> A )
2826, 27sylib 190 . . . . . 6  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 1st `  y ) : C --> A )
2928ffvelrnda 5873 . . . . 5  |-  ( ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) )  /\  z  e.  C )  ->  ( ( 1st `  y
) `  z )  e.  A )
30 xp2nd 6380 . . . . . . 7  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 2nd `  y )  e.  ( B  ^m  C
) )
316, 8elmap 7045 . . . . . . 7  |-  ( ( 2nd `  y )  e.  ( B  ^m  C )  <->  ( 2nd `  y ) : C --> B )
3230, 31sylib 190 . . . . . 6  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 2nd `  y ) : C --> B )
3332ffvelrnda 5873 . . . . 5  |-  ( ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) )  /\  z  e.  C )  ->  ( ( 2nd `  y
) `  z )  e.  B )
34 opelxpi 4913 . . . . 5  |-  ( ( ( ( 1st `  y
) `  z )  e.  A  /\  (
( 2nd `  y
) `  z )  e.  B )  ->  <. (
( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >.  e.  ( A  X.  B ) )
3529, 33, 34syl2anc 644 . . . 4  |-  ( ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) )  /\  z  e.  C )  -> 
<. ( ( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >.  e.  ( A  X.  B ) )
36 xpmapenlem.6 . . . 4  |-  S  =  ( z  e.  C  |-> 
<. ( ( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >. )
3735, 36fmptd 5896 . . 3  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  S : C --> ( A  X.  B ) )
387, 8elmap 7045 . . 3  |-  ( S  e.  ( ( A  X.  B )  ^m  C )  <->  S : C
--> ( A  X.  B
) )
3937, 38sylibr 205 . 2  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  S  e.  ( ( A  X.  B )  ^m  C
) )
40 1st2nd2 6389 . . . . 5  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  y  =  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
4140ad2antlr 709 . . . 4  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  y  =  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
4228feqmptd 5782 . . . . . . 7  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 1st `  y )  =  ( z  e.  C  |->  ( ( 1st `  y
) `  z )
) )
4342ad2antlr 709 . . . . . 6  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  ( 1st `  y )  =  ( z  e.  C  |->  ( ( 1st `  y
) `  z )
) )
44 simplr 733 . . . . . . . . . . . 12  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  x  =  S )  /\  z  e.  C )  ->  x  =  S )
4544fveq1d 5733 . . . . . . . . . . 11  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  x  =  S )  /\  z  e.  C )  ->  (
x `  z )  =  ( S `  z ) )
46 opex 4430 . . . . . . . . . . . . 13  |-  <. (
( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >.  e.  _V
4736fvmpt2 5815 . . . . . . . . . . . . 13  |-  ( ( z  e.  C  /\  <.
( ( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >.  e.  _V )  ->  ( S `  z
)  =  <. (
( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >. )
4846, 47mpan2 654 . . . . . . . . . . . 12  |-  ( z  e.  C  ->  ( S `  z )  =  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)
4948adantl 454 . . . . . . . . . . 11  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  x  =  S )  /\  z  e.  C )  ->  ( S `  z )  =  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)
5045, 49eqtrd 2470 . . . . . . . . . 10  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  x  =  S )  /\  z  e.  C )  ->  (
x `  z )  =  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)
5150fveq2d 5735 . . . . . . . . 9  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  x  =  S )  /\  z  e.  C )  ->  ( 1st `  ( x `  z ) )  =  ( 1st `  <. ( ( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >. ) )
52 fvex 5745 . . . . . . . . . 10  |-  ( ( 1st `  y ) `
 z )  e. 
_V
53 fvex 5745 . . . . . . . . . 10  |-  ( ( 2nd `  y ) `
 z )  e. 
_V
5452, 53op1st 6358 . . . . . . . . 9  |-  ( 1st `  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)  =  ( ( 1st `  y ) `
 z )
5551, 54syl6eq 2486 . . . . . . . 8  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  x  =  S )  /\  z  e.  C )  ->  ( 1st `  ( x `  z ) )  =  ( ( 1st `  y
) `  z )
)
5655mpteq2dva 4298 . . . . . . 7  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  (
z  e.  C  |->  ( 1st `  ( x `
 z ) ) )  =  ( z  e.  C  |->  ( ( 1st `  y ) `
 z ) ) )
5714, 56syl5eq 2482 . . . . . 6  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  D  =  ( z  e.  C  |->  ( ( 1st `  y ) `  z
) ) )
5843, 57eqtr4d 2473 . . . . 5  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  ( 1st `  y )  =  D )
5932feqmptd 5782 . . . . . . 7  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 2nd `  y )  =  ( z  e.  C  |->  ( ( 2nd `  y
) `  z )
) )
6059ad2antlr 709 . . . . . 6  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  ( 2nd `  y )  =  ( z  e.  C  |->  ( ( 2nd `  y
) `  z )
) )
6150fveq2d 5735 . . . . . . . . 9  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  x  =  S )  /\  z  e.  C )  ->  ( 2nd `  ( x `  z ) )  =  ( 2nd `  <. ( ( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >. ) )
6252, 53op2nd 6359 . . . . . . . . 9  |-  ( 2nd `  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)  =  ( ( 2nd `  y ) `
 z )
6361, 62syl6eq 2486 . . . . . . . 8  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  x  =  S )  /\  z  e.  C )  ->  ( 2nd `  ( x `  z ) )  =  ( ( 2nd `  y
) `  z )
)
6463mpteq2dva 4298 . . . . . . 7  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  (
z  e.  C  |->  ( 2nd `  ( x `
 z ) ) )  =  ( z  e.  C  |->  ( ( 2nd `  y ) `
 z ) ) )
6520, 64syl5eq 2482 . . . . . 6  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  R  =  ( z  e.  C  |->  ( ( 2nd `  y ) `  z
) ) )
6660, 65eqtr4d 2473 . . . . 5  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  ( 2nd `  y )  =  R )
6758, 66opeq12d 3994 . . . 4  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  <. ( 1st `  y ) ,  ( 2nd `  y
) >.  =  <. D ,  R >. )
6841, 67eqtrd 2470 . . 3  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  y  =  <. D ,  R >. )
69 simpll 732 . . . . . 6  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  x  e.  ( ( A  X.  B
)  ^m  C )
)
7069, 9sylib 190 . . . . 5  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  x : C --> ( A  X.  B
) )
7170feqmptd 5782 . . . 4  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  x  =  ( z  e.  C  |->  ( x `  z ) ) )
72 simpr 449 . . . . . . . . . . . 12  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  y  =  <. D ,  R >. )
7372fveq2d 5735 . . . . . . . . . . 11  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( 1st `  y
)  =  ( 1st `  <. D ,  R >. ) )
7417ad2antrr 708 . . . . . . . . . . . 12  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  D  e.  ( A  ^m  C ) )
7523ad2antrr 708 . . . . . . . . . . . 12  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  R  e.  ( B  ^m  C ) )
76 op1stg 6362 . . . . . . . . . . . 12  |-  ( ( D  e.  ( A  ^m  C )  /\  R  e.  ( B  ^m  C ) )  -> 
( 1st `  <. D ,  R >. )  =  D )
7774, 75, 76syl2anc 644 . . . . . . . . . . 11  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( 1st `  <. D ,  R >. )  =  D )
7873, 77eqtrd 2470 . . . . . . . . . 10  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( 1st `  y
)  =  D )
7978fveq1d 5733 . . . . . . . . 9  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( ( 1st `  y ) `  z
)  =  ( D `
 z ) )
80 fvex 5745 . . . . . . . . . 10  |-  ( 1st `  ( x `  z
) )  e.  _V
8114fvmpt2 5815 . . . . . . . . . 10  |-  ( ( z  e.  C  /\  ( 1st `  ( x `
 z ) )  e.  _V )  -> 
( D `  z
)  =  ( 1st `  ( x `  z
) ) )
8280, 81mpan2 654 . . . . . . . . 9  |-  ( z  e.  C  ->  ( D `  z )  =  ( 1st `  (
x `  z )
) )
8379, 82sylan9eq 2490 . . . . . . . 8  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  /\  z  e.  C
)  ->  ( ( 1st `  y ) `  z )  =  ( 1st `  ( x `
 z ) ) )
8472fveq2d 5735 . . . . . . . . . . 11  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( 2nd `  y
)  =  ( 2nd `  <. D ,  R >. ) )
85 op2ndg 6363 . . . . . . . . . . . 12  |-  ( ( D  e.  ( A  ^m  C )  /\  R  e.  ( B  ^m  C ) )  -> 
( 2nd `  <. D ,  R >. )  =  R )
8674, 75, 85syl2anc 644 . . . . . . . . . . 11  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( 2nd `  <. D ,  R >. )  =  R )
8784, 86eqtrd 2470 . . . . . . . . . 10  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( 2nd `  y
)  =  R )
8887fveq1d 5733 . . . . . . . . 9  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( ( 2nd `  y ) `  z
)  =  ( R `
 z ) )
89 fvex 5745 . . . . . . . . . 10  |-  ( 2nd `  ( x `  z
) )  e.  _V
9020fvmpt2 5815 . . . . . . . . . 10  |-  ( ( z  e.  C  /\  ( 2nd `  ( x `
 z ) )  e.  _V )  -> 
( R `  z
)  =  ( 2nd `  ( x `  z
) ) )
9189, 90mpan2 654 . . . . . . . . 9  |-  ( z  e.  C  ->  ( R `  z )  =  ( 2nd `  (
x `  z )
) )
9288, 91sylan9eq 2490 . . . . . . . 8  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  /\  z  e.  C
)  ->  ( ( 2nd `  y ) `  z )  =  ( 2nd `  ( x `
 z ) ) )
9383, 92opeq12d 3994 . . . . . . 7  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  /\  z  e.  C
)  ->  <. ( ( 1st `  y ) `
 z ) ,  ( ( 2nd `  y
) `  z ) >.  =  <. ( 1st `  (
x `  z )
) ,  ( 2nd `  ( x `  z
) ) >. )
9470ffvelrnda 5873 . . . . . . . 8  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  /\  z  e.  C
)  ->  ( x `  z )  e.  ( A  X.  B ) )
95 1st2nd2 6389 . . . . . . . 8  |-  ( ( x `  z )  e.  ( A  X.  B )  ->  (
x `  z )  =  <. ( 1st `  (
x `  z )
) ,  ( 2nd `  ( x `  z
) ) >. )
9694, 95syl 16 . . . . . . 7  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  /\  z  e.  C
)  ->  ( x `  z )  =  <. ( 1st `  ( x `
 z ) ) ,  ( 2nd `  (
x `  z )
) >. )
9793, 96eqtr4d 2473 . . . . . 6  |-  ( ( ( ( x  e.  ( ( A  X.  B )  ^m  C
)  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  /\  z  e.  C
)  ->  <. ( ( 1st `  y ) `
 z ) ,  ( ( 2nd `  y
) `  z ) >.  =  ( x `  z ) )
9897mpteq2dva 4298 . . . . 5  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( z  e.  C  |->  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)  =  ( z  e.  C  |->  ( x `
 z ) ) )
9936, 98syl5eq 2482 . . . 4  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  S  =  ( z  e.  C  |->  ( x `  z ) ) )
10071, 99eqtr4d 2473 . . 3  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  x  =  S )
10168, 100impbida 807 . 2  |-  ( ( x  e.  ( ( A  X.  B )  ^m  C )  /\  y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) ) )  -> 
( x  =  S  <-> 
y  =  <. D ,  R >. ) )
1021, 4, 25, 39, 101en3i 7149 1  |-  ( ( A  X.  B )  ^m  C )  ~~  ( ( A  ^m  C )  X.  ( B  ^m  C ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1653    e. wcel 1726   _Vcvv 2958   <.cop 3819   class class class wbr 4215    e. cmpt 4269    X. cxp 4879   -->wf 5453   ` cfv 5457  (class class class)co 6084   1stc1st 6350   2ndc2nd 6351    ^m cmap 7021    ~~ cen 7109
This theorem is referenced by:  xpmapen  7278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-map 7023  df-en 7113
  Copyright terms: Public domain W3C validator