Theorem ablfacrp 18909

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 4113	. . . . 5 ⊢ (𝐾 ∩ 𝐿) = ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁})
4		inrab 4201	. . . . 5 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁}) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
5	3, 4	eqtri 2821	. . . 4 ⊢ (𝐾 ∩ 𝐿) = {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)}
6		ablfacrp.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐺)
7		ablfacrp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (od‘𝐺)
8	6, 7	odcl 18399	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ0)
9	8	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ0)
10	9	nn0zd 11939	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
11		ablfacrp.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
12	11	nnzd 11940	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
13	12	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑀 ∈ ℤ)
14		ablfacrp.n	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℕ)
15	14	nnzd 11940	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
16	15	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ ℤ)
17		dvdsgcd 15725	. . . . . . . . . . 11 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
18	10, 13, 16, 17	syl3anc 1364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁)))
19	18	3impia 1110	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) ∥ (𝑀 gcd 𝑁))
20		ablfacrp.1	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1)
21	20	3ad2ant1 1126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑀 gcd 𝑁) = 1)
22	19, 21	breqtrd 4994	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) ∥ 1)
23		simp2 1130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ 𝐵)
24		dvds1 15506	. . . . . . . . 9 ⊢ ((𝑂‘𝑥) ∈ ℕ0 → ((𝑂‘𝑥) ∥ 1 ↔ (𝑂‘𝑥) = 1))
25	23, 8, 24	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) ∥ 1 ↔ (𝑂‘𝑥) = 1))
26	22, 25	mpbid 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → (𝑂‘𝑥) = 1)
27		ablfacrp.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ Abel)
28		ablgrp 18642	. . . . . . . . . 10 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
29	27, 28	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ Grp)
30	29	3ad2ant1 1126	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝐺 ∈ Grp)
31		ablfacrp.z	. . . . . . . . 9 ⊢ 0 = (0g‘𝐺)
32	7, 31, 6	odeq1 18421	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
33	30, 23, 32	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → ((𝑂‘𝑥) = 1 ↔ 𝑥 = 0 ))
34	26, 33	mpbid 233	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 = 0 )
35		velsn 4494	. . . . . 6 ⊢ (𝑥 ∈ { 0 } ↔ 𝑥 = 0 )
36	34, 35	sylibr 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)) → 𝑥 ∈ { 0 })
37	36	rabssdv 3978	. . . 4 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((𝑂‘𝑥) ∥ 𝑀 ∧ (𝑂‘𝑥) ∥ 𝑁)} ⊆ { 0 })
38	5, 37	eqsstrid 3942	. . 3 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ { 0 })
39	7, 6	oddvdssubg 18702	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
40	27, 12, 39	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} ∈ (SubGrp‘𝐺))
41	1, 40	syl5eqel 2889	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺))
42	31	subg0cl 18045	. . . . . 6 ⊢ (𝐾 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐾)
43	41, 42	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐾)
44	7, 6	oddvdssubg 18702	. . . . . . . 8 ⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
45	27, 15, 44	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺))
46	2, 45	syl5eqel 2889	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ (SubGrp‘𝐺))
47	31	subg0cl 18045	. . . . . 6 ⊢ (𝐿 ∈ (SubGrp‘𝐺) → 0 ∈ 𝐿)
48	46, 47	syl 17	. . . . 5 ⊢ (𝜑 → 0 ∈ 𝐿)
49	43, 48	elind 4098	. . . 4 ⊢ (𝜑 → 0 ∈ (𝐾 ∩ 𝐿))
50	49	snssd 4655	. . 3 ⊢ (𝜑 → { 0 } ⊆ (𝐾 ∩ 𝐿))
51	38, 50	eqssd 3912	. 2 ⊢ (𝜑 → (𝐾 ∩ 𝐿) = { 0 })
52		ablfacrp.s	. . . . . 6 ⊢ ⊕ = (LSSum‘𝐺)
53	52	lsmsubg2 18706	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
54	27, 41, 46, 53	syl3anc 1364	. . . 4 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺))
55	6	subgss 18038	. . . 4 ⊢ ((𝐾 ⊕ 𝐿) ∈ (SubGrp‘𝐺) → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
56	54, 55	syl 17	. . 3 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) ⊆ 𝐵)
57		eqid 2797	. . . . . 6 ⊢ (.g‘𝐺) = (.g‘𝐺)
58	6, 57	mulg1 17994	. . . . 5 ⊢ (𝑔 ∈ 𝐵 → (1(.g‘𝐺)𝑔) = 𝑔)
59	58	adantl 482	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) = 𝑔)
60		bezout 15724	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
61	12, 15, 60	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
62	61	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))
63	20	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 gcd 𝑁) = 1)
64	63	eqeq1d 2799	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) ↔ 1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏))))
65	12	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℤ)
66		simprl 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℤ)
67	65, 66	zmulcld 11947	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℤ)
68	67	zcnd 11942	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑎) ∈ ℂ)
69	15	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℤ)
70		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℤ)
71	69, 70	zmulcld 11947	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℤ)
72	71	zcnd 11942	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑁 · 𝑏) ∈ ℂ)
73	68, 72	addcomd 10695	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎) + (𝑁 · 𝑏)) = ((𝑁 · 𝑏) + (𝑀 · 𝑎)))
74	73	oveq1d 7038	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔))
75	29	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐺 ∈ Grp)
76		simplr 765	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑔 ∈ 𝐵)
77		eqid 2797	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
78	6, 57, 77	mulgdir 18017	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ ((𝑁 · 𝑏) ∈ ℤ ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
79	75, 71, 67, 76, 78	syl13anc 1365	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏) + (𝑀 · 𝑎))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
80	74, 79	eqtrd 2833	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) = (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
81	41	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐾 ∈ (SubGrp‘𝐺))
82	46	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐿 ∈ (SubGrp‘𝐺))
83	6, 57	mulgcl 18004	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑁 · 𝑏) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
84	75, 71, 76, 83	syl3anc 1364	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵)
85	6, 7	odcl 18399	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ 𝐵 → (𝑂‘𝑔) ∈ ℕ0)
86	85	ad2antlr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℕ0)
87	86	nn0zd 11939	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∈ ℤ)
88	65, 69	zmulcld 11947	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑀 · 𝑁) ∈ ℤ)
89		ablfacrp.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁))
90	11, 14	nnmulcld 11544	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ)
91	90	nnnn0d 11809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑀 · 𝑁) ∈ ℕ0)
92	89, 91	eqeltrd 2885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
93	6	fvexi 6559	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
94		hashclb 13573	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
95	93, 94	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
96	92, 95	sylibr 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ Fin)
97	96	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐵 ∈ Fin)
98	6, 7	oddvds2 18427	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑔 ∈ 𝐵) → (𝑂‘𝑔) ∥ (♯‘𝐵))
99	75, 97, 76, 98	syl3anc 1364	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (♯‘𝐵))
100	89	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (♯‘𝐵) = (𝑀 · 𝑁))
101	99, 100	breqtrd 4994	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · 𝑁))
102	87, 88, 70, 101	dvdsmultr1d 15485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑏))
103	65	zcnd 11942	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑀 ∈ ℂ)
104	69	zcnd 11942	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈ ℂ)
105	70	zcnd 11942	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈ ℂ)
106	103, 104, 105	mulassd 10517	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑏) = (𝑀 · (𝑁 · 𝑏)))
107	102, 106	breqtrd 4994	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏)))
108	6, 7, 57	odmulgid 18415	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑁 · 𝑏) ∈ ℤ) ∧ 𝑀 ∈ ℤ) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
109	75, 76, 71, 65, 108	syl31anc 1366	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀 ↔ (𝑂‘𝑔) ∥ (𝑀 · (𝑁 · 𝑏))))
110	107, 109	mpbird 258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀)
111		fveq2 6545	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)))
112	111	breq1d 4978	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑁 · 𝑏)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑀 ↔ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
113	112, 1	elrab2 3624	. . . . . . . . . . 11 ⊢ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ↔ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑁 · 𝑏)(.g‘𝐺)𝑔)) ∥ 𝑀))
114	84, 110, 113	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾)
115	6, 57	mulgcl 18004	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑎) ∈ ℤ ∧ 𝑔 ∈ 𝐵) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
116	75, 67, 76, 115	syl3anc 1364	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵)
117	87, 88, 66, 101	dvdsmultr1d 15485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ ((𝑀 · 𝑁) · 𝑎))
118		zcn 11840	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
119	118	ad2antrl 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈ ℂ)
120		mulass 10478	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑀 · (𝑁 · 𝑎)))
121		mul12 10658	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (𝑀 · (𝑁 · 𝑎)) = (𝑁 · (𝑀 · 𝑎)))
122	120, 121	eqtrd 2833	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
123	103, 104, 119, 122	syl3anc 1364	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑁) · 𝑎) = (𝑁 · (𝑀 · 𝑎)))
124	117, 123	breqtrd 4994	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎)))
125	6, 7, 57	odmulgid 18415	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝑀 · 𝑎) ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
126	75, 76, 67, 69, 125	syl31anc 1366	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁 ↔ (𝑂‘𝑔) ∥ (𝑁 · (𝑀 · 𝑎))))
127	124, 126	mpbird 258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁)
128		fveq2 6545	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → (𝑂‘𝑥) = (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)))
129	128	breq1d 4978	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑀 · 𝑎)(.g‘𝐺)𝑔) → ((𝑂‘𝑥) ∥ 𝑁 ↔ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
130	129, 2	elrab2 3624	. . . . . . . . . . 11 ⊢ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿 ↔ (((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐵 ∧ (𝑂‘((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∥ 𝑁))
131	116, 127, 130	sylanbrc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)
132	77, 52	lsmelvali 18509	. . . . . . . . . 10 ⊢ (((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐿 ∈ (SubGrp‘𝐺)) ∧ (((𝑁 · 𝑏)(.g‘𝐺)𝑔) ∈ 𝐾 ∧ ((𝑀 · 𝑎)(.g‘𝐺)𝑔) ∈ 𝐿)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
133	81, 82, 114, 131, 132	syl22anc 835	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑁 · 𝑏)(.g‘𝐺)𝑔)(+g‘𝐺)((𝑀 · 𝑎)(.g‘𝐺)𝑔)) ∈ (𝐾 ⊕ 𝐿))
134	80, 133	eqeltrd 2885	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
135		oveq1 7030	. . . . . . . . 9 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) = (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔))
136	135	eleq1d 2869	. . . . . . . 8 ⊢ (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → ((1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿) ↔ (((𝑀 · 𝑎) + (𝑁 · 𝑏))(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
137	134, 136	syl5ibrcom 248	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (1 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
138	64, 137	sylbid 241	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐵) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
139	138	rexlimdvva 3259	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝑀 gcd 𝑁) = ((𝑀 · 𝑎) + (𝑁 · 𝑏)) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿)))
140	62, 139	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → (1(.g‘𝐺)𝑔) ∈ (𝐾 ⊕ 𝐿))
141	59, 140	eqeltrrd 2886	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ (𝐾 ⊕ 𝐿))
142	56, 141	eqelssd 3915	. 2 ⊢ (𝜑 → (𝐾 ⊕ 𝐿) = 𝐵)
143	51, 142	jca 512	1 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083  ∃wrex 3108  {crab 3111  Vcvv 3440   ∩ cin 3864   ⊆ wss 3865  {csn 4478   class class class wbr 4968  ‘cfv 6232  (class class class)co 7023  Fincfn 8364  ℂcc 10388  1c1 10391   + caddc 10393   · cmul 10395  ℕcn 11492  ℕ₀cn0 11751  ℤcz 11835  ♯chash 13544   ∥ cdvds 15444   gcd cgcd 15680  Basecbs 16316  +_gcplusg 16398  0_gc0g 16546  Grpcgrp 17865  ._gcmg 17985  SubGrpcsubg 18031  odcod 18387  LSSumclsm 18493  Abelcabl 18638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-disj 4937  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-omul 7965  df-er 8146  df-ec 8148  df-qs 8152  df-map 8265  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-sup 8759  df-inf 8760  df-oi 8827  df-card 9221  df-acn 9224  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-n0 11752  df-z 11836  df-uz 12098  df-rp 12244  df-fz 12747  df-fzo 12888  df-fl 13016  df-mod 13092  df-seq 13224  df-exp 13284  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-clim 14683  df-sum 14881  df-dvds 15445  df-gcd 15681  df-ndx 16319  df-slot 16320  df-base 16322  df-sets 16323  df-ress 16324  df-plusg 16411  df-0g 16548  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-submnd 17779  df-grp 17868  df-minusg 17869  df-sbg 17870  df-mulg 17986  df-subg 18034  df-eqg 18036  df-cntz 18192  df-od 18391  df-lsm 18495  df-cmn 18639  df-abl 18640

This theorem is referenced by:  ablfacrp2  18910  ablfac1b  18913