Theorem ablfacrp 20133

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 4171	. . . . 5 ⊢ (𝐾 ∩ 𝐿) = ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁})
4		inrab 4269	. . . . 5 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
5	3, 4	eqtri 2786	. . . 4 ⊢ (𝐾 ∩ 𝐿) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
6		ablfacrp.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐺)
7		ablfacrp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (od‘𝐺)
8	6, 7	odcl 19601	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ0)
9	8	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ0)
10	9	nn0zd 12611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
11		ablfacrp.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
12	11	nnzd 12612	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
13	12	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑀 ∈ ℤ)
14		ablfacrp.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
15	14	nnzd 12612	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
16	15	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ ℤ)
17		dvdsgcd 16597	. . . . . . . . . . 11 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
18	10, 13, 16, 17	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
19	18	3impia 1135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁))
20		ablfacrp.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
21	20	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑀 gcd 𝑁) = 1)
22	19, 21	breqtrd 5137	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) ∥ 1)
23		simp2 1155	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ 𝐵)
24		dvds1 16372	. . . . . . . . 9 ⊢ ((𝑂‘𝑥) ∈ ℕ0 → ((𝑂‘𝑥) ∥ 1 ↔ (𝑂‘𝑥) = 1))
25	23, 8, 24	3syl 19	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) ∥ 1 ↔ (𝑂‘𝑥) = 1))
26	22, 25	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) = 1)
27		ablfacrp.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ Abel)
28		ablgrp 19850	. . . . . . . . . 10 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
29	27, 28	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
30	29	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝐺 ∈ Grp)
31		ablfacrp.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐺)
32	7, 31, 6	odeq1 19625	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
33	30, 23, 32	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
34	26, 33	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 = 0 )
35		velsn 4605	. . . . . 6 ⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
36	34, 35	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ { 0 })
37	36	rabssdv 4028	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)} ⊆ { 0 })
38	5, 37	eqsstrid 3975	. . 3 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ { 0 })
39	7, 6	oddvdssubg 19920	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
40	27, 12, 39	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
41	1, 40	eqeltrid 2867	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
42	31	subg0cl 19195	. . . . . 6 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐾)
43	41, 42	syl 18	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐾)
44	7, 6	oddvdssubg 19920	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
45	27, 15, 44	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
46	2, 45	eqeltrid 2867	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (SubGrp‘𝐺))
47	31	subg0cl 19195	. . . . . 6 ⊢ (𝐿 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐿)
48	46, 47	syl 18	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐿)
49	43, 48	elind 4153	. . . 4 ⊢ (𝜑 → 0 ∈ (𝐾 ∩ 𝐿))
50	49	snssd 4752	. . 3 ⊢ (𝜑 → { 0 } ⊆ (𝐾 ∩ 𝐿))
51	38, 50	eqssd 3954	. 2 ⊢ (𝜑 → (𝐾 ∩ 𝐿) = { 0 })
52		ablfacrp.s	. . . . . 6 ⊢ ⊕ = (LSSum‘𝐺)
53	52	lsmsubg2 19924	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
54	27, 41, 46, 53	syl3anc 1398	. . . 4 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
55	6	subgss 19188	. . . 4 ⊢ ((𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺) → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
56	54, 55	syl 18	. . 3 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
57		eqid 2763	. . . . . 6 ⊢ (.g‘𝐺) = (.g‘𝐺)
58	6, 57	mulg1 19142	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → (1(.g‘𝐺)𝑔) = 𝑔)
59	58	adantl 486	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) = 𝑔)
60		bezout 16596	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
61	12, 15, 60	syl2anc 595	. . . . . 6 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
62	61	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
63	20	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 gcd 𝑁) = 1)
64	63	eqeq1d 2765	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) ↔ 1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏))))
65	12	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℤ)
66		simprl 782	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
67	65, 66	zmulcld 12701	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℤ)
68	67	zcnd 12696	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℂ)
69	15	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℤ)
70		simprr 784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
71	69, 70	zmulcld 12701	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℤ)
72	71	zcnd 12696	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℂ)
73	68, 72	addcomd 11407	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎) + (𝑁 · 𝑏)) = ((𝑁 · 𝑏) + (𝑀 · 𝑎)))
74	73	oveq1d 7425	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔))
75	29	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐺 ∈ Grp)
76		simplr 780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑔 ∈ 𝐵)
77		eqid 2763	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
78	6, 57, 77	mulgdir 19167	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ ((𝑁 · 𝑏) ∈ ℤ ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
79	75, 71, 67, 76, 78	syl13anc 1399	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
80	74, 79	eqtrd 2798	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
81	41	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐾 ∈ (SubGrp‘𝐺))
82	46	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐿 ∈ (SubGrp‘𝐺))
83	6, 57	mulgcl 19152	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑁 · 𝑏) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
84	75, 71, 76, 83	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
85	6, 7	odcl 19601	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝐵 → (𝑂‘𝑔) ∈ ℕ0)
86	85	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℕ0)
87	86	nn0zd 12611	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℤ)
88	65, 69	zmulcld 12701	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑁) ∈ ℤ)
89		ablfacrp.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))
90	11, 14	nnmulcld 12284	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
91	90	nnnn0d 12560	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ0)
92	89, 91	eqeltrd 2863	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
93	6	fvexi 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
94		hashclb 14390	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
95	93, 94	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
96	92, 95	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ Fin)
97	96	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐵 ∈ Fin)
98	6, 7	oddvds2 19631	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑔 ∈ 𝐵) → (𝑂‘𝑔) ∥ (♯‘𝐵))
99	75, 97, 76, 98	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (♯‘𝐵))
100	89	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (♯‘𝐵) = (𝑀 · 𝑁))
101	99, 100	breqtrd 5137	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · 𝑁))
102	87, 88, 70, 101	dvdsmultr1d 16350	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑏))
103	65	zcnd 12696	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℂ)
104	69	zcnd 12696	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℂ)
105	70	zcnd 12696	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℂ)
106	103, 104, 105	mulassd 11227	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑏) = (𝑀 · (𝑁 · 𝑏)))
107	102, 106	breqtrd 5137	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏)))
108	6, 7, 57	odmulgid 19619	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑁 · 𝑏) ∈ ℤ) ∧ 𝑀 ∈ ℤ) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
109	75, 76, 71, 65, 108	syl31anc 1400	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
110	107, 109	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀)
111		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)))
112	111	breq1d 5119	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑀 ↔ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
113	112, 1	elrab2 3654	. . . . . . . . . . 11 ⊢ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ↔ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
114	84, 110, 113	sylanbrc 594	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾)
115	6, 57	mulgcl 19152	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
116	75, 67, 76, 115	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
117	87, 88, 66, 101	dvdsmultr1d 16350	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑎))
118		zcn 12591	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
119	118	ad2antrl 740	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℂ)
120		mulass 11183	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑀 · (𝑁 · 𝑎)))
121		mul12 11370	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (𝑀 · (𝑁 · 𝑎)) = (𝑁 · (𝑀 · 𝑎)))
122	120, 121	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
123	103, 104, 119, 122	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
124	117, 123	breqtrd 5137	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎)))
125	6, 7, 57	odmulgid 19619	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑀 · 𝑎) ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
126	75, 76, 67, 69, 125	syl31anc 1400	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
127	124, 126	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁)
128		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
129	128	breq1d 5119	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
130	129, 2	elrab2 3654	. . . . . . . . . . 11 ⊢ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿 ↔ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
131	116, 127, 130	sylanbrc 594	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)
132	77, 52	lsmelvali 19715	. . . . . . . . . 10 ⊢ (((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) ∧ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ∧ ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
133	81, 82, 114, 131, 132	syl22anc 851	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
134	80, 133	eqeltrd 2863	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
135		oveq1 7417	. . . . . . . . 9 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) = (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔))
136	135	eleq1d 2848	. . . . . . . 8 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → ((1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿) ↔ (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
137	134, 136	syl5ibrcom 250	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
138	64, 137	sylbid 243	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
139	138	rexlimdvva 3222	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
140	62, 139	mpd 16	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
141	59, 140	eqeltrrd 2864	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐾 ⊕ 𝐿))
142	56, 141	eqelssd 3958	. 2 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) = 𝐵)
143	51, 142	jca 520	1 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ∃wrex 3089  {crab 3416  Vcvv 3455   ∩ cin 3904   ⊆ wss 3905  {csn 4589   class class class wbr 5109  ‘cfv 6536  (class class class)co 7410  Fincfn 8939  ℂcc 11093  1c1 11096   + caddc 11098   · cmul 11100  ℕcn 12228  ℕ₀cn0 12499  ℤcz 12586  ♯chash 14362   ∥ cdvds 16305   gcd cgcd 16547  Basecbs 17264  +_gcplusg 17305  0_gc0g 17487  Grpcgrp 18995  ._gcmg 19128  SubGrpcsubg 19181  odcod 19589  LSSumclsm 19699  Abelcabl 19846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9606  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-disj 5077  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-oadd 8453  df-omul 8454  df-er 8690  df-ec 8692  df-qs 8696  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9398  df-inf 9399  df-oi 9468  df-card 9921  df-acn 9924  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-2 12298  df-3 12299  df-n0 12500  df-z 12587  df-uz 12858  df-rp 13012  df-fz 13531  df-fzo 13679  df-fl 13821  df-mod 13899  df-seq 14034  df-exp 14094  df-hash 14363  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283  df-clim 15535  df-sum 15734  df-dvds 16306  df-gcd 16548  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-ress 17286  df-plusg 17318  df-0g 17489  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-submnd 18837  df-grp 18998  df-minusg 18999  df-sbg 19000  df-mulg 19129  df-subg 19184  df-eqg 19186  df-cntz 19382  df-od 19593  df-lsm 19701  df-cmn 19847  df-abl 19848

This theorem is referenced by:  ablfacrp2  20134  ablfac1b  20137