ablfac1b - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ablfac1b		Structured version Visualization version GIF version

Theorem ablfac1b 20292

Description: Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016.)

**Hypotheses**
Ref	Expression
ablfac1.b	⊢ 𝐵 = (Base‘𝐺)
ablfac1.o	⊢ 𝑂 = (od‘𝐺)
ablfac1.s	⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
ablfac1.g	⊢ (𝜑 → 𝐺 ∈ Abel)
ablfac1.f	⊢ (𝜑 → 𝐵 ∈ Fin)
ablfac1.1	⊢ (𝜑 → 𝐴 ⊆ ℙ)

**Assertion**
Ref	Expression
ablfac1b	⊢ (𝜑 → 𝐺dom DProd 𝑆)

Distinct variable groups: 𝑥,𝑝,𝐵 𝜑,𝑝,𝑥 𝐴,𝑝,𝑥 𝑂,𝑝,𝑥 𝐺,𝑝,𝑥 Allowed substitution hints: 𝑆(𝑥, 𝑝)

Proof of Theorem ablfac1b Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2760	. 2 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2760	. 2 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		eqid 2760	. 2 ⊢ (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
4		ablfac1.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ Abel)
5		ablgrp 20005	. . 3 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
6	4, 5	syl 18	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		ablfac1.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℙ)
8		prmex 16858	. . . 4 ⊢ ℙ ∈ V
9	8	ssex 5281	. . 3 ⊢ (𝐴 ⊆ ℙ → 𝐴 ∈ V)
10	7, 9	syl 18	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
11	4	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐺 ∈ Abel)
12	7	sselda 3908	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℙ)
13		prmnn 16855	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
14	12, 13	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℕ)
15		ablfac1.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐺)
16	15	grpbn0 19183	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
17	6, 16	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ≠ ∅)
18		ablfac1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ Fin)
19		hashnncl 14514	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
20	18, 19	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
21	17, 20	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
22	21	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ)
23	12, 22	pccld 17034	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)
24	14, 23	nnexpcld 14393	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ)
25	24	nnzd 12723	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ)
26		ablfac1.o	. . . . 5 ⊢ 𝑂 = (od‘𝐺)
27	26, 15	oddvdssubg 20075	. . . 4 ⊢ ((𝐺 ∈ Abel ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺))
28	11, 25, 27	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺))
29		ablfac1.s	. . 3 ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
30	28, 29	fmptd 7115	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
31	4	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝐺 ∈ Abel)
32	30	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑆:𝐴⟶(SubGrp‘𝐺))
33		simpr1 1213	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝐴)
34	32, 33	ffvelcdmd 7086	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ∈ (SubGrp‘𝐺))
35		simpr2 1214	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝐴)
36	32, 35	ffvelcdmd 7086	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑏) ∈ (SubGrp‘𝐺))
37	1, 31, 34, 36	ablcntzd 20077	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑏)))
38		id 23	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → 𝑝 = 𝑎)
39		oveq1 7428	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → (𝑝 pCnt (♯‘𝐵)) = (𝑎 pCnt (♯‘𝐵)))
40	38, 39	oveq12d 7439	. . . . . . . . 9 ⊢ (𝑝 = 𝑎 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵))))
41	40	breq2d 5114	. . . . . . . 8 ⊢ (𝑝 = 𝑎 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))))
42	41	rabbidv 3419	. . . . . . 7 ⊢ (𝑝 = 𝑎 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
43	15	fvexi 6900	. . . . . . . 8 ⊢ 𝐵 ∈ V
44	43	rabex 5299	. . . . . . 7 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
45	42, 29, 44	fvmpt3i 7000	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
46	45	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
47		eqimss 3966	. . . . 5 ⊢ ((𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
48	46, 47	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
49	4	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐺 ∈ Abel)
50		eqid 2760	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
51	50	subgacs 19377	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
52		acsmre 17832	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
53	49, 5, 51, 52	4syl 20	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
54		df-ima 5663	. . . . . . 7 ⊢ (𝑆 “ (𝐴 ∖ {𝑎})) = ran (𝑆 ↾ (𝐴 ∖ {𝑎}))
55	7	sselda 3908	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℙ)
56	55	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℙ)
57	21	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℕ)
58		pcdvds 17048	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
59	56, 57, 58	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
60	7	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝐴 ⊆ ℙ)
61		eldifi 4067	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ∈ 𝐴)
62	61	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ 𝐴)
63	60, 62	sseldd 3909	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℙ)
64		pcdvds 17048	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
65	63, 57, 64	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
66		eqid 2760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎↑(𝑎 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵)))
67		eqid 2760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) = ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))
68	15, 26, 29, 4, 18, 7, 66, 67	ablfac1lem 20290	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1 ∧ (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))))
69	68	simp1d 1160	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ))
70	69	simpld 500	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ)
71	70	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ)
72	71	nnzd 12723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ)
73	63, 13	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℕ)
74	63, 57	pccld 17034	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)
75	73, 74	nnexpcld 14393	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ)
76	75	nnzd 12723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ)
77	57	nnzd 12723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ)
78		eldifsni 4749	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ≠ 𝑎)
79	78	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ≠ 𝑎)
80	79	necomd 3010	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ≠ 𝑝)
81		prmrp 16894	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
82	56, 63, 81	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
83	80, 82	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 gcd 𝑝) = 1)
84		prmz 16856	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℙ → 𝑎 ∈ ℤ)
85	56, 84	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℤ)
86		prmz 16856	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
87	63, 86	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℤ)
88	56, 57	pccld 17034	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 pCnt (♯‘𝐵)) ∈ ℕ₀)
89		rpexp12i 16906	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ ((𝑎 pCnt (♯‘𝐵)) ∈ ℕ₀ ∧ (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1))
90	85, 87, 88, 74, 89	syl112anc 1401	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1))
91	83, 90	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1)
92		coprmdvds2 16835	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)))
93	72, 76, 77, 91, 92	syl31anc 1400	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)))
94	59, 65, 93	mp2and 712	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵))
95	68	simp3d 1162	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
96	95	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
97	94, 96	breqtrd 5130	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
98	69	simprd 501	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)
99	98	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)
100	99	nnzd 12723	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ)
101	71	nnne0d 12392	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)
102		dvdscmulr 16460	. . . . . . . . . . . . . 14 ⊢ (((𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
103	76, 100, 72, 101, 102	syl112anc 1401	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
104	97, 103	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))
105	15, 26	odcl 19756	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ₀)
106	105	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ₀)
107	106	nn0zd 12722	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
108		dvdstr 16470	. . . . . . . . . . . . 13 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
109	107, 76, 100, 108	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
110	104, 109	mpan2d 707	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
111	110	ss2rabdv 4000	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
112	44	elpw 4560	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
113	111, 112	sylibr 237	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
114	29	reseq1i 5965	. . . . . . . . . 10 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎}))
115		difss 4072	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑎}) ⊆ 𝐴
116		resmpt 6028	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝑎}) ⊆ 𝐴 → ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}))
117	115, 116	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
118	114, 117	eqtri 2783	. . . . . . . . 9 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
119	113, 118	fmptd 7115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 ↾ (𝐴 ∖ {𝑎})):(𝐴 ∖ {𝑎})⟶𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
120	119	frnd 6719	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ran (𝑆 ↾ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
121	54, 120	eqsstrid 3946	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
122		sspwuni 5059	. . . . . 6 ⊢ ((𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
123	121, 122	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
124	98	nnzd 12723	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ)
125	26, 15	oddvdssubg 20075	. . . . . 6 ⊢ ((𝐺 ∈ Abel ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺))
126	49, 124, 125	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺))
127	3	mrcsscl 17800	. . . . 5 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∧ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
128	53, 123, 126, 127	syl3anc 1398	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
129		ss2in 4141	. . . 4 ⊢ (((𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∧ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}))
130	48, 128, 129	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}))
131		eqid 2760	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}
132		eqid 2760	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}
133	68	simp2d 1161	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1)
134		eqid 2760	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
135	15, 26, 131, 132, 49, 70, 98, 133, 95, 2, 134	ablfacrp 20288	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0_g‘𝐺)} ∧ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} (LSSum‘𝐺){𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = 𝐵))
136	135	simpld 500	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0_g‘𝐺)})
137	130, 136	sseqtrd 3944	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ {(0_g‘𝐺)})
138	1, 2, 3, 6, 10, 30, 37, 137	dmdprdd 20221	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 {crab 3412 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∩ cin 4089 ∅c0 4278 𝒫 cpw 4556 {csn 4584 ∪ cuni 4866 class class class wbr 5102 ↦ cmpt 5185 dom cdm 5650 ran crn 5651 ↾ cres 5652 “ cima 5653 ⟶wf 6535 ‘cfv 6539 (class class class)co 7421 Fincfn 8977 0cc0 11204 1c1 11205 · cmul 11209 / cdiv 11977 ℕcn 12339 ℕ₀cn0 12610 ℤcz 12697 ↑cexp 14208 ♯chash 14478 ∥ cdvds 16428 gcd cgcd 16670 ℙcprime 16852 pCnt cpc 17020 Basecbs 17393 0_gc0g 17616 Moorecmre 17758 mrClscmrc 17759 ACScacs 17761 Grpcgrp 19150 SubGrpcsubg 19336 Cntzccntz 19535 odcod 19744 LSSumclsm 19854 Abelcabl 20001 DProd cdprd 20215

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-inf2 9646 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-isom 6548 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-oadd 8484 df-omul 8485 df-er 8721 df-ec 8723 df-qs 8727 df-map 8853 df-ixp 8930 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-sup 9438 df-inf 9439 df-oi 9508 df-card 10024 df-acn 10027 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-n0 12611 df-z 12698 df-uz 12970 df-q 13080 df-rp 13125 df-fz 13644 df-fzo 13793 df-fl 13936 df-mod 14014 df-seq 14149 df-exp 14209 df-hash 14479 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-clim 15661 df-sum 15860 df-dvds 16429 df-gcd 16671 df-prm 16853 df-pc 17021 df-sets 17348 df-slot 17366 df-ndx 17378 df-base 17394 df-ress 17415 df-plusg 17447 df-0g 17618 df-mre 17762 df-mrc 17763 df-acs 17765 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-submnd 18985 df-grp 19153 df-minusg 19154 df-sbg 19155 df-mulg 19284 df-subg 19339 df-eqg 19341 df-cntz 19537 df-od 19748 df-lsm 19856 df-cmn 20002 df-abl 20003 df-dprd 20217

This theorem is used by: ablfac1c 20293 ablfac1eu 20295 ablfaclem2 20308 ablfaclem3 20309

W3C validator