Theorem ablfacrp 20037

Description: A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups 𝐾, 𝐿 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
ablfacrp	⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵))

Distinct variable groups:   𝑥,𝐵   𝑥,𝐺   𝑥,𝑂   𝑥,𝑀   𝑥,𝑁   𝜑,𝑥   𝑥, 0

Allowed substitution hints:   ⊕ (𝑥)   𝐾(𝑥)   𝐿(𝑥)

Proof of Theorem ablfacrp

Dummy variables 𝑎 𝑏 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ablfacrp.k	. . . . . 6 ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀}
2		ablfacrp.l	. . . . . 6 ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}
3	1, 2	ineq12i 4159	. . . . 5 ⊢ (𝐾 ∩ 𝐿) = ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁})
4		inrab 4257	. . . . 5 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
5	3, 4	eqtri 2760	. . . 4 ⊢ (𝐾 ∩ 𝐿) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
6		ablfacrp.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐺)
7		ablfacrp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (od‘𝐺)
8	6, 7	odcl 19505	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ0)
9	8	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ0)
10	9	nn0zd 12543	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
11		ablfacrp.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
12	11	nnzd 12544	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
13	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑀 ∈ ℤ)
14		ablfacrp.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
15	14	nnzd 12544	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
16	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ ℤ)
17		dvdsgcd 16507	. . . . . . . . . . 11 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
18	10, 13, 16, 17	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
19	18	3impia 1118	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁))
20		ablfacrp.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
21	20	3ad2ant1 1134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑀 gcd 𝑁) = 1)
22	19, 21	breqtrd 5112	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) ∥ 1)
23		simp2 1138	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ 𝐵)
24		dvds1 16282	. . . . . . . . 9 ⊢ ((𝑂‘𝑥) ∈ ℕ0 → ((𝑂‘𝑥) ∥ 1 ↔ (𝑂‘𝑥) = 1))
25	23, 8, 24	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) ∥ 1 ↔ (𝑂‘𝑥) = 1))
26	22, 25	mpbid 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) = 1)
27		ablfacrp.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ Abel)
28		ablgrp 19754	. . . . . . . . . 10 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
29	27, 28	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
30	29	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝐺 ∈ Grp)
31		ablfacrp.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐺)
32	7, 31, 6	odeq1 19529	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
33	30, 23, 32	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
34	26, 33	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 = 0 )
35		velsn 4584	. . . . . 6 ⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
36	34, 35	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ { 0 })
37	36	rabssdv 4015	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)} ⊆ { 0 })
38	5, 37	eqsstrid 3961	. . 3 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ { 0 })
39	7, 6	oddvdssubg 19824	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
40	27, 12, 39	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
41	1, 40	eqeltrid 2841	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
42	31	subg0cl 19104	. . . . . 6 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐾)
43	41, 42	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐾)
44	7, 6	oddvdssubg 19824	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
45	27, 15, 44	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
46	2, 45	eqeltrid 2841	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (SubGrp‘𝐺))
47	31	subg0cl 19104	. . . . . 6 ⊢ (𝐿 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐿)
48	46, 47	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐿)
49	43, 48	elind 4141	. . . 4 ⊢ (𝜑 → 0 ∈ (𝐾 ∩ 𝐿))
50	49	snssd 4753	. . 3 ⊢ (𝜑 → { 0 } ⊆ (𝐾 ∩ 𝐿))
51	38, 50	eqssd 3940	. 2 ⊢ (𝜑 → (𝐾 ∩ 𝐿) = { 0 })
52		ablfacrp.s	. . . . . 6 ⊢ ⊕ = (LSSum‘𝐺)
53	52	lsmsubg2 19828	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
54	27, 41, 46, 53	syl3anc 1374	. . . 4 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
55	6	subgss 19097	. . . 4 ⊢ ((𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺) → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
56	54, 55	syl 17	. . 3 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
57		eqid 2737	. . . . . 6 ⊢ (.g‘𝐺) = (.g‘𝐺)
58	6, 57	mulg1 19051	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → (1(.g‘𝐺)𝑔) = 𝑔)
59	58	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) = 𝑔)
60		bezout 16506	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
61	12, 15, 60	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
62	61	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
63	20	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 gcd 𝑁) = 1)
64	63	eqeq1d 2739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) ↔ 1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏))))
65	12	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℤ)
66		simprl 771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
67	65, 66	zmulcld 12633	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℤ)
68	67	zcnd 12628	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℂ)
69	15	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℤ)
70		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
71	69, 70	zmulcld 12633	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℤ)
72	71	zcnd 12628	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℂ)
73	68, 72	addcomd 11342	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎) + (𝑁 · 𝑏)) = ((𝑁 · 𝑏) + (𝑀 · 𝑎)))
74	73	oveq1d 7376	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔))
75	29	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐺 ∈ Grp)
76		simplr 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑔 ∈ 𝐵)
77		eqid 2737	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
78	6, 57, 77	mulgdir 19076	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ ((𝑁 · 𝑏) ∈ ℤ ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
79	75, 71, 67, 76, 78	syl13anc 1375	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
80	74, 79	eqtrd 2772	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
81	41	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐾 ∈ (SubGrp‘𝐺))
82	46	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐿 ∈ (SubGrp‘𝐺))
83	6, 57	mulgcl 19061	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑁 · 𝑏) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
84	75, 71, 76, 83	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
85	6, 7	odcl 19505	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝐵 → (𝑂‘𝑔) ∈ ℕ0)
86	85	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℕ0)
87	86	nn0zd 12543	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℤ)
88	65, 69	zmulcld 12633	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑁) ∈ ℤ)
89		ablfacrp.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))
90	11, 14	nnmulcld 12224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
91	90	nnnn0d 12492	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ0)
92	89, 91	eqeltrd 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
93	6	fvexi 6849	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
94		hashclb 14314	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
95	93, 94	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
96	92, 95	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ Fin)
97	96	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐵 ∈ Fin)
98	6, 7	oddvds2 19535	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑔 ∈ 𝐵) → (𝑂‘𝑔) ∥ (♯‘𝐵))
99	75, 97, 76, 98	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (♯‘𝐵))
100	89	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (♯‘𝐵) = (𝑀 · 𝑁))
101	99, 100	breqtrd 5112	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · 𝑁))
102	87, 88, 70, 101	dvdsmultr1d 16260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑏))
103	65	zcnd 12628	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℂ)
104	69	zcnd 12628	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℂ)
105	70	zcnd 12628	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℂ)
106	103, 104, 105	mulassd 11162	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑏) = (𝑀 · (𝑁 · 𝑏)))
107	102, 106	breqtrd 5112	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏)))
108	6, 7, 57	odmulgid 19523	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑁 · 𝑏) ∈ ℤ) ∧ 𝑀 ∈ ℤ) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
109	75, 76, 71, 65, 108	syl31anc 1376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
110	107, 109	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀)
111		fveq2 6835	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)))
112	111	breq1d 5096	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑀 ↔ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
113	112, 1	elrab2 3638	. . . . . . . . . . 11 ⊢ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ↔ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
114	84, 110, 113	sylanbrc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾)
115	6, 57	mulgcl 19061	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
116	75, 67, 76, 115	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
117	87, 88, 66, 101	dvdsmultr1d 16260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑎))
118		zcn 12523	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
119	118	ad2antrl 729	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℂ)
120		mulass 11120	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑀 · (𝑁 · 𝑎)))
121		mul12 11305	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (𝑀 · (𝑁 · 𝑎)) = (𝑁 · (𝑀 · 𝑎)))
122	120, 121	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
123	103, 104, 119, 122	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
124	117, 123	breqtrd 5112	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎)))
125	6, 7, 57	odmulgid 19523	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑀 · 𝑎) ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
126	75, 76, 67, 69, 125	syl31anc 1376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
127	124, 126	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁)
128		fveq2 6835	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
129	128	breq1d 5096	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
130	129, 2	elrab2 3638	. . . . . . . . . . 11 ⊢ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿 ↔ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
131	116, 127, 130	sylanbrc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)
132	77, 52	lsmelvali 19619	. . . . . . . . . 10 ⊢ (((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) ∧ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ∧ ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
133	81, 82, 114, 131, 132	syl22anc 839	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
134	80, 133	eqeltrd 2837	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
135		oveq1 7368	. . . . . . . . 9 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) = (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔))
136	135	eleq1d 2822	. . . . . . . 8 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → ((1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿) ↔ (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
137	134, 136	syl5ibrcom 247	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
138	64, 137	sylbid 240	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
139	138	rexlimdvva 3195	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
140	62, 139	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
141	59, 140	eqeltrrd 2838	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐾 ⊕ 𝐿))
142	56, 141	eqelssd 3944	. 2 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) = 𝐵)
143	51, 142	jca 511	1 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  {crab 3390  Vcvv 3430   ∩ cin 3889   ⊆ wss 3890  {csn 4568   class class class wbr 5086  ‘cfv 6493  (class class class)co 7361  Fincfn 8887  ℂcc 11030  1c1 11033   + caddc 11035   · cmul 11037  ℕcn 12168  ℕ₀cn0 12431  ℤcz 12518  ♯chash 14286   ∥ cdvds 16215   gcd cgcd 16457  Basecbs 17173  +_gcplusg 17214  0_gc0g 17396  Grpcgrp 18903  ._gcmg 19037  SubGrpcsubg 19090  odcod 19493  LSSumclsm 19603  Abelcabl 19750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-inf2 9556  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109  ax-pre-sup 11110

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-disj 5054  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-oadd 8403  df-omul 8404  df-er 8637  df-ec 8639  df-qs 8643  df-map 8769  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-sup 9349  df-inf 9350  df-oi 9419  df-card 9857  df-acn 9860  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-div 11802  df-nn 12169  df-2 12238  df-3 12239  df-n0 12432  df-z 12519  df-uz 12783  df-rp 12937  df-fz 13456  df-fzo 13603  df-fl 13745  df-mod 13823  df-seq 13958  df-exp 14018  df-hash 14287  df-cj 15055  df-re 15056  df-im 15057  df-sqrt 15191  df-abs 15192  df-clim 15444  df-sum 15643  df-dvds 16216  df-gcd 16458  df-sets 17128  df-slot 17146  df-ndx 17158  df-base 17174  df-ress 17195  df-plusg 17227  df-0g 17398  df-mgm 18602  df-sgrp 18681  df-mnd 18697  df-submnd 18746  df-grp 18906  df-minusg 18907  df-sbg 18908  df-mulg 19038  df-subg 19093  df-eqg 19095  df-cntz 19286  df-od 19497  df-lsm 19605  df-cmn 19751  df-abl 19752

This theorem is referenced by:  ablfacrp2  20038  ablfac1b  20041