Metamath Proof Explorer

Theorem mulgpropd

Description: Two structures with the same group-nature have the same group multiple function. K is expected to either be _V (when strong equality is available) or B (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mulgpropd.m 
|- .x. = ( .g ` G )
mulgpropd.n 
|- .X. = ( .g ` H )
mulgpropd.b1 
|- ( ph -> B = ( Base ` G ) )
mulgpropd.b2 
|- ( ph -> B = ( Base ` H ) )
mulgpropd.i 
|- ( ph -> B C_ K )
mulgpropd.k 
|- ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` G ) y ) e. K )
mulgpropd.e 
|- ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
Assertion mulgpropd 
|- ( ph -> .x. = .X. )

Proof

Step Hyp Ref Expression
1 mulgpropd.m 
 |-  .x. = ( .g ` G )
2 mulgpropd.n 
 |-  .X. = ( .g ` H )
3 mulgpropd.b1 
 |-  ( ph -> B = ( Base ` G ) )
4 mulgpropd.b2 
 |-  ( ph -> B = ( Base ` H ) )
5 mulgpropd.i 
 |-  ( ph -> B C_ K )
6 mulgpropd.k 
 |-  ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` G ) y ) e. K )
7 mulgpropd.e 
 |-  ( ( ph /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
8 ssel 
 |-  ( B C_ K -> ( x e. B -> x e. K ) )
9 ssel 
 |-  ( B C_ K -> ( y e. B -> y e. K ) )
10 8 9 anim12d 
 |-  ( B C_ K -> ( ( x e. B /\ y e. B ) -> ( x e. K /\ y e. K ) ) )
11 5 10 syl 
 |-  ( ph -> ( ( x e. B /\ y e. B ) -> ( x e. K /\ y e. K ) ) )
12 11 imp 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x e. K /\ y e. K ) )
13 12 7 syldan 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
14 3 4 13 grpidpropd 
 |-  ( ph -> ( 0g ` G ) = ( 0g ` H ) )
15 14 3ad2ant1 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> ( 0g ` G ) = ( 0g ` H ) )
16 1zzd 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> 1 e. ZZ )
17 vex 
 |-  b e. _V
18 17 fvconst2 
 |-  ( x e. NN -> ( ( NN X. { b } ) ` x ) = b )
19 nnuz 
 |-  NN = ( ZZ>= ` 1 )
20 19 eqcomi 
 |-  ( ZZ>= ` 1 ) = NN
21 18 20 eleq2s 
 |-  ( x e. ( ZZ>= ` 1 ) -> ( ( NN X. { b } ) ` x ) = b )
22 21 adantl 
 |-  ( ( ( ph /\ a e. ZZ /\ b e. B ) /\ x e. ( ZZ>= ` 1 ) ) -> ( ( NN X. { b } ) ` x ) = b )
23 5 3ad2ant1 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> B C_ K )
24 simp3 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> b e. B )
25 23 24 sseldd 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> b e. K )
26 25 adantr 
 |-  ( ( ( ph /\ a e. ZZ /\ b e. B ) /\ x e. ( ZZ>= ` 1 ) ) -> b e. K )
27 22 26 eqeltrd 
 |-  ( ( ( ph /\ a e. ZZ /\ b e. B ) /\ x e. ( ZZ>= ` 1 ) ) -> ( ( NN X. { b } ) ` x ) e. K )
28 6 3ad2antl1 
 |-  ( ( ( ph /\ a e. ZZ /\ b e. B ) /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` G ) y ) e. K )
29 7 3ad2antl1 
 |-  ( ( ( ph /\ a e. ZZ /\ b e. B ) /\ ( x e. K /\ y e. K ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` H ) y ) )
30 16 27 28 29 seqfeq3 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) = seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) )
31 30 fveq1d 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) = ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) )
32 3 4 13 grpinvpropd 
 |-  ( ph -> ( invg ` G ) = ( invg ` H ) )
33 32 3ad2ant1 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> ( invg ` G ) = ( invg ` H ) )
34 30 fveq1d 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) = ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) )
35 33 34 fveq12d 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) = ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) )
36 31 35 ifeq12d 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) = if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) )
37 15 36 ifeq12d 
 |-  ( ( ph /\ a e. ZZ /\ b e. B ) -> if ( a = 0 , ( 0g ` G ) , if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) ) = if ( a = 0 , ( 0g ` H ) , if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) ) )
38 37 mpoeq3dva 
 |-  ( ph -> ( a e. ZZ , b e. B |-> if ( a = 0 , ( 0g ` G ) , if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) ) ) = ( a e. ZZ , b e. B |-> if ( a = 0 , ( 0g ` H ) , if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) ) ) )
39 eqidd 
 |-  ( ph -> ZZ = ZZ )
40 eqidd 
 |-  ( ph -> if ( a = 0 , ( 0g ` G ) , if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) ) = if ( a = 0 , ( 0g ` G ) , if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) ) )
41 39 3 40 mpoeq123dv 
 |-  ( ph -> ( a e. ZZ , b e. B |-> if ( a = 0 , ( 0g ` G ) , if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) ) ) = ( a e. ZZ , b e. ( Base ` G ) |-> if ( a = 0 , ( 0g ` G ) , if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) ) ) )
42 eqidd 
 |-  ( ph -> if ( a = 0 , ( 0g ` H ) , if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) ) = if ( a = 0 , ( 0g ` H ) , if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) ) )
43 39 4 42 mpoeq123dv 
 |-  ( ph -> ( a e. ZZ , b e. B |-> if ( a = 0 , ( 0g ` H ) , if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) ) ) = ( a e. ZZ , b e. ( Base ` H ) |-> if ( a = 0 , ( 0g ` H ) , if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) ) ) )
44 38 41 43 3eqtr3d 
 |-  ( ph -> ( a e. ZZ , b e. ( Base ` G ) |-> if ( a = 0 , ( 0g ` G ) , if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) ) ) = ( a e. ZZ , b e. ( Base ` H ) |-> if ( a = 0 , ( 0g ` H ) , if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) ) ) )
45 eqid 
 |-  ( Base ` G ) = ( Base ` G )
46 eqid 
 |-  ( +g ` G ) = ( +g ` G )
47 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
48 eqid 
 |-  ( invg ` G ) = ( invg ` G )
49 45 46 47 48 1 mulgfval 
 |-  .x. = ( a e. ZZ , b e. ( Base ` G ) |-> if ( a = 0 , ( 0g ` G ) , if ( 0 < a , ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` G ) ` ( seq 1 ( ( +g ` G ) , ( NN X. { b } ) ) ` -u a ) ) ) ) )
50 eqid 
 |-  ( Base ` H ) = ( Base ` H )
51 eqid 
 |-  ( +g ` H ) = ( +g ` H )
52 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
53 eqid 
 |-  ( invg ` H ) = ( invg ` H )
54 50 51 52 53 2 mulgfval 
 |-  .X. = ( a e. ZZ , b e. ( Base ` H ) |-> if ( a = 0 , ( 0g ` H ) , if ( 0 < a , ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` a ) , ( ( invg ` H ) ` ( seq 1 ( ( +g ` H ) , ( NN X. { b } ) ) ` -u a ) ) ) ) )
55 44 49 54 3eqtr4g 
 |-  ( ph -> .x. = .X. )