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 20047

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 2736	. 2 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2736	. 2 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		eqid 2736	. 2 ⊢ (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
4		ablfac1.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ Abel)
5		ablgrp 19760	. . 3 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		ablfac1.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℙ)
8		prmex 16646	. . . 4 ⊢ ℙ ∈ V
9	8	ssex 5262	. . 3 ⊢ (𝐴 ⊆ ℙ → 𝐴 ∈ V)
10	7, 9	syl 17	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
11	4	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐺 ∈ Abel)
12	7	sselda 3921	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℙ)
13		prmnn 16643	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
14	12, 13	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℕ)
15		ablfac1.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐺)
16	15	grpbn0 18942	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
17	6, 16	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ≠ ∅)
18		ablfac1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ Fin)
19		hashnncl 14328	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
21	17, 20	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
22	21	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ)
23	12, 22	pccld 16821	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)
24	14, 23	nnexpcld 14207	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ)
25	24	nnzd 12550	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ)
26		ablfac1.o	. . . . 5 ⊢ 𝑂 = (od‘𝐺)
27	26, 15	oddvdssubg 19830	. . . 4 ⊢ ((𝐺 ∈ Abel ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺))
28	11, 25, 27	syl2anc 585	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺))
29		ablfac1.s	. . 3 ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
30	28, 29	fmptd 7066	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
31	4	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝐺 ∈ Abel)
32	30	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑆:𝐴⟶(SubGrp‘𝐺))
33		simpr1 1196	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝐴)
34	32, 33	ffvelcdmd 7037	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ∈ (SubGrp‘𝐺))
35		simpr2 1197	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝐴)
36	32, 35	ffvelcdmd 7037	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑏) ∈ (SubGrp‘𝐺))
37	1, 31, 34, 36	ablcntzd 19832	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑏)))
38		id 22	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → 𝑝 = 𝑎)
39		oveq1 7374	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → (𝑝 pCnt (♯‘𝐵)) = (𝑎 pCnt (♯‘𝐵)))
40	38, 39	oveq12d 7385	. . . . . . . . 9 ⊢ (𝑝 = 𝑎 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵))))
41	40	breq2d 5097	. . . . . . . 8 ⊢ (𝑝 = 𝑎 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))))
42	41	rabbidv 3396	. . . . . . 7 ⊢ (𝑝 = 𝑎 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
43	15	fvexi 6854	. . . . . . . 8 ⊢ 𝐵 ∈ V
44	43	rabex 5280	. . . . . . 7 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
45	42, 29, 44	fvmpt3i 6953	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
46	45	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
47		eqimss 3980	. . . . 5 ⊢ ((𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
48	46, 47	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
49	4	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐺 ∈ Abel)
50		eqid 2736	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
51	50	subgacs 19136	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
52		acsmre 17618	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
53	49, 5, 51, 52	4syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
54		df-ima 5644	. . . . . . 7 ⊢ (𝑆 “ (𝐴 ∖ {𝑎})) = ran (𝑆 ↾ (𝐴 ∖ {𝑎}))
55	7	sselda 3921	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℙ)
56	55	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℙ)
57	21	ad3antrrr 731	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℕ)
58		pcdvds 16835	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
59	56, 57, 58	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
60	7	ad3antrrr 731	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝐴 ⊆ ℙ)
61		eldifi 4071	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ∈ 𝐴)
62	61	ad2antlr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ 𝐴)
63	60, 62	sseldd 3922	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℙ)
64		pcdvds 16835	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
65	63, 57, 64	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
66		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎↑(𝑎 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵)))
67		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) = ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))
68	15, 26, 29, 4, 18, 7, 66, 67	ablfac1lem 20045	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1 ∧ (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))))
69	68	simp1d 1143	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ))
70	69	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ)
71	70	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ)
72	71	nnzd 12550	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ)
73	63, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℕ)
74	63, 57	pccld 16821	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)
75	73, 74	nnexpcld 14207	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ)
76	75	nnzd 12550	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ)
77	57	nnzd 12550	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ)
78		eldifsni 4735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ≠ 𝑎)
79	78	ad2antlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ≠ 𝑎)
80	79	necomd 2987	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ≠ 𝑝)
81		prmrp 16682	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
82	56, 63, 81	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
83	80, 82	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 gcd 𝑝) = 1)
84		prmz 16644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℙ → 𝑎 ∈ ℤ)
85	56, 84	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℤ)
86		prmz 16644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
87	63, 86	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℤ)
88	56, 57	pccld 16821	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 pCnt (♯‘𝐵)) ∈ ℕ₀)
89		rpexp12i 16694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ ((𝑎 pCnt (♯‘𝐵)) ∈ ℕ₀ ∧ (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1))
90	85, 87, 88, 74, 89	syl112anc 1377	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1))
91	83, 90	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1)
92		coprmdvds2 16623	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)))
93	72, 76, 77, 91, 92	syl31anc 1376	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)))
94	59, 65, 93	mp2and 700	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵))
95	68	simp3d 1145	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
96	95	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
97	94, 96	breqtrd 5111	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
98	69	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)
99	98	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)
100	99	nnzd 12550	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ)
101	71	nnne0d 12227	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)
102		dvdscmulr 16253	. . . . . . . . . . . . . 14 ⊢ (((𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
103	76, 100, 72, 101, 102	syl112anc 1377	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
104	97, 103	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))
105	15, 26	odcl 19511	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ₀)
106	105	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ₀)
107	106	nn0zd 12549	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
108		dvdstr 16263	. . . . . . . . . . . . 13 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
109	107, 76, 100, 108	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
110	104, 109	mpan2d 695	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
111	110	ss2rabdv 4015	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
112	44	elpw 4545	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
113	111, 112	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
114	29	reseq1i 5940	. . . . . . . . . 10 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎}))
115		difss 4076	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑎}) ⊆ 𝐴
116		resmpt 6002	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝑎}) ⊆ 𝐴 → ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}))
117	115, 116	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
118	114, 117	eqtri 2759	. . . . . . . . 9 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
119	113, 118	fmptd 7066	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 ↾ (𝐴 ∖ {𝑎})):(𝐴 ∖ {𝑎})⟶𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
120	119	frnd 6676	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ran (𝑆 ↾ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
121	54, 120	eqsstrid 3960	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
122		sspwuni 5042	. . . . . 6 ⊢ ((𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
123	121, 122	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
124	98	nnzd 12550	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ)
125	26, 15	oddvdssubg 19830	. . . . . 6 ⊢ ((𝐺 ∈ Abel ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺))
126	49, 124, 125	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺))
127	3	mrcsscl 17586	. . . . 5 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∧ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
128	53, 123, 126, 127	syl3anc 1374	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
129		ss2in 4185	. . . 4 ⊢ (((𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∧ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}))
130	48, 128, 129	syl2anc 585	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}))
131		eqid 2736	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}
132		eqid 2736	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}
133	68	simp2d 1144	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1)
134		eqid 2736	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
135	15, 26, 131, 132, 49, 70, 98, 133, 95, 2, 134	ablfacrp 20043	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0_g‘𝐺)} ∧ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} (LSSum‘𝐺){𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = 𝐵))
136	135	simpld 494	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0_g‘𝐺)})
137	130, 136	sseqtrd 3958	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ {(0_g‘𝐺)})
138	1, 2, 3, 6, 10, 30, 37, 137	dmdprdd 19976	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 {crab 3389 Vcvv 3429 ∖ cdif 3886 ∩ cin 3888 ⊆ wss 3889 ∅c0 4273 𝒫 cpw 4541 {csn 4567 ∪ cuni 4850 class class class wbr 5085 ↦ cmpt 5166 dom cdm 5631 ran crn 5632 ↾ cres 5633 “ cima 5634 ⟶wf 6494 ‘cfv 6498 (class class class)co 7367 Fincfn 8893 0cc0 11038 1c1 11039 · cmul 11043 / cdiv 11807 ℕcn 12174 ℕ₀cn0 12437 ℤcz 12524 ↑cexp 14023 ♯chash 14292 ∥ cdvds 16221 gcd cgcd 16463 ℙcprime 16640 pCnt cpc 16807 Basecbs 17179 0_gc0g 17402 Moorecmre 17544 mrClscmrc 17545 ACScacs 17547 Grpcgrp 18909 SubGrpcsubg 19096 Cntzccntz 19290 odcod 19499 LSSumclsm 19609 Abelcabl 19756 DProd cdprd 19970

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-iin 4936 df-disj 5053 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-oadd 8409 df-omul 8410 df-er 8643 df-ec 8645 df-qs 8649 df-map 8775 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-sup 9355 df-inf 9356 df-oi 9425 df-card 9863 df-acn 9866 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-z 12525 df-uz 12789 df-q 12899 df-rp 12943 df-fz 13462 df-fzo 13609 df-fl 13751 df-mod 13829 df-seq 13964 df-exp 14024 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-sum 15649 df-dvds 16222 df-gcd 16464 df-prm 16641 df-pc 16808 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-0g 17404 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-submnd 18752 df-grp 18912 df-minusg 18913 df-sbg 18914 df-mulg 19044 df-subg 19099 df-eqg 19101 df-cntz 19292 df-od 19503 df-lsm 19611 df-cmn 19757 df-abl 19758 df-dprd 19972

This theorem is referenced by: ablfac1c 20048 ablfac1eu 20050 ablfaclem2 20063 ablfaclem3 20064

W3C validator