Theorem ablfacrp 19859

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 4175	. . . . 5 ⊢ (𝐾 ∩ 𝐿) = ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁})
4		inrab 4271	. . . . 5 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
5	3, 4	eqtri 2759	. . . 4 ⊢ (𝐾 ∩ 𝐿) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
6		ablfacrp.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐺)
7		ablfacrp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (od‘𝐺)
8	6, 7	odcl 19332	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ0)
9	8	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ0)
10	9	nn0zd 12534	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
11		ablfacrp.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
12	11	nnzd 12535	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
13	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑀 ∈ ℤ)
14		ablfacrp.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
15	14	nnzd 12535	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
16	15	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ ℤ)
17		dvdsgcd 16436	. . . . . . . . . . 11 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
18	10, 13, 16, 17	syl3anc 1371	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
19	18	3impia 1117	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁))
20		ablfacrp.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
21	20	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑀 gcd 𝑁) = 1)
22	19, 21	breqtrd 5136	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) ∥ 1)
23		simp2 1137	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ 𝐵)
24		dvds1 16212	. . . . . . . . 9 ⊢ ((𝑂‘𝑥) ∈ ℕ0 → ((𝑂‘𝑥) ∥ 1 ↔ (𝑂‘𝑥) = 1))
25	23, 8, 24	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) ∥ 1 ↔ (𝑂‘𝑥) = 1))
26	22, 25	mpbid 231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) = 1)
27		ablfacrp.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ Abel)
28		ablgrp 19581	. . . . . . . . . 10 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
29	27, 28	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
30	29	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝐺 ∈ Grp)
31		ablfacrp.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐺)
32	7, 31, 6	odeq1 19356	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
33	30, 23, 32	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
34	26, 33	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 = 0 )
35		velsn 4607	. . . . . 6 ⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
36	34, 35	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ { 0 })
37	36	rabssdv 4037	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)} ⊆ { 0 })
38	5, 37	eqsstrid 3995	. . 3 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ { 0 })
39	7, 6	oddvdssubg 19647	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
40	27, 12, 39	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
41	1, 40	eqeltrid 2836	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
42	31	subg0cl 18950	. . . . . 6 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐾)
43	41, 42	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐾)
44	7, 6	oddvdssubg 19647	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
45	27, 15, 44	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
46	2, 45	eqeltrid 2836	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (SubGrp‘𝐺))
47	31	subg0cl 18950	. . . . . 6 ⊢ (𝐿 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐿)
48	46, 47	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐿)
49	43, 48	elind 4159	. . . 4 ⊢ (𝜑 → 0 ∈ (𝐾 ∩ 𝐿))
50	49	snssd 4774	. . 3 ⊢ (𝜑 → { 0 } ⊆ (𝐾 ∩ 𝐿))
51	38, 50	eqssd 3964	. 2 ⊢ (𝜑 → (𝐾 ∩ 𝐿) = { 0 })
52		ablfacrp.s	. . . . . 6 ⊢ ⊕ = (LSSum‘𝐺)
53	52	lsmsubg2 19651	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
54	27, 41, 46, 53	syl3anc 1371	. . . 4 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
55	6	subgss 18943	. . . 4 ⊢ ((𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺) → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
56	54, 55	syl 17	. . 3 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
57		eqid 2731	. . . . . 6 ⊢ (.g‘𝐺) = (.g‘𝐺)
58	6, 57	mulg1 18897	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → (1(.g‘𝐺)𝑔) = 𝑔)
59	58	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) = 𝑔)
60		bezout 16435	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
61	12, 15, 60	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
62	61	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
63	20	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 gcd 𝑁) = 1)
64	63	eqeq1d 2733	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) ↔ 1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏))))
65	12	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℤ)
66		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
67	65, 66	zmulcld 12622	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℤ)
68	67	zcnd 12617	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℂ)
69	15	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℤ)
70		simprr 771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
71	69, 70	zmulcld 12622	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℤ)
72	71	zcnd 12617	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℂ)
73	68, 72	addcomd 11366	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎) + (𝑁 · 𝑏)) = ((𝑁 · 𝑏) + (𝑀 · 𝑎)))
74	73	oveq1d 7377	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔))
75	29	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐺 ∈ Grp)
76		simplr 767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑔 ∈ 𝐵)
77		eqid 2731	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
78	6, 57, 77	mulgdir 18922	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ ((𝑁 · 𝑏) ∈ ℤ ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
79	75, 71, 67, 76, 78	syl13anc 1372	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
80	74, 79	eqtrd 2771	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
81	41	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐾 ∈ (SubGrp‘𝐺))
82	46	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐿 ∈ (SubGrp‘𝐺))
83	6, 57	mulgcl 18907	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑁 · 𝑏) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
84	75, 71, 76, 83	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
85	6, 7	odcl 19332	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝐵 → (𝑂‘𝑔) ∈ ℕ0)
86	85	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℕ0)
87	86	nn0zd 12534	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℤ)
88	65, 69	zmulcld 12622	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑁) ∈ ℤ)
89		ablfacrp.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))
90	11, 14	nnmulcld 12215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
91	90	nnnn0d 12482	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ0)
92	89, 91	eqeltrd 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
93	6	fvexi 6861	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
94		hashclb 14268	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
95	93, 94	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
96	92, 95	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ Fin)
97	96	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐵 ∈ Fin)
98	6, 7	oddvds2 19362	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑔 ∈ 𝐵) → (𝑂‘𝑔) ∥ (♯‘𝐵))
99	75, 97, 76, 98	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (♯‘𝐵))
100	89	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (♯‘𝐵) = (𝑀 · 𝑁))
101	99, 100	breqtrd 5136	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · 𝑁))
102	87, 88, 70, 101	dvdsmultr1d 16190	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑏))
103	65	zcnd 12617	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℂ)
104	69	zcnd 12617	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℂ)
105	70	zcnd 12617	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℂ)
106	103, 104, 105	mulassd 11187	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑏) = (𝑀 · (𝑁 · 𝑏)))
107	102, 106	breqtrd 5136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏)))
108	6, 7, 57	odmulgid 19350	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑁 · 𝑏) ∈ ℤ) ∧ 𝑀 ∈ ℤ) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
109	75, 76, 71, 65, 108	syl31anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
110	107, 109	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀)
111		fveq2 6847	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)))
112	111	breq1d 5120	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑀 ↔ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
113	112, 1	elrab2 3651	. . . . . . . . . . 11 ⊢ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ↔ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
114	84, 110, 113	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾)
115	6, 57	mulgcl 18907	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
116	75, 67, 76, 115	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
117	87, 88, 66, 101	dvdsmultr1d 16190	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑎))
118		zcn 12513	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
119	118	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℂ)
120		mulass 11148	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑀 · (𝑁 · 𝑎)))
121		mul12 11329	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (𝑀 · (𝑁 · 𝑎)) = (𝑁 · (𝑀 · 𝑎)))
122	120, 121	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
123	103, 104, 119, 122	syl3anc 1371	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
124	117, 123	breqtrd 5136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎)))
125	6, 7, 57	odmulgid 19350	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑀 · 𝑎) ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
126	75, 76, 67, 69, 125	syl31anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
127	124, 126	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁)
128		fveq2 6847	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
129	128	breq1d 5120	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
130	129, 2	elrab2 3651	. . . . . . . . . . 11 ⊢ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿 ↔ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
131	116, 127, 130	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)
132	77, 52	lsmelvali 19446	. . . . . . . . . 10 ⊢ (((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) ∧ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ∧ ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
133	81, 82, 114, 131, 132	syl22anc 837	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
134	80, 133	eqeltrd 2832	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
135		oveq1 7369	. . . . . . . . 9 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) = (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔))
136	135	eleq1d 2817	. . . . . . . 8 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → ((1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿) ↔ (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
137	134, 136	syl5ibrcom 246	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
138	64, 137	sylbid 239	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
139	138	rexlimdvva 3201	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
140	62, 139	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
141	59, 140	eqeltrrd 2833	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐾 ⊕ 𝐿))
142	56, 141	eqelssd 3968	. 2 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) = 𝐵)
143	51, 142	jca 512	1 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∃wrex 3069  {crab 3405  Vcvv 3446   ∩ cin 3912   ⊆ wss 3913  {csn 4591   class class class wbr 5110  ‘cfv 6501  (class class class)co 7362  Fincfn 8890  ℂcc 11058  1c1 11061   + caddc 11063   · cmul 11065  ℕcn 12162  ℕ₀cn0 12422  ℤcz 12508  ♯chash 14240   ∥ cdvds 16147   gcd cgcd 16385  Basecbs 17094  +_gcplusg 17147  0_gc0g 17335  Grpcgrp 18762  ._gcmg 18886  SubGrpcsubg 18936  odcod 19320  LSSumclsm 19430  Abelcabl 19577

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9586  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137  ax-pre-sup 11138

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-disj 5076  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-omul 8422  df-er 8655  df-ec 8657  df-qs 8661  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9387  df-inf 9388  df-oi 9455  df-card 9884  df-acn 9887  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-div 11822  df-nn 12163  df-2 12225  df-3 12226  df-n0 12423  df-z 12509  df-uz 12773  df-rp 12925  df-fz 13435  df-fzo 13578  df-fl 13707  df-mod 13785  df-seq 13917  df-exp 13978  df-hash 14241  df-cj 14996  df-re 14997  df-im 14998  df-sqrt 15132  df-abs 15133  df-clim 15382  df-sum 15583  df-dvds 16148  df-gcd 16386  df-sets 17047  df-slot 17065  df-ndx 17077  df-base 17095  df-ress 17124  df-plusg 17160  df-0g 17337  df-mgm 18511  df-sgrp 18560  df-mnd 18571  df-submnd 18616  df-grp 18765  df-minusg 18766  df-sbg 18767  df-mulg 18887  df-subg 18939  df-eqg 18941  df-cntz 19111  df-od 19324  df-lsm 19432  df-cmn 19578  df-abl 19579

This theorem is referenced by:  ablfacrp2  19860  ablfac1b  19863