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 ‘ 𝐺 )
lsmhash.o 0 = ( 0g𝐺 )
lsmhash.z 𝑍 = ( Cntz ‘ 𝐺 )
lsmhash.t ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
lsmhash.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
lsmhash.i ( 𝜑 → ( 𝑇𝑈 ) = { 0 } )
lsmhash.s ( 𝜑𝑇 ⊆ ( 𝑍𝑈 ) )
lsmhash.1 ( 𝜑𝑇 ∈ Fin )
lsmhash.2 ( 𝜑𝑈 ∈ Fin )
Assertion lsmhash ( 𝜑 → ( ♯ ‘ ( 𝑇 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) · ( ♯ ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lsmhash.p = ( LSSum ‘ 𝐺 )
2 lsmhash.o 0 = ( 0g𝐺 )
3 lsmhash.z 𝑍 = ( Cntz ‘ 𝐺 )
4 lsmhash.t ( 𝜑𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
5 lsmhash.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
6 lsmhash.i ( 𝜑 → ( 𝑇𝑈 ) = { 0 } )
7 lsmhash.s ( 𝜑𝑇 ⊆ ( 𝑍𝑈 ) )
8 lsmhash.1 ( 𝜑𝑇 ∈ Fin )
9 lsmhash.2 ( 𝜑𝑈 ∈ Fin )
10 ovexd ( 𝜑 → ( 𝑇 𝑈 ) ∈ V )
11 eqid ( 𝑥 ∈ ( 𝑇 𝑈 ) ↦ ⟨ ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ ( 𝑇 𝑈 ) ↦ ⟨ ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ )
12 eqid ( +g𝐺 ) = ( +g𝐺 )
13 eqid ( proj1𝐺 ) = ( proj1𝐺 )
14 12 1 2 3 4 5 6 7 13 pj1f ( 𝜑 → ( 𝑇 ( proj1𝐺 ) 𝑈 ) : ( 𝑇 𝑈 ) ⟶ 𝑇 )
15 14 ffvelrnda ( ( 𝜑𝑥 ∈ ( 𝑇 𝑈 ) ) → ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) ∈ 𝑇 )
16 12 1 2 3 4 5 6 7 13 pj2f ( 𝜑 → ( 𝑈 ( proj1𝐺 ) 𝑇 ) : ( 𝑇 𝑈 ) ⟶ 𝑈 )
17 16 ffvelrnda ( ( 𝜑𝑥 ∈ ( 𝑇 𝑈 ) ) → ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ∈ 𝑈 )
18 15 17 opelxpd ( ( 𝜑𝑥 ∈ ( 𝑇 𝑈 ) ) → ⟨ ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ∈ ( 𝑇 × 𝑈 ) )
19 4 5 jca ( 𝜑 → ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) )
20 xp1st ( 𝑦 ∈ ( 𝑇 × 𝑈 ) → ( 1st𝑦 ) ∈ 𝑇 )
21 xp2nd ( 𝑦 ∈ ( 𝑇 × 𝑈 ) → ( 2nd𝑦 ) ∈ 𝑈 )
22 20 21 jca ( 𝑦 ∈ ( 𝑇 × 𝑈 ) → ( ( 1st𝑦 ) ∈ 𝑇 ∧ ( 2nd𝑦 ) ∈ 𝑈 ) )
23 12 1 lsmelvali ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 1st𝑦 ) ∈ 𝑇 ∧ ( 2nd𝑦 ) ∈ 𝑈 ) ) → ( ( 1st𝑦 ) ( +g𝐺 ) ( 2nd𝑦 ) ) ∈ ( 𝑇 𝑈 ) )
24 19 22 23 syl2an ( ( 𝜑𝑦 ∈ ( 𝑇 × 𝑈 ) ) → ( ( 1st𝑦 ) ( +g𝐺 ) ( 2nd𝑦 ) ) ∈ ( 𝑇 𝑈 ) )
25 4 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
26 5 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
27 6 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑇𝑈 ) = { 0 } )
28 7 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → 𝑇 ⊆ ( 𝑍𝑈 ) )
29 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → 𝑥 ∈ ( 𝑇 𝑈 ) )
30 20 ad2antll ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 1st𝑦 ) ∈ 𝑇 )
31 21 ad2antll ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 2nd𝑦 ) ∈ 𝑈 )
32 12 1 2 3 25 26 27 28 13 29 30 31 pj1eq ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑥 = ( ( 1st𝑦 ) ( +g𝐺 ) ( 2nd𝑦 ) ) ↔ ( ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) = ( 1st𝑦 ) ∧ ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) = ( 2nd𝑦 ) ) ) )
33 eqcom ( ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) = ( 1st𝑦 ) ↔ ( 1st𝑦 ) = ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) )
34 eqcom ( ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) = ( 2nd𝑦 ) ↔ ( 2nd𝑦 ) = ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) )
35 33 34 anbi12i ( ( ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) = ( 1st𝑦 ) ∧ ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) = ( 2nd𝑦 ) ) ↔ ( ( 1st𝑦 ) = ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) ∧ ( 2nd𝑦 ) = ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ) )
36 32 35 bitrdi ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑥 = ( ( 1st𝑦 ) ( +g𝐺 ) ( 2nd𝑦 ) ) ↔ ( ( 1st𝑦 ) = ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) ∧ ( 2nd𝑦 ) = ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ) ) )
37 eqop ( 𝑦 ∈ ( 𝑇 × 𝑈 ) → ( 𝑦 = ⟨ ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ↔ ( ( 1st𝑦 ) = ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) ∧ ( 2nd𝑦 ) = ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ) ) )
38 37 ad2antll ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑦 = ⟨ ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ↔ ( ( 1st𝑦 ) = ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) ∧ ( 2nd𝑦 ) = ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ) ) )
39 36 38 bitr4d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑥 = ( ( 1st𝑦 ) ( +g𝐺 ) ( 2nd𝑦 ) ) ↔ 𝑦 = ⟨ ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ) )
40 11 18 24 39 f1o2d ( 𝜑 → ( 𝑥 ∈ ( 𝑇 𝑈 ) ↦ ⟨ ( ( 𝑇 ( proj1𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj1𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ) : ( 𝑇 𝑈 ) –1-1-onto→ ( 𝑇 × 𝑈 ) )
41 10 40 hasheqf1od ( 𝜑 → ( ♯ ‘ ( 𝑇 𝑈 ) ) = ( ♯ ‘ ( 𝑇 × 𝑈 ) ) )
42 hashxp ( ( 𝑇 ∈ Fin ∧ 𝑈 ∈ Fin ) → ( ♯ ‘ ( 𝑇 × 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) · ( ♯ ‘ 𝑈 ) ) )
43 8 9 42 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝑇 × 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) · ( ♯ ‘ 𝑈 ) ) )
44 41 43 eqtrd ( 𝜑 → ( ♯ ‘ ( 𝑇 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) · ( ♯ ‘ 𝑈 ) ) )