Metamath Proof Explorer

Theorem lsmhash

Description: The order of the direct product of groups. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses lsmhash.p 
|- .(+) = ( LSSum ` G )
lsmhash.o 
|- .0. = ( 0g ` G )
lsmhash.z 
|- Z = ( Cntz ` G )
lsmhash.t 
|- ( ph -> T e. ( SubGrp ` G ) )
lsmhash.u 
|- ( ph -> U e. ( SubGrp ` G ) )
lsmhash.i 
|- ( ph -> ( T i^i U ) = { .0. } )
lsmhash.s 
|- ( ph -> T C_ ( Z ` U ) )
lsmhash.1 
|- ( ph -> T e. Fin )
lsmhash.2 
|- ( ph -> U e. Fin )
Assertion lsmhash 
|- ( ph -> ( # ` ( T .(+) U ) ) = ( ( # ` T ) x. ( # ` U ) ) )

Proof

Step Hyp Ref Expression
1 lsmhash.p 
 |-  .(+) = ( LSSum ` G )
2 lsmhash.o 
 |-  .0. = ( 0g ` G )
3 lsmhash.z 
 |-  Z = ( Cntz ` G )
4 lsmhash.t 
 |-  ( ph -> T e. ( SubGrp ` G ) )
5 lsmhash.u 
 |-  ( ph -> U e. ( SubGrp ` G ) )
6 lsmhash.i 
 |-  ( ph -> ( T i^i U ) = { .0. } )
7 lsmhash.s 
 |-  ( ph -> T C_ ( Z ` U ) )
8 lsmhash.1 
 |-  ( ph -> T e. Fin )
9 lsmhash.2 
 |-  ( ph -> U e. Fin )
10 ovexd 
 |-  ( ph -> ( T .(+) U ) e. _V )
11 eqid 
 |-  ( x e. ( T .(+) U ) |-> <. ( ( T ( proj1 ` G ) U ) ` x ) , ( ( U ( proj1 ` G ) T ) ` x ) >. ) = ( x e. ( T .(+) U ) |-> <. ( ( T ( proj1 ` G ) U ) ` x ) , ( ( U ( proj1 ` G ) T ) ` x ) >. )
12 eqid 
 |-  ( +g ` G ) = ( +g ` G )
13 eqid 
 |-  ( proj1 ` G ) = ( proj1 ` G )
14 12 1 2 3 4 5 6 7 13 pj1f 
 |-  ( ph -> ( T ( proj1 ` G ) U ) : ( T .(+) U ) --> T )
15 14 ffvelrnda 
 |-  ( ( ph /\ x e. ( T .(+) U ) ) -> ( ( T ( proj1 ` G ) U ) ` x ) e. T )
16 12 1 2 3 4 5 6 7 13 pj2f 
 |-  ( ph -> ( U ( proj1 ` G ) T ) : ( T .(+) U ) --> U )
17 16 ffvelrnda 
 |-  ( ( ph /\ x e. ( T .(+) U ) ) -> ( ( U ( proj1 ` G ) T ) ` x ) e. U )
18 15 17 opelxpd 
 |-  ( ( ph /\ x e. ( T .(+) U ) ) -> <. ( ( T ( proj1 ` G ) U ) ` x ) , ( ( U ( proj1 ` G ) T ) ` x ) >. e. ( T X. U ) )
19 4 5 jca 
 |-  ( ph -> ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) )
20 xp1st 
 |-  ( y e. ( T X. U ) -> ( 1st ` y ) e. T )
21 xp2nd 
 |-  ( y e. ( T X. U ) -> ( 2nd ` y ) e. U )
22 20 21 jca 
 |-  ( y e. ( T X. U ) -> ( ( 1st ` y ) e. T /\ ( 2nd ` y ) e. U ) )
23 12 1 lsmelvali 
 |-  ( ( ( T e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) /\ ( ( 1st ` y ) e. T /\ ( 2nd ` y ) e. U ) ) -> ( ( 1st ` y ) ( +g ` G ) ( 2nd ` y ) ) e. ( T .(+) U ) )
24 19 22 23 syl2an 
 |-  ( ( ph /\ y e. ( T X. U ) ) -> ( ( 1st ` y ) ( +g ` G ) ( 2nd ` y ) ) e. ( T .(+) U ) )
25 4 adantr 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> T e. ( SubGrp ` G ) )
26 5 adantr 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> U e. ( SubGrp ` G ) )
27 6 adantr 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> ( T i^i U ) = { .0. } )
28 7 adantr 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> T C_ ( Z ` U ) )
29 simprl 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> x e. ( T .(+) U ) )
30 20 ad2antll 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> ( 1st ` y ) e. T )
31 21 ad2antll 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> ( 2nd ` y ) e. U )
32 12 1 2 3 25 26 27 28 13 29 30 31 pj1eq 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> ( x = ( ( 1st ` y ) ( +g ` G ) ( 2nd ` y ) ) <-> ( ( ( T ( proj1 ` G ) U ) ` x ) = ( 1st ` y ) /\ ( ( U ( proj1 ` G ) T ) ` x ) = ( 2nd ` y ) ) ) )
33 eqcom 
 |-  ( ( ( T ( proj1 ` G ) U ) ` x ) = ( 1st ` y ) <-> ( 1st ` y ) = ( ( T ( proj1 ` G ) U ) ` x ) )
34 eqcom 
 |-  ( ( ( U ( proj1 ` G ) T ) ` x ) = ( 2nd ` y ) <-> ( 2nd ` y ) = ( ( U ( proj1 ` G ) T ) ` x ) )
35 33 34 anbi12i 
 |-  ( ( ( ( T ( proj1 ` G ) U ) ` x ) = ( 1st ` y ) /\ ( ( U ( proj1 ` G ) T ) ` x ) = ( 2nd ` y ) ) <-> ( ( 1st ` y ) = ( ( T ( proj1 ` G ) U ) ` x ) /\ ( 2nd ` y ) = ( ( U ( proj1 ` G ) T ) ` x ) ) )
36 32 35 bitrdi 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> ( x = ( ( 1st ` y ) ( +g ` G ) ( 2nd ` y ) ) <-> ( ( 1st ` y ) = ( ( T ( proj1 ` G ) U ) ` x ) /\ ( 2nd ` y ) = ( ( U ( proj1 ` G ) T ) ` x ) ) ) )
37 eqop 
 |-  ( y e. ( T X. U ) -> ( y = <. ( ( T ( proj1 ` G ) U ) ` x ) , ( ( U ( proj1 ` G ) T ) ` x ) >. <-> ( ( 1st ` y ) = ( ( T ( proj1 ` G ) U ) ` x ) /\ ( 2nd ` y ) = ( ( U ( proj1 ` G ) T ) ` x ) ) ) )
38 37 ad2antll 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> ( y = <. ( ( T ( proj1 ` G ) U ) ` x ) , ( ( U ( proj1 ` G ) T ) ` x ) >. <-> ( ( 1st ` y ) = ( ( T ( proj1 ` G ) U ) ` x ) /\ ( 2nd ` y ) = ( ( U ( proj1 ` G ) T ) ` x ) ) ) )
39 36 38 bitr4d 
 |-  ( ( ph /\ ( x e. ( T .(+) U ) /\ y e. ( T X. U ) ) ) -> ( x = ( ( 1st ` y ) ( +g ` G ) ( 2nd ` y ) ) <-> y = <. ( ( T ( proj1 ` G ) U ) ` x ) , ( ( U ( proj1 ` G ) T ) ` x ) >. ) )
40 11 18 24 39 f1o2d 
 |-  ( ph -> ( x e. ( T .(+) U ) |-> <. ( ( T ( proj1 ` G ) U ) ` x ) , ( ( U ( proj1 ` G ) T ) ` x ) >. ) : ( T .(+) U ) -1-1-onto-> ( T X. U ) )
41 10 40 hasheqf1od 
 |-  ( ph -> ( # ` ( T .(+) U ) ) = ( # ` ( T X. U ) ) )
42 hashxp 
 |-  ( ( T e. Fin /\ U e. Fin ) -> ( # ` ( T X. U ) ) = ( ( # ` T ) x. ( # ` U ) ) )
43 8 9 42 syl2anc 
 |-  ( ph -> ( # ` ( T X. U ) ) = ( ( # ` T ) x. ( # ` U ) ) )
44 41 43 eqtrd 
 |-  ( ph -> ( # ` ( T .(+) U ) ) = ( ( # ` T ) x. ( # ` U ) ) )