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

Theorem xpmapenlem 7483
Description: Lemma for xpmapen 7484. (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 6121 . 2  |-  ( ( A  X.  B )  ^m  C )  e. 
_V
2 ovex 6121 . . 3  |-  ( A  ^m  C )  e. 
_V
3 ovex 6121 . . 3  |-  ( B  ^m  C )  e. 
_V
42, 3xpex 6513 . 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 6513 . . . . . . . 8  |-  ( A  X.  B )  e. 
_V
8 xpmapen.3 . . . . . . . 8  |-  C  e. 
_V
97, 8elmap 7246 . . . . . . 7  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  <->  x : C
--> ( A  X.  B
) )
10 ffvelrn 5846 . . . . . . 7  |-  ( ( x : C --> ( A  X.  B )  /\  z  e.  C )  ->  ( x `  z
)  e.  ( A  X.  B ) )
119, 10sylanb 472 . . . . . 6  |-  ( ( x  e.  ( ( A  X.  B )  ^m  C )  /\  z  e.  C )  ->  ( x `  z
)  e.  ( A  X.  B ) )
12 xp1st 6611 . . . . . 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 5872 . . . 4  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  D : C --> A )
165, 8elmap 7246 . . . 4  |-  ( D  e.  ( A  ^m  C )  <->  D : C
--> A )
1715, 16sylibr 212 . . 3  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  D  e.  ( A  ^m  C
) )
18 xp2nd 6612 . . . . . 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 5872 . . . 4  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  R : C --> B )
226, 8elmap 7246 . . . 4  |-  ( R  e.  ( B  ^m  C )  <->  R : C
--> B )
2321, 22sylibr 212 . . 3  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  R  e.  ( B  ^m  C
) )
24 opelxpi 4876 . . 3  |-  ( ( D  e.  ( A  ^m  C )  /\  R  e.  ( B  ^m  C ) )  ->  <. D ,  R >.  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )
2517, 23, 24syl2anc 661 . 2  |-  ( x  e.  ( ( A  X.  B )  ^m  C )  ->  <. D ,  R >.  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) ) )
26 xp1st 6611 . . . . . . 7  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 1st `  y )  e.  ( A  ^m  C
) )
275, 8elmap 7246 . . . . . . 7  |-  ( ( 1st `  y )  e.  ( A  ^m  C )  <->  ( 1st `  y ) : C --> A )
2826, 27sylib 196 . . . . . 6  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 1st `  y ) : C --> A )
2928ffvelrnda 5848 . . . . 5  |-  ( ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) )  /\  z  e.  C )  ->  ( ( 1st `  y
) `  z )  e.  A )
30 xp2nd 6612 . . . . . . 7  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 2nd `  y )  e.  ( B  ^m  C
) )
316, 8elmap 7246 . . . . . . 7  |-  ( ( 2nd `  y )  e.  ( B  ^m  C )  <->  ( 2nd `  y ) : C --> B )
3230, 31sylib 196 . . . . . 6  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 2nd `  y ) : C --> B )
3332ffvelrnda 5848 . . . . 5  |-  ( ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C ) )  /\  z  e.  C )  ->  ( ( 2nd `  y
) `  z )  e.  B )
34 opelxpi 4876 . . . . 5  |-  ( ( ( ( 1st `  y
) `  z )  e.  A  /\  (
( 2nd `  y
) `  z )  e.  B )  ->  <. (
( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >.  e.  ( A  X.  B ) )
3529, 33, 34syl2anc 661 . . . 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 5872 . . 3  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  S : C --> ( A  X.  B ) )
387, 8elmap 7246 . . 3  |-  ( S  e.  ( ( A  X.  B )  ^m  C )  <->  S : C
--> ( A  X.  B
) )
3937, 38sylibr 212 . 2  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  S  e.  ( ( A  X.  B )  ^m  C
) )
40 1st2nd2 6618 . . . . 5  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  y  =  <. ( 1st `  y
) ,  ( 2nd `  y ) >. )
4140ad2antlr 726 . . . 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 5749 . . . . . . 7  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 1st `  y )  =  ( z  e.  C  |->  ( ( 1st `  y
) `  z )
) )
4342ad2antlr 726 . . . . . 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 754 . . . . . . . . . . . 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 5698 . . . . . . . . . . 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 4561 . . . . . . . . . . . . 13  |-  <. (
( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >.  e.  _V
4736fvmpt2 5786 . . . . . . . . . . . . 13  |-  ( ( z  e.  C  /\  <.
( ( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >.  e.  _V )  ->  ( S `  z
)  =  <. (
( 1st `  y
) `  z ) ,  ( ( 2nd `  y ) `  z
) >. )
4846, 47mpan2 671 . . . . . . . . . . . 12  |-  ( z  e.  C  ->  ( S `  z )  =  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)
4948adantl 466 . . . . . . . . . . 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 2475 . . . . . . . . . 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 5700 . . . . . . . . 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 5706 . . . . . . . . . 10  |-  ( ( 1st `  y ) `
 z )  e. 
_V
53 fvex 5706 . . . . . . . . . 10  |-  ( ( 2nd `  y ) `
 z )  e. 
_V
5452, 53op1st 6590 . . . . . . . . 9  |-  ( 1st `  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)  =  ( ( 1st `  y ) `
 z )
5551, 54syl6eq 2491 . . . . . . . 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 4383 . . . . . . 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 2487 . . . . . 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 2478 . . . . 5  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  ( 1st `  y )  =  D )
5932feqmptd 5749 . . . . . . 7  |-  ( y  e.  ( ( A  ^m  C )  X.  ( B  ^m  C
) )  ->  ( 2nd `  y )  =  ( z  e.  C  |->  ( ( 2nd `  y
) `  z )
) )
6059ad2antlr 726 . . . . . 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 5700 . . . . . . . . 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 6591 . . . . . . . . 9  |-  ( 2nd `  <. ( ( 1st `  y ) `  z
) ,  ( ( 2nd `  y ) `
 z ) >.
)  =  ( ( 2nd `  y ) `
 z )
6361, 62syl6eq 2491 . . . . . . . 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 4383 . . . . . . 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 2487 . . . . . 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 2478 . . . . 5  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  ( 2nd `  y )  =  R )
6758, 66opeq12d 4072 . . . 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 2475 . . 3  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  x  =  S )  ->  y  =  <. D ,  R >. )
69 simpll 753 . . . . . 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 196 . . . . 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 5749 . . . 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 461 . . . . . . . . . . . 12  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  y  =  <. D ,  R >. )
7372fveq2d 5700 . . . . . . . . . . 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 725 . . . . . . . . . . . 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 725 . . . . . . . . . . . 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 6594 . . . . . . . . . . . 12  |-  ( ( D  e.  ( A  ^m  C )  /\  R  e.  ( B  ^m  C ) )  -> 
( 1st `  <. D ,  R >. )  =  D )
7774, 75, 76syl2anc 661 . . . . . . . . . . 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 2475 . . . . . . . . . 10  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( 1st `  y
)  =  D )
7978fveq1d 5698 . . . . . . . . 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 5706 . . . . . . . . . 10  |-  ( 1st `  ( x `  z
) )  e.  _V
8114fvmpt2 5786 . . . . . . . . . 10  |-  ( ( z  e.  C  /\  ( 1st `  ( x `
 z ) )  e.  _V )  -> 
( D `  z
)  =  ( 1st `  ( x `  z
) ) )
8280, 81mpan2 671 . . . . . . . . 9  |-  ( z  e.  C  ->  ( D `  z )  =  ( 1st `  (
x `  z )
) )
8379, 82sylan9eq 2495 . . . . . . . 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 5700 . . . . . . . . . . 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 6595 . . . . . . . . . . . 12  |-  ( ( D  e.  ( A  ^m  C )  /\  R  e.  ( B  ^m  C ) )  -> 
( 2nd `  <. D ,  R >. )  =  R )
8674, 75, 85syl2anc 661 . . . . . . . . . . 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 2475 . . . . . . . . . 10  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  ( 2nd `  y
)  =  R )
8887fveq1d 5698 . . . . . . . . 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 5706 . . . . . . . . . 10  |-  ( 2nd `  ( x `  z
) )  e.  _V
9020fvmpt2 5786 . . . . . . . . . 10  |-  ( ( z  e.  C  /\  ( 2nd `  ( x `
 z ) )  e.  _V )  -> 
( R `  z
)  =  ( 2nd `  ( x `  z
) ) )
9189, 90mpan2 671 . . . . . . . . 9  |-  ( z  e.  C  ->  ( R `  z )  =  ( 2nd `  (
x `  z )
) )
9288, 91sylan9eq 2495 . . . . . . . 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 4072 . . . . . . 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 5848 . . . . . . . 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 6618 . . . . . . . 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 2478 . . . . . 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 4383 . . . . 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 2487 . . . 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 2478 . . 3  |-  ( ( ( x  e.  ( ( A  X.  B
)  ^m  C )  /\  y  e.  (
( A  ^m  C
)  X.  ( B  ^m  C ) ) )  /\  y  = 
<. D ,  R >. )  ->  x  =  S )
10168, 100impbida 828 . 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 7353 1  |-  ( ( A  X.  B )  ^m  C )  ~~  ( ( A  ^m  C )  X.  ( B  ^m  C ) )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369    e. wcel 1756   _Vcvv 2977   <.cop 3888   class class class wbr 4297    e. cmpt 4355    X. cxp 4843   -->wf 5419   ` cfv 5423  (class class class)co 6096   1stc1st 6580   2ndc2nd 6581    ^m cmap 7219    ~~ cen 7312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-1st 6582  df-2nd 6583  df-map 7221  df-en 7316
This theorem is referenced by:  xpmapen  7484
  Copyright terms: Public domain W3C validator