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 20105

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 2735	. 2 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2735	. 2 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		eqid 2735	. 2 ⊢ (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
4		ablfac1.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ Abel)
5		ablgrp 19818	. . 3 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		ablfac1.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℙ)
8		prmex 16711	. . . 4 ⊢ ℙ ∈ V
9	8	ssex 5327	. . 3 ⊢ (𝐴 ⊆ ℙ → 𝐴 ∈ V)
10	7, 9	syl 17	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
11	4	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐺 ∈ Abel)
12	7	sselda 3995	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℙ)
13		prmnn 16708	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
14	12, 13	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℕ)
15		ablfac1.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐺)
16	15	grpbn0 18997	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
17	6, 16	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ≠ ∅)
18		ablfac1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ Fin)
19		hashnncl 14402	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
21	17, 20	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
22	21	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ)
23	12, 22	pccld 16884	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)
24	14, 23	nnexpcld 14281	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ)
25	24	nnzd 12638	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ)
26		ablfac1.o	. . . . 5 ⊢ 𝑂 = (od‘𝐺)
27	26, 15	oddvdssubg 19888	. . . 4 ⊢ ((𝐺 ∈ Abel ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺))
28	11, 25, 27	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺))
29		ablfac1.s	. . 3 ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
30	28, 29	fmptd 7134	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
31	4	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝐺 ∈ Abel)
32	30	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑆:𝐴⟶(SubGrp‘𝐺))
33		simpr1 1193	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝐴)
34	32, 33	ffvelcdmd 7105	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ∈ (SubGrp‘𝐺))
35		simpr2 1194	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝐴)
36	32, 35	ffvelcdmd 7105	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑏) ∈ (SubGrp‘𝐺))
37	1, 31, 34, 36	ablcntzd 19890	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑏)))
38		id 22	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → 𝑝 = 𝑎)
39		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → (𝑝 pCnt (♯‘𝐵)) = (𝑎 pCnt (♯‘𝐵)))
40	38, 39	oveq12d 7449	. . . . . . . . 9 ⊢ (𝑝 = 𝑎 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵))))
41	40	breq2d 5160	. . . . . . . 8 ⊢ (𝑝 = 𝑎 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))))
42	41	rabbidv 3441	. . . . . . 7 ⊢ (𝑝 = 𝑎 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
43	15	fvexi 6921	. . . . . . . 8 ⊢ 𝐵 ∈ V
44	43	rabex 5345	. . . . . . 7 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
45	42, 29, 44	fvmpt3i 7021	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
46	45	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
47		eqimss 4054	. . . . 5 ⊢ ((𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
48	46, 47	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
49	4	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐺 ∈ Abel)
50		eqid 2735	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
51	50	subgacs 19192	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
52		acsmre 17697	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
53	49, 5, 51, 52	4syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
54		df-ima 5702	. . . . . . 7 ⊢ (𝑆 “ (𝐴 ∖ {𝑎})) = ran (𝑆 ↾ (𝐴 ∖ {𝑎}))
55	7	sselda 3995	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℙ)
56	55	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℙ)
57	21	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℕ)
58		pcdvds 16898	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
59	56, 57, 58	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
60	7	ad3antrrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝐴 ⊆ ℙ)
61		eldifi 4141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ∈ 𝐴)
62	61	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ 𝐴)
63	60, 62	sseldd 3996	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℙ)
64		pcdvds 16898	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
65	63, 57, 64	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
66		eqid 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎↑(𝑎 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵)))
67		eqid 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) = ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))
68	15, 26, 29, 4, 18, 7, 66, 67	ablfac1lem 20103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1 ∧ (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))))
69	68	simp1d 1141	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ))
70	69	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ)
71	70	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ)
72	71	nnzd 12638	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ)
73	63, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℕ)
74	63, 57	pccld 16884	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)
75	73, 74	nnexpcld 14281	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ)
76	75	nnzd 12638	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ)
77	57	nnzd 12638	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ)
78		eldifsni 4795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ≠ 𝑎)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ≠ 𝑎)
80	79	necomd 2994	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ≠ 𝑝)
81		prmrp 16746	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
82	56, 63, 81	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
83	80, 82	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 gcd 𝑝) = 1)
84		prmz 16709	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℙ → 𝑎 ∈ ℤ)
85	56, 84	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℤ)
86		prmz 16709	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
87	63, 86	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℤ)
88	56, 57	pccld 16884	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 pCnt (♯‘𝐵)) ∈ ℕ₀)
89		rpexp12i 16758	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ ((𝑎 pCnt (♯‘𝐵)) ∈ ℕ₀ ∧ (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1))
90	85, 87, 88, 74, 89	syl112anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1))
91	83, 90	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1)
92		coprmdvds2 16688	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)))
93	72, 76, 77, 91, 92	syl31anc 1372	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)))
94	59, 65, 93	mp2and 699	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵))
95	68	simp3d 1143	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
96	95	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
97	94, 96	breqtrd 5174	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
98	69	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)
99	98	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)
100	99	nnzd 12638	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ)
101	71	nnne0d 12314	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)
102		dvdscmulr 16319	. . . . . . . . . . . . . 14 ⊢ (((𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
103	76, 100, 72, 101, 102	syl112anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
104	97, 103	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))
105	15, 26	odcl 19569	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ₀)
106	105	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ₀)
107	106	nn0zd 12637	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
108		dvdstr 16328	. . . . . . . . . . . . 13 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
109	107, 76, 100, 108	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
110	104, 109	mpan2d 694	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
111	110	ss2rabdv 4086	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
112	44	elpw 4609	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
113	111, 112	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
114	29	reseq1i 5996	. . . . . . . . . 10 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎}))
115		difss 4146	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑎}) ⊆ 𝐴
116		resmpt 6057	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝑎}) ⊆ 𝐴 → ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}))
117	115, 116	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
118	114, 117	eqtri 2763	. . . . . . . . 9 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
119	113, 118	fmptd 7134	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 ↾ (𝐴 ∖ {𝑎})):(𝐴 ∖ {𝑎})⟶𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
120	119	frnd 6745	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ran (𝑆 ↾ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
121	54, 120	eqsstrid 4044	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
122		sspwuni 5105	. . . . . 6 ⊢ ((𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
123	121, 122	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
124	98	nnzd 12638	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ)
125	26, 15	oddvdssubg 19888	. . . . . 6 ⊢ ((𝐺 ∈ Abel ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺))
126	49, 124, 125	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺))
127	3	mrcsscl 17665	. . . . 5 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∧ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
128	53, 123, 126, 127	syl3anc 1370	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
129		ss2in 4253	. . . 4 ⊢ (((𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∧ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}))
130	48, 128, 129	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}))
131		eqid 2735	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}
132		eqid 2735	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}
133	68	simp2d 1142	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1)
134		eqid 2735	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
135	15, 26, 131, 132, 49, 70, 98, 133, 95, 2, 134	ablfacrp 20101	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0_g‘𝐺)} ∧ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} (LSSum‘𝐺){𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = 𝐵))
136	135	simpld 494	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0_g‘𝐺)})
137	130, 136	sseqtrd 4036	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ {(0_g‘𝐺)})
138	1, 2, 3, 6, 10, 30, 37, 137	dmdprdd 20034	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 {crab 3433 Vcvv 3478 ∖ cdif 3960 ∩ cin 3962 ⊆ wss 3963 ∅c0 4339 𝒫 cpw 4605 {csn 4631 ∪ cuni 4912 class class class wbr 5148 ↦ cmpt 5231 dom cdm 5689 ran crn 5690 ↾ cres 5691 “ cima 5692 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 Fincfn 8984 0cc0 11153 1c1 11154 · cmul 11158 / cdiv 11918 ℕcn 12264 ℕ₀cn0 12524 ℤcz 12611 ↑cexp 14099 ♯chash 14366 ∥ cdvds 16287 gcd cgcd 16528 ℙcprime 16705 pCnt cpc 16870 Basecbs 17245 0_gc0g 17486 Moorecmre 17627 mrClscmrc 17628 ACScacs 17630 Grpcgrp 18964 SubGrpcsubg 19151 Cntzccntz 19346 odcod 19557 LSSumclsm 19667 Abelcabl 19814 DProd cdprd 20028

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-inf2 9679 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-iin 4999 df-disj 5116 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-se 5642 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-isom 6572 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-2o 8506 df-oadd 8509 df-omul 8510 df-er 8744 df-ec 8746 df-qs 8750 df-map 8867 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-sup 9480 df-inf 9481 df-oi 9548 df-card 9977 df-acn 9980 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-n0 12525 df-z 12612 df-uz 12877 df-q 12989 df-rp 13033 df-fz 13545 df-fzo 13692 df-fl 13829 df-mod 13907 df-seq 14040 df-exp 14100 df-hash 14367 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-clim 15521 df-sum 15720 df-dvds 16288 df-gcd 16529 df-prm 16706 df-pc 16871 df-sets 17198 df-slot 17216 df-ndx 17228 df-base 17246 df-ress 17275 df-plusg 17311 df-0g 17488 df-mre 17631 df-mrc 17632 df-acs 17634 df-mgm 18666 df-sgrp 18745 df-mnd 18761 df-submnd 18810 df-grp 18967 df-minusg 18968 df-sbg 18969 df-mulg 19099 df-subg 19154 df-eqg 19156 df-cntz 19348 df-od 19561 df-lsm 19669 df-cmn 19815 df-abl 19816 df-dprd 20030

This theorem is referenced by: ablfac1c 20106 ablfac1eu 20108 ablfaclem2 20121 ablfaclem3 20122

W3C validator