Metamath Proof Explorer

Theorem ablfacrp

Description: A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups K , L that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of Shapiro, p. 199. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses ablfacrp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfacrp.o ⊢ 𝑂 = ( od ‘ 𝐺 )
ablfacrp.k ⊢ 𝐾 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 }
ablfacrp.l ⊢ 𝐿 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 }
ablfacrp.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfacrp.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
ablfacrp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ablfacrp.1 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
ablfacrp.2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) )
ablfacrp.z ⊢ 0 = ( 0g ‘ 𝐺 )
ablfacrp.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion ablfacrp ( 𝜑 → ( ( 𝐾 ∩ 𝐿 ) = { 0 } ∧ ( 𝐾 ⊕ 𝐿 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ablfacrp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablfacrp.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 ablfacrp.k ⊢ 𝐾 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 }
4 ablfacrp.l ⊢ 𝐿 = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 }
5 ablfacrp.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
6 ablfacrp.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 ablfacrp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8 ablfacrp.1 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
9 ablfacrp.2 ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) )
10 ablfacrp.z ⊢ 0 = ( 0g ‘ 𝐺 )
11 ablfacrp.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
12 3 4 ineq12i ⊢ ( 𝐾 ∩ 𝐿 ) = ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 } ∩ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } )
13 inrab ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 } ∩ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ) = { 𝑥 ∈ 𝐵 ∣ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) }
14 12 13 eqtri ⊢ ( 𝐾 ∩ 𝐿 ) = { 𝑥 ∈ 𝐵 ∣ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) }
15 1 2 odcl ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
17 16 nn0zd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 ‘ 𝑥 ) ∈ ℤ )
18 6 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑀 ∈ ℤ )
20 7 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ℤ )
22 dvdsgcd ⊢ ( ( ( 𝑂 ‘ 𝑥 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) → ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑀 gcd 𝑁 ) ) )
23 17 19 21 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) → ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑀 gcd 𝑁 ) ) )
24 23 3impia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑀 gcd 𝑁 ) )
25 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
26 24 25 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ 𝑥 ) ∥ 1 )
27 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → 𝑥 ∈ 𝐵 )
28 dvds1 ⊢ ( ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 → ( ( 𝑂 ‘ 𝑥 ) ∥ 1 ↔ ( 𝑂 ‘ 𝑥 ) = 1 ) )
29 27 15 28 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 1 ↔ ( 𝑂 ‘ 𝑥 ) = 1 ) )
30 26 29 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → ( 𝑂 ‘ 𝑥 ) = 1 )
31 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
32 5 31 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
33 32 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → 𝐺 ∈ Grp )
34 2 10 1 odeq1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑂 ‘ 𝑥 ) = 1 ↔ 𝑥 = 0 ) )
35 33 27 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → ( ( 𝑂 ‘ 𝑥 ) = 1 ↔ 𝑥 = 0 ) )
36 30 35 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → 𝑥 = 0 )
37 velsn ⊢ ( 𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
38 36 37 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) ) → 𝑥 ∈ { 0 } )
39 38 rabssdv ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ∧ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) } ⊆ { 0 } )
40 14 39 eqsstrid ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐿 ) ⊆ { 0 } )
41 2 1 oddvdssubg ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 } ∈ ( SubGrp ‘ 𝐺 ) )
42 5 18 41 syl2anc ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 } ∈ ( SubGrp ‘ 𝐺 ) )
43 3 42 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
44 10 subg0cl ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝐾 )
45 43 44 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
46 2 1 oddvdssubg ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ ( SubGrp ‘ 𝐺 ) )
47 5 20 46 syl2anc ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 } ∈ ( SubGrp ‘ 𝐺 ) )
48 4 47 eqeltrid ⊢ ( 𝜑 → 𝐿 ∈ ( SubGrp ‘ 𝐺 ) )
49 10 subg0cl ⊢ ( 𝐿 ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ 𝐿 )
50 48 49 syl ⊢ ( 𝜑 → 0 ∈ 𝐿 )
51 45 50 elind ⊢ ( 𝜑 → 0 ∈ ( 𝐾 ∩ 𝐿 ) )
52 51 snssd ⊢ ( 𝜑 → { 0 } ⊆ ( 𝐾 ∩ 𝐿 ) )
53 40 52 eqssd ⊢ ( 𝜑 → ( 𝐾 ∩ 𝐿 ) = { 0 } )
54 11 lsmsubg2 ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐿 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐾 ⊕ 𝐿 ) ∈ ( SubGrp ‘ 𝐺 ) )
55 5 43 48 54 syl3anc ⊢ ( 𝜑 → ( 𝐾 ⊕ 𝐿 ) ∈ ( SubGrp ‘ 𝐺 ) )
56 1 subgss ⊢ ( ( 𝐾 ⊕ 𝐿 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐾 ⊕ 𝐿 ) ⊆ 𝐵 )
57 55 56 syl ⊢ ( 𝜑 → ( 𝐾 ⊕ 𝐿 ) ⊆ 𝐵 )
58 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
59 1 58 mulg1 ⊢ ( 𝑔 ∈ 𝐵 → ( 1 ( .g ‘ 𝐺 ) 𝑔 ) = 𝑔 )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( 1 ( .g ‘ 𝐺 ) 𝑔 ) = 𝑔 )
61 bezout ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) )
62 18 20 61 syl2anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) )
64 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
65 64 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) ↔ 1 = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) ) )
66 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
67 simprl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
68 66 67 zmulcld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑀 · 𝑎 ) ∈ ℤ )
69 68 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑀 · 𝑎 ) ∈ ℂ )
70 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
71 simprr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
72 70 71 zmulcld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑁 · 𝑏 ) ∈ ℤ )
73 72 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑁 · 𝑏 ) ∈ ℂ )
74 69 73 addcomd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) = ( ( 𝑁 · 𝑏 ) + ( 𝑀 · 𝑎 ) ) )
75 74 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) ( .g ‘ 𝐺 ) 𝑔 ) = ( ( ( 𝑁 · 𝑏 ) + ( 𝑀 · 𝑎 ) ) ( .g ‘ 𝐺 ) 𝑔 ) )
76 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐺 ∈ Grp )
77 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑔 ∈ 𝐵 )
78 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
79 1 58 78 mulgdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑁 · 𝑏 ) ∈ ℤ ∧ ( 𝑀 · 𝑎 ) ∈ ℤ ∧ 𝑔 ∈ 𝐵 ) ) → ( ( ( 𝑁 · 𝑏 ) + ( 𝑀 · 𝑎 ) ) ( .g ‘ 𝐺 ) 𝑔 ) = ( ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ( +g ‘ 𝐺 ) ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) )
80 76 72 68 77 79 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑁 · 𝑏 ) + ( 𝑀 · 𝑎 ) ) ( .g ‘ 𝐺 ) 𝑔 ) = ( ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ( +g ‘ 𝐺 ) ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) )
81 75 80 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) ( .g ‘ 𝐺 ) 𝑔 ) = ( ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ( +g ‘ 𝐺 ) ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) )
82 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
83 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐿 ∈ ( SubGrp ‘ 𝐺 ) )
84 1 58 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑁 · 𝑏 ) ∈ ℤ ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐵 )
85 76 72 77 84 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐵 )
86 1 2 odcl ⊢ ( 𝑔 ∈ 𝐵 → ( 𝑂 ‘ 𝑔 ) ∈ ℕ0 )
87 86 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ 𝑔 ) ∈ ℕ0 )
88 87 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ 𝑔 ) ∈ ℤ )
89 66 70 zmulcld ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
90 6 7 nnmulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℕ )
91 90 nnnn0d ⊢ ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℕ0 )
92 9 91 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
93 1 fvexi ⊢ 𝐵 ∈ V
94 hashclb ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) )
95 93 94 ax-mp ⊢ ( 𝐵 ∈ Fin ↔ ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
96 92 95 sylibr ⊢ ( 𝜑 → 𝐵 ∈ Fin )
97 96 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐵 ∈ Fin )
98 1 2 oddvds2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑔 ∈ 𝐵 ) → ( 𝑂 ‘ 𝑔 ) ∥ ( ♯ ‘ 𝐵 ) )
99 76 97 77 98 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ 𝑔 ) ∥ ( ♯ ‘ 𝐵 ) )
100 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ♯ ‘ 𝐵 ) = ( 𝑀 · 𝑁 ) )
101 99 100 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ 𝑔 ) ∥ ( 𝑀 · 𝑁 ) )
102 88 89 71 101 dvdsmultr1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ 𝑔 ) ∥ ( ( 𝑀 · 𝑁 ) · 𝑏 ) )
103 66 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑀 ∈ ℂ )
104 70 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑁 ∈ ℂ )
105 71 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
106 103 104 105 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑀 · 𝑁 ) · 𝑏 ) = ( 𝑀 · ( 𝑁 · 𝑏 ) ) )
107 102 106 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ 𝑔 ) ∥ ( 𝑀 · ( 𝑁 · 𝑏 ) ) )
108 1 2 58 odmulgid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ ( 𝑁 · 𝑏 ) ∈ ℤ ) ∧ 𝑀 ∈ ℤ ) → ( ( 𝑂 ‘ ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑀 ↔ ( 𝑂 ‘ 𝑔 ) ∥ ( 𝑀 · ( 𝑁 · 𝑏 ) ) ) )
109 76 77 72 66 108 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑂 ‘ ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑀 ↔ ( 𝑂 ‘ 𝑔 ) ∥ ( 𝑀 · ( 𝑁 · 𝑏 ) ) ) )
110 107 109 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑀 )
111 fveq2 ⊢ ( 𝑥 = ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ) )
112 111 breq1d ⊢ ( 𝑥 = ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑀 ↔ ( 𝑂 ‘ ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑀 ) )
113 112 3 elrab2 ⊢ ( ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐾 ↔ ( ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐵 ∧ ( 𝑂 ‘ ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑀 ) )
114 85 110 113 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐾 )
115 1 58 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑀 · 𝑎 ) ∈ ℤ ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐵 )
116 76 68 77 115 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐵 )
117 88 89 67 101 dvdsmultr1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ 𝑔 ) ∥ ( ( 𝑀 · 𝑁 ) · 𝑎 ) )
118 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
119 118 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
120 mulass ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( ( 𝑀 · 𝑁 ) · 𝑎 ) = ( 𝑀 · ( 𝑁 · 𝑎 ) ) )
121 mul12 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 𝑀 · ( 𝑁 · 𝑎 ) ) = ( 𝑁 · ( 𝑀 · 𝑎 ) ) )
122 120 121 eqtrd ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( ( 𝑀 · 𝑁 ) · 𝑎 ) = ( 𝑁 · ( 𝑀 · 𝑎 ) ) )
123 103 104 119 122 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑀 · 𝑁 ) · 𝑎 ) = ( 𝑁 · ( 𝑀 · 𝑎 ) ) )
124 117 123 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ 𝑔 ) ∥ ( 𝑁 · ( 𝑀 · 𝑎 ) ) )
125 1 2 58 odmulgid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ ( 𝑀 · 𝑎 ) ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑁 ↔ ( 𝑂 ‘ 𝑔 ) ∥ ( 𝑁 · ( 𝑀 · 𝑎 ) ) ) )
126 76 77 68 70 125 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑂 ‘ ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑁 ↔ ( 𝑂 ‘ 𝑔 ) ∥ ( 𝑁 · ( 𝑀 · 𝑎 ) ) ) )
127 124 126 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑂 ‘ ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑁 )
128 fveq2 ⊢ ( 𝑥 = ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) )
129 128 breq1d ⊢ ( 𝑥 = ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑂 ‘ ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑁 ) )
130 129 4 elrab2 ⊢ ( ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐿 ↔ ( ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐵 ∧ ( 𝑂 ‘ ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∥ 𝑁 ) )
131 116 127 130 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐿 )
132 78 11 lsmelvali ⊢ ( ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐿 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐾 ∧ ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ 𝐿 ) ) → ( ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ( +g ‘ 𝐺 ) ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∈ ( 𝐾 ⊕ 𝐿 ) )
133 82 83 114 131 132 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑁 · 𝑏 ) ( .g ‘ 𝐺 ) 𝑔 ) ( +g ‘ 𝐺 ) ( ( 𝑀 · 𝑎 ) ( .g ‘ 𝐺 ) 𝑔 ) ) ∈ ( 𝐾 ⊕ 𝐿 ) )
134 81 133 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ ( 𝐾 ⊕ 𝐿 ) )
135 oveq1 ⊢ ( 1 = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) → ( 1 ( .g ‘ 𝐺 ) 𝑔 ) = ( ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) ( .g ‘ 𝐺 ) 𝑔 ) )
136 135 eleq1d ⊢ ( 1 = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) → ( ( 1 ( .g ‘ 𝐺 ) 𝑔 ) ∈ ( 𝐾 ⊕ 𝐿 ) ↔ ( ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) ( .g ‘ 𝐺 ) 𝑔 ) ∈ ( 𝐾 ⊕ 𝐿 ) ) )
137 134 136 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 1 = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) → ( 1 ( .g ‘ 𝐺 ) 𝑔 ) ∈ ( 𝐾 ⊕ 𝐿 ) ) )
138 65 137 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) → ( 1 ( .g ‘ 𝐺 ) 𝑔 ) ∈ ( 𝐾 ⊕ 𝐿 ) ) )
139 138 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑎 ) + ( 𝑁 · 𝑏 ) ) → ( 1 ( .g ‘ 𝐺 ) 𝑔 ) ∈ ( 𝐾 ⊕ 𝐿 ) ) )
140 63 139 mpd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( 1 ( .g ‘ 𝐺 ) 𝑔 ) ∈ ( 𝐾 ⊕ 𝐿 ) )
141 60 140 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( 𝐾 ⊕ 𝐿 ) )
142 57 141 eqelssd ⊢ ( 𝜑 → ( 𝐾 ⊕ 𝐿 ) = 𝐵 )
143 53 142 jca ⊢ ( 𝜑 → ( ( 𝐾 ∩ 𝐿 ) = { 0 } ∧ ( 𝐾 ⊕ 𝐿 ) = 𝐵 ) )