Theorem ablfacrp 20005

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 4184	. . . . 5 ⊢ (𝐾 ∩ 𝐿) = ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁})
4		inrab 4282	. . . . 5 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
5	3, 4	eqtri 2753	. . . 4 ⊢ (𝐾 ∩ 𝐿) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
6		ablfacrp.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐺)
7		ablfacrp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (od‘𝐺)
8	6, 7	odcl 19473	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ0)
9	8	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ0)
10	9	nn0zd 12562	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
11		ablfacrp.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
12	11	nnzd 12563	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
13	12	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑀 ∈ ℤ)
14		ablfacrp.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
15	14	nnzd 12563	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
16	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ ℤ)
17		dvdsgcd 16521	. . . . . . . . . . 11 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
18	10, 13, 16, 17	syl3anc 1373	. . . . . . . . . 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 16296	. . . . . . . . 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 19722	. . . . . . . . . 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 19497	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
33	30, 23, 32	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
34	26, 33	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 = 0 )
35		velsn 4608	. . . . . 6 ⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
36	34, 35	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ { 0 })
37	36	rabssdv 4041	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)} ⊆ { 0 })
38	5, 37	eqsstrid 3988	. . 3 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ { 0 })
39	7, 6	oddvdssubg 19792	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
40	27, 12, 39	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
41	1, 40	eqeltrid 2833	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
42	31	subg0cl 19073	. . . . . 6 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐾)
43	41, 42	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐾)
44	7, 6	oddvdssubg 19792	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
45	27, 15, 44	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
46	2, 45	eqeltrid 2833	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (SubGrp‘𝐺))
47	31	subg0cl 19073	. . . . . 6 ⊢ (𝐿 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐿)
48	46, 47	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐿)
49	43, 48	elind 4166	. . . 4 ⊢ (𝜑 → 0 ∈ (𝐾 ∩ 𝐿))
50	49	snssd 4776	. . 3 ⊢ (𝜑 → { 0 } ⊆ (𝐾 ∩ 𝐿))
51	38, 50	eqssd 3967	. 2 ⊢ (𝜑 → (𝐾 ∩ 𝐿) = { 0 })
52		ablfacrp.s	. . . . . 6 ⊢ ⊕ = (LSSum‘𝐺)
53	52	lsmsubg2 19796	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
54	27, 41, 46, 53	syl3anc 1373	. . . 4 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
55	6	subgss 19066	. . . 4 ⊢ ((𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺) → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
56	54, 55	syl 17	. . 3 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
57		eqid 2730	. . . . . 6 ⊢ (.g‘𝐺) = (.g‘𝐺)
58	6, 57	mulg1 19020	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → (1(.g‘𝐺)𝑔) = 𝑔)
59	58	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) = 𝑔)
60		bezout 16520	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
61	12, 15, 60	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
62	61	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
63	20	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 gcd 𝑁) = 1)
64	63	eqeq1d 2732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) ↔ 1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏))))
65	12	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℤ)
66		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
67	65, 66	zmulcld 12651	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℤ)
68	67	zcnd 12646	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℂ)
69	15	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℤ)
70		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
71	69, 70	zmulcld 12651	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℤ)
72	71	zcnd 12646	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℂ)
73	68, 72	addcomd 11383	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎) + (𝑁 · 𝑏)) = ((𝑁 · 𝑏) + (𝑀 · 𝑎)))
74	73	oveq1d 7405	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔))
75	29	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐺 ∈ Grp)
76		simplr 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑔 ∈ 𝐵)
77		eqid 2730	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
78	6, 57, 77	mulgdir 19045	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ ((𝑁 · 𝑏) ∈ ℤ ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
79	75, 71, 67, 76, 78	syl13anc 1374	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
80	74, 79	eqtrd 2765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
81	41	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐾 ∈ (SubGrp‘𝐺))
82	46	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐿 ∈ (SubGrp‘𝐺))
83	6, 57	mulgcl 19030	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑁 · 𝑏) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
84	75, 71, 76, 83	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
85	6, 7	odcl 19473	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝐵 → (𝑂‘𝑔) ∈ ℕ0)
86	85	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℕ0)
87	86	nn0zd 12562	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℤ)
88	65, 69	zmulcld 12651	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑁) ∈ ℤ)
89		ablfacrp.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))
90	11, 14	nnmulcld 12246	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
91	90	nnnn0d 12510	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ0)
92	89, 91	eqeltrd 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
93	6	fvexi 6875	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
94		hashclb 14330	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
95	93, 94	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
96	92, 95	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ Fin)
97	96	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐵 ∈ Fin)
98	6, 7	oddvds2 19503	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑔 ∈ 𝐵) → (𝑂‘𝑔) ∥ (♯‘𝐵))
99	75, 97, 76, 98	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (♯‘𝐵))
100	89	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (♯‘𝐵) = (𝑀 · 𝑁))
101	99, 100	breqtrd 5136	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · 𝑁))
102	87, 88, 70, 101	dvdsmultr1d 16274	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑏))
103	65	zcnd 12646	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℂ)
104	69	zcnd 12646	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℂ)
105	70	zcnd 12646	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℂ)
106	103, 104, 105	mulassd 11204	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑏) = (𝑀 · (𝑁 · 𝑏)))
107	102, 106	breqtrd 5136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏)))
108	6, 7, 57	odmulgid 19491	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑁 · 𝑏) ∈ ℤ) ∧ 𝑀 ∈ ℤ) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
109	75, 76, 71, 65, 108	syl31anc 1375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
110	107, 109	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀)
111		fveq2 6861	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)))
112	111	breq1d 5120	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑀 ↔ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
113	112, 1	elrab2 3665	. . . . . . . . . . 11 ⊢ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ↔ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
114	84, 110, 113	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾)
115	6, 57	mulgcl 19030	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
116	75, 67, 76, 115	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
117	87, 88, 66, 101	dvdsmultr1d 16274	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑎))
118		zcn 12541	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
119	118	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℂ)
120		mulass 11163	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑀 · (𝑁 · 𝑎)))
121		mul12 11346	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (𝑀 · (𝑁 · 𝑎)) = (𝑁 · (𝑀 · 𝑎)))
122	120, 121	eqtrd 2765	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
123	103, 104, 119, 122	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
124	117, 123	breqtrd 5136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎)))
125	6, 7, 57	odmulgid 19491	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑀 · 𝑎) ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
126	75, 76, 67, 69, 125	syl31anc 1375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
127	124, 126	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁)
128		fveq2 6861	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
129	128	breq1d 5120	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
130	129, 2	elrab2 3665	. . . . . . . . . . 11 ⊢ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿 ↔ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
131	116, 127, 130	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)
132	77, 52	lsmelvali 19587	. . . . . . . . . 10 ⊢ (((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) ∧ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ∧ ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
133	81, 82, 114, 131, 132	syl22anc 838	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
134	80, 133	eqeltrd 2829	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
135		oveq1 7397	. . . . . . . . 9 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) = (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔))
136	135	eleq1d 2814	. . . . . . . 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 2830	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐾 ⊕ 𝐿))
142	56, 141	eqelssd 3971	. 2 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) = 𝐵)
143	51, 142	jca 511	1 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∃wrex 3054  {crab 3408  Vcvv 3450   ∩ cin 3916   ⊆ wss 3917  {csn 4592   class class class wbr 5110  ‘cfv 6514  (class class class)co 7390  Fincfn 8921  ℂcc 11073  1c1 11076   + caddc 11078   · cmul 11080  ℕcn 12193  ℕ₀cn0 12449  ℤcz 12536  ♯chash 14302   ∥ cdvds 16229   gcd cgcd 16471  Basecbs 17186  +_gcplusg 17227  0_gc0g 17409  Grpcgrp 18872  ._gcmg 19006  SubGrpcsubg 19059  odcod 19461  LSSumclsm 19571  Abelcabl 19718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-disj 5078  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-oadd 8441  df-omul 8442  df-er 8674  df-ec 8676  df-qs 8680  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-sup 9400  df-inf 9401  df-oi 9470  df-card 9899  df-acn 9902  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-n0 12450  df-z 12537  df-uz 12801  df-rp 12959  df-fz 13476  df-fzo 13623  df-fl 13761  df-mod 13839  df-seq 13974  df-exp 14034  df-hash 14303  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-clim 15461  df-sum 15660  df-dvds 16230  df-gcd 16472  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17187  df-ress 17208  df-plusg 17240  df-0g 17411  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-submnd 18718  df-grp 18875  df-minusg 18876  df-sbg 18877  df-mulg 19007  df-subg 19062  df-eqg 19064  df-cntz 19256  df-od 19465  df-lsm 19573  df-cmn 19719  df-abl 19720

This theorem is referenced by:  ablfacrp2  20006  ablfac1b  20009