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