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 ) ) )