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 20058

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 19771	. . 3 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		ablfac1.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℙ)
8		prmex 16701	. . . 4 ⊢ ℙ ∈ V
9	8	ssex 5296	. . 3 ⊢ (𝐴 ⊆ ℙ → 𝐴 ∈ V)
10	7, 9	syl 17	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
11	4	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐺 ∈ Abel)
12	7	sselda 3963	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℙ)
13		prmnn 16698	. . . . . . 7 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
14	12, 13	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℕ)
15		ablfac1.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐺)
16	15	grpbn0 18954	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
17	6, 16	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ≠ ∅)
18		ablfac1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ Fin)
19		hashnncl 14389	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
21	17, 20	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
22	21	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (♯‘𝐵) ∈ ℕ)
23	12, 22	pccld 16875	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)
24	14, 23	nnexpcld 14268	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ)
25	24	nnzd 12620	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ)
26		ablfac1.o	. . . . 5 ⊢ 𝑂 = (od‘𝐺)
27	26, 15	oddvdssubg 19841	. . . 4 ⊢ ((𝐺 ∈ Abel ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺))
28	11, 25, 27	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ (SubGrp‘𝐺))
29		ablfac1.s	. . 3 ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
30	28, 29	fmptd 7109	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
31	4	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝐺 ∈ Abel)
32	30	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑆:𝐴⟶(SubGrp‘𝐺))
33		simpr1 1195	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝐴)
34	32, 33	ffvelcdmd 7080	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ∈ (SubGrp‘𝐺))
35		simpr2 1196	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝐴)
36	32, 35	ffvelcdmd 7080	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑏) ∈ (SubGrp‘𝐺))
37	1, 31, 34, 36	ablcntzd 19843	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑏)))
38		id 22	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → 𝑝 = 𝑎)
39		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → (𝑝 pCnt (♯‘𝐵)) = (𝑎 pCnt (♯‘𝐵)))
40	38, 39	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑝 = 𝑎 → (𝑝↑(𝑝 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵))))
41	40	breq2d 5136	. . . . . . . 8 ⊢ (𝑝 = 𝑎 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))))
42	41	rabbidv 3428	. . . . . . 7 ⊢ (𝑝 = 𝑎 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
43	15	fvexi 6895	. . . . . . . 8 ⊢ 𝐵 ∈ V
44	43	rabex 5314	. . . . . . 7 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
45	42, 29, 44	fvmpt3i 6996	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
46	45	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))})
47		eqimss 4022	. . . . 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 19149	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
52		acsmre 17669	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
53	49, 5, 51, 52	4syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
54		df-ima 5672	. . . . . . 7 ⊢ (𝑆 “ (𝐴 ∖ {𝑎})) = ran (𝑆 ↾ (𝐴 ∖ {𝑎}))
55	7	sselda 3963	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℙ)
56	55	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℙ)
57	21	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℕ)
58		pcdvds 16889	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
59	56, 57, 58	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
60	7	ad3antrrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝐴 ⊆ ℙ)
61		eldifi 4111	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ∈ 𝐴)
62	61	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ 𝐴)
63	60, 62	sseldd 3964	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℙ)
64		pcdvds 16889	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (♯‘𝐵) ∈ ℕ) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
65	63, 57, 64	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵))
66		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎↑(𝑎 pCnt (♯‘𝐵))) = (𝑎↑(𝑎 pCnt (♯‘𝐵)))
67		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) = ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))
68	15, 26, 29, 4, 18, 7, 66, 67	ablfac1lem 20056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1 ∧ (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))))
69	68	simp1d 1142	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ))
70	69	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ)
71	70	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℕ)
72	71	nnzd 12620	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ)
73	63, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℕ)
74	63, 57	pccld 16875	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)
75	73, 74	nnexpcld 14268	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℕ)
76	75	nnzd 12620	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ)
77	57	nnzd 12620	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ)
78		eldifsni 4771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ≠ 𝑎)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ≠ 𝑎)
80	79	necomd 2988	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ≠ 𝑝)
81		prmrp 16736	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
82	56, 63, 81	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
83	80, 82	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 gcd 𝑝) = 1)
84		prmz 16699	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℙ → 𝑎 ∈ ℤ)
85	56, 84	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℤ)
86		prmz 16699	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
87	63, 86	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℤ)
88	56, 57	pccld 16875	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 pCnt (♯‘𝐵)) ∈ ℕ₀)
89		rpexp12i 16748	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ ((𝑎 pCnt (♯‘𝐵)) ∈ ℕ₀ ∧ (𝑝 pCnt (♯‘𝐵)) ∈ ℕ₀)) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1))
90	85, 87, 88, 74, 89	syl112anc 1376	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1))
91	83, 90	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1)
92		coprmdvds2 16678	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd (𝑝↑(𝑝 pCnt (♯‘𝐵)))) = 1) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)))
93	72, 76, 77, 91, 92	syl31anc 1375	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∥ (♯‘𝐵) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ (♯‘𝐵)) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵)))
94	59, 65, 93	mp2and 699	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ (♯‘𝐵))
95	68	simp3d 1144	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
96	95	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) = ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
97	94, 96	breqtrd 5150	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
98	69	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)
99	98	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℕ)
100	99	nnzd 12620	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ)
101	71	nnne0d 12295	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)
102		dvdscmulr 16309	. . . . . . . . . . . . . 14 ⊢ (((𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ ∧ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) ∈ ℤ ∧ (𝑎↑(𝑎 pCnt (♯‘𝐵))) ≠ 0)) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
103	76, 100, 72, 101, 102	syl112anc 1376	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (♯‘𝐵))) · (𝑝↑(𝑝 pCnt (♯‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (♯‘𝐵))) · ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
104	97, 103	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))))
105	15, 26	odcl 19522	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ₀)
106	105	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ₀)
107	106	nn0zd 12619	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
108		dvdstr 16318	. . . . . . . . . . . . 13 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∈ ℤ ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
109	107, 76, 100, 108	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (♯‘𝐵))) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
110	104, 109	mpan2d 694	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵))) → (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))))
111	110	ss2rabdv 4056	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
112	44	elpw 4584	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
113	111, 112	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
114	29	reseq1i 5967	. . . . . . . . . 10 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎}))
115		difss 4116	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑎}) ⊆ 𝐴
116		resmpt 6029	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝑎}) ⊆ 𝐴 → ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}))
117	115, 116	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
118	114, 117	eqtri 2759	. . . . . . . . 9 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
119	113, 118	fmptd 7109	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 ↾ (𝐴 ∖ {𝑎})):(𝐴 ∖ {𝑎})⟶𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
120	119	frnd 6719	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ran (𝑆 ↾ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
121	54, 120	eqsstrid 4002	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
122		sspwuni 5081	. . . . . 6 ⊢ ((𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ↔ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
123	121, 122	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
124	98	nnzd 12620	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ)
125	26, 15	oddvdssubg 19841	. . . . . 6 ⊢ ((𝐺 ∈ Abel ∧ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵)))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺))
126	49, 124, 125	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺))
127	3	mrcsscl 17637	. . . . 5 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∧ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
128	53, 123, 126, 127	syl3anc 1373	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))})
129		ss2in 4225	. . . 4 ⊢ (((𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∧ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}))
130	48, 128, 129	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}))
131		eqid 2736	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))}
132		eqid 2736	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}
133	68	simp2d 1143	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (♯‘𝐵))) gcd ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))) = 1)
134		eqid 2736	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
135	15, 26, 131, 132, 49, 70, 98, 133, 95, 2, 134	ablfacrp 20054	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0_g‘𝐺)} ∧ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} (LSSum‘𝐺){𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = 𝐵))
136	135	simpld 494	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (♯‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((♯‘𝐵) / (𝑎↑(𝑎 pCnt (♯‘𝐵))))}) = {(0_g‘𝐺)})
137	130, 136	sseqtrd 4000	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ {(0_g‘𝐺)})
138	1, 2, 3, 6, 10, 30, 37, 137	dmdprdd 19987	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 {crab 3420 Vcvv 3464 ∖ cdif 3928 ∩ cin 3930 ⊆ wss 3931 ∅c0 4313 𝒫 cpw 4580 {csn 4606 ∪ cuni 4888 class class class wbr 5124 ↦ cmpt 5206 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 Fincfn 8964 0cc0 11134 1c1 11135 · cmul 11139 / cdiv 11899 ℕcn 12245 ℕ₀cn0 12506 ℤcz 12593 ↑cexp 14084 ♯chash 14353 ∥ cdvds 16277 gcd cgcd 16518 ℙcprime 16695 pCnt cpc 16861 Basecbs 17233 0_gc0g 17458 Moorecmre 17599 mrClscmrc 17600 ACScacs 17602 Grpcgrp 18921 SubGrpcsubg 19108 Cntzccntz 19303 odcod 19510 LSSumclsm 19620 Abelcabl 19767 DProd cdprd 19981

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 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-inf2 9660 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

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 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-disj 5092 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-oadd 8489 df-omul 8490 df-er 8724 df-ec 8726 df-qs 8730 df-map 8847 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-sup 9459 df-inf 9460 df-oi 9529 df-card 9958 df-acn 9961 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-n0 12507 df-z 12594 df-uz 12858 df-q 12970 df-rp 13014 df-fz 13530 df-fzo 13677 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-hash 14354 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-clim 15509 df-sum 15708 df-dvds 16278 df-gcd 16519 df-prm 16696 df-pc 16862 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-0g 17460 df-mre 17603 df-mrc 17604 df-acs 17606 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-submnd 18767 df-grp 18924 df-minusg 18925 df-sbg 18926 df-mulg 19056 df-subg 19111 df-eqg 19113 df-cntz 19305 df-od 19514 df-lsm 19622 df-cmn 19768 df-abl 19769 df-dprd 19983

This theorem is referenced by: ablfac1c 20059 ablfac1eu 20061 ablfaclem2 20074 ablfaclem3 20075

W3C validator