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 18390

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 2621	. 2 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2621	. 2 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		eqid 2621	. 2 ⊢ (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
4		ablfac1.g	. . 3 ⊢ (𝜑 → 𝐺 ∈ Abel)
5		ablgrp 18119	. . 3 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
6	4, 5	syl 17	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		ablfac1.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ ℙ)
8		nnex 10970	. . . . 5 ⊢ ℕ ∈ V
9		prmnn 15312	. . . . . 6 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
10	9	ssriv 3587	. . . . 5 ⊢ ℙ ⊆ ℕ
11	8, 10	ssexi 4763	. . . 4 ⊢ ℙ ∈ V
12	11	ssex 4762	. . 3 ⊢ (𝐴 ⊆ ℙ → 𝐴 ∈ V)
13	7, 12	syl 17	. 2 ⊢ (𝜑 → 𝐴 ∈ V)
14	4	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝐺 ∈ Abel)
15	7	sselda 3583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℙ)
16	15, 9	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ ℕ)
17		ablfac1.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐺)
18	17	grpbn0 17372	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
19	6, 18	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ≠ ∅)
20		ablfac1.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ Fin)
21		hashnncl 13097	. . . . . . . . . 10 ⊢ (𝐵 ∈ Fin → ((#‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
22	20, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((#‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
23	19, 22	mpbird 247	. . . . . . . 8 ⊢ (𝜑 → (#‘𝐵) ∈ ℕ)
24	23	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (#‘𝐵) ∈ ℕ)
25	15, 24	pccld 15479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝 pCnt (#‘𝐵)) ∈ ℕ₀)
26	16, 25	nnexpcld 12970	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (#‘𝐵))) ∈ ℕ)
27	26	nnzd 11425	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → (𝑝↑(𝑝 pCnt (#‘𝐵))) ∈ ℤ)
28		ablfac1.o	. . . . 5 ⊢ 𝑂 = (od‘𝐺)
29	28, 17	oddvdssubg 18179	. . . 4 ⊢ ((𝐺 ∈ Abel ∧ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ (SubGrp‘𝐺))
30	14, 27, 29	syl2anc 692	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ (SubGrp‘𝐺))
31		ablfac1.s	. . 3 ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))})
32	30, 31	fmptd 6340	. 2 ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺))
33	4	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝐺 ∈ Abel)
34	32	adantr 481	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑆:𝐴⟶(SubGrp‘𝐺))
35		simpr1 1065	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝐴)
36	34, 35	ffvelrnd 6316	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ∈ (SubGrp‘𝐺))
37		simpr2 1066	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝐴)
38	34, 37	ffvelrnd 6316	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑏) ∈ (SubGrp‘𝐺))
39	1, 33, 36, 38	ablcntzd 18181	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏)) → (𝑆‘𝑎) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑏)))
40		id 22	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → 𝑝 = 𝑎)
41		oveq1 6611	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → (𝑝 pCnt (#‘𝐵)) = (𝑎 pCnt (#‘𝐵)))
42	40, 41	oveq12d 6622	. . . . . . . . 9 ⊢ (𝑝 = 𝑎 → (𝑝↑(𝑝 pCnt (#‘𝐵))) = (𝑎↑(𝑎 pCnt (#‘𝐵))))
43	42	breq2d 4625	. . . . . . . 8 ⊢ (𝑝 = 𝑎 → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵))) ↔ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))))
44	43	rabbidv 3177	. . . . . . 7 ⊢ (𝑝 = 𝑎 → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))})
45		fvex 6158	. . . . . . . . 9 ⊢ (Base‘𝐺) ∈ V
46	17, 45	eqeltri 2694	. . . . . . . 8 ⊢ 𝐵 ∈ V
47	46	rabex 4773	. . . . . . 7 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ V
48	44, 31, 47	fvmpt3i 6244	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))})
49	48	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))})
50		eqimss 3636	. . . . 5 ⊢ ((𝑆‘𝑎) = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))} → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))})
51	49, 50	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))})
52	4	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐺 ∈ Abel)
53		eqid 2621	. . . . . . 7 ⊢ (Base‘𝐺) = (Base‘𝐺)
54	53	subgacs 17550	. . . . . 6 ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)))
55		acsmre 16234	. . . . . 6 ⊢ ((SubGrp‘𝐺) ∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
56	52, 5, 54, 55	4syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)))
57		df-ima 5087	. . . . . . 7 ⊢ (𝑆 “ (𝐴 ∖ {𝑎})) = ran (𝑆 ↾ (𝐴 ∖ {𝑎}))
58	7	sselda 3583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℙ)
59	58	ad2antrr 761	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℙ)
60	23	ad3antrrr 765	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (#‘𝐵) ∈ ℕ)
61		pcdvds 15492	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℙ ∧ (#‘𝐵) ∈ ℕ) → (𝑎↑(𝑎 pCnt (#‘𝐵))) ∥ (#‘𝐵))
62	59, 60, 61	syl2anc 692	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (#‘𝐵))) ∥ (#‘𝐵))
63	7	ad3antrrr 765	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝐴 ⊆ ℙ)
64		eldifi 3710	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ∈ 𝐴)
65	64	ad2antlr 762	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ 𝐴)
66	63, 65	sseldd 3584	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℙ)
67		pcdvds 15492	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℙ ∧ (#‘𝐵) ∈ ℕ) → (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ (#‘𝐵))
68	66, 60, 67	syl2anc 692	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ (#‘𝐵))
69		eqid 2621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎↑(𝑎 pCnt (#‘𝐵))) = (𝑎↑(𝑎 pCnt (#‘𝐵)))
70		eqid 2621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) = ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))
71	17, 28, 31, 4, 20, 7, 69, 70	ablfac1lem 18388	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (((𝑎↑(𝑎 pCnt (#‘𝐵))) ∈ ℕ ∧ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℕ) ∧ ((𝑎↑(𝑎 pCnt (#‘𝐵))) gcd ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))) = 1 ∧ (#‘𝐵) = ((𝑎↑(𝑎 pCnt (#‘𝐵))) · ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))))))
72	71	simp1d 1071	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (#‘𝐵))) ∈ ℕ ∧ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℕ))
73	72	simpld 475	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎↑(𝑎 pCnt (#‘𝐵))) ∈ ℕ)
74	73	ad2antrr 761	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (#‘𝐵))) ∈ ℕ)
75	74	nnzd 11425	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (#‘𝐵))) ∈ ℤ)
76	66, 9	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℕ)
77	66, 60	pccld 15479	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝 pCnt (#‘𝐵)) ∈ ℕ₀)
78	76, 77	nnexpcld 12970	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (#‘𝐵))) ∈ ℕ)
79	78	nnzd 11425	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (#‘𝐵))) ∈ ℤ)
80	60	nnzd 11425	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (#‘𝐵) ∈ ℤ)
81		eldifsni 4289	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (𝐴 ∖ {𝑎}) → 𝑝 ≠ 𝑎)
82	81	ad2antlr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ≠ 𝑎)
83	82	necomd 2845	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ≠ 𝑝)
84		prmrp 15348	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ℙ ∧ 𝑝 ∈ ℙ) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
85	59, 66, 84	syl2anc 692	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 ↔ 𝑎 ≠ 𝑝))
86	83, 85	mpbird 247	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 gcd 𝑝) = 1)
87		prmz 15313	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℙ → 𝑎 ∈ ℤ)
88	59, 87	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑎 ∈ ℤ)
89		prmz 15313	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
90	66, 89	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → 𝑝 ∈ ℤ)
91	59, 60	pccld 15479	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎 pCnt (#‘𝐵)) ∈ ℕ₀)
92		rpexp12i 15358	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ ((𝑎 pCnt (#‘𝐵)) ∈ ℕ₀ ∧ (𝑝 pCnt (#‘𝐵)) ∈ ℕ₀)) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (#‘𝐵))) gcd (𝑝↑(𝑝 pCnt (#‘𝐵)))) = 1))
93	88, 90, 91, 77, 92	syl112anc 1327	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎 gcd 𝑝) = 1 → ((𝑎↑(𝑎 pCnt (#‘𝐵))) gcd (𝑝↑(𝑝 pCnt (#‘𝐵)))) = 1))
94	86, 93	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (#‘𝐵))) gcd (𝑝↑(𝑝 pCnt (#‘𝐵)))) = 1)
95		coprmdvds2 15292	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎↑(𝑎 pCnt (#‘𝐵))) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∈ ℤ ∧ (#‘𝐵) ∈ ℤ) ∧ ((𝑎↑(𝑎 pCnt (#‘𝐵))) gcd (𝑝↑(𝑝 pCnt (#‘𝐵)))) = 1) → (((𝑎↑(𝑎 pCnt (#‘𝐵))) ∥ (#‘𝐵) ∧ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ (#‘𝐵)) → ((𝑎↑(𝑎 pCnt (#‘𝐵))) · (𝑝↑(𝑝 pCnt (#‘𝐵)))) ∥ (#‘𝐵)))
96	75, 79, 80, 94, 95	syl31anc 1326	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (#‘𝐵))) ∥ (#‘𝐵) ∧ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ (#‘𝐵)) → ((𝑎↑(𝑎 pCnt (#‘𝐵))) · (𝑝↑(𝑝 pCnt (#‘𝐵)))) ∥ (#‘𝐵)))
97	62, 68, 96	mp2and 714	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (#‘𝐵))) · (𝑝↑(𝑝 pCnt (#‘𝐵)))) ∥ (#‘𝐵))
98	71	simp3d 1073	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (#‘𝐵) = ((𝑎↑(𝑎 pCnt (#‘𝐵))) · ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))))
99	98	ad2antrr 761	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (#‘𝐵) = ((𝑎↑(𝑎 pCnt (#‘𝐵))) · ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))))
100	97, 99	breqtrd 4639	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑎↑(𝑎 pCnt (#‘𝐵))) · (𝑝↑(𝑝 pCnt (#‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (#‘𝐵))) · ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))))
101	72	simprd 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℕ)
102	101	ad2antrr 761	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℕ)
103	102	nnzd 11425	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℤ)
104	74	nnne0d 11009	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑎↑(𝑎 pCnt (#‘𝐵))) ≠ 0)
105		dvdscmulr 14934	. . . . . . . . . . . . . 14 ⊢ (((𝑝↑(𝑝 pCnt (#‘𝐵))) ∈ ℤ ∧ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℤ ∧ ((𝑎↑(𝑎 pCnt (#‘𝐵))) ∈ ℤ ∧ (𝑎↑(𝑎 pCnt (#‘𝐵))) ≠ 0)) → (((𝑎↑(𝑎 pCnt (#‘𝐵))) · (𝑝↑(𝑝 pCnt (#‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (#‘𝐵))) · ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))))
106	79, 103, 75, 104, 105	syl112anc 1327	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑎↑(𝑎 pCnt (#‘𝐵))) · (𝑝↑(𝑝 pCnt (#‘𝐵)))) ∥ ((𝑎↑(𝑎 pCnt (#‘𝐵))) · ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))) ↔ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))))
107	100, 106	mpbid 222	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))))
108	17, 28	odcl 17876	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐵 → (𝑂‘𝑥) ∈ ℕ₀)
109	108	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℕ₀)
110	109	nn0zd 11424	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (𝑂‘𝑥) ∈ ℤ)
111		dvdstr 14942	. . . . . . . . . . . . 13 ⊢ (((𝑂‘𝑥) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∈ ℤ ∧ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℤ) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))) → (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))))
112	110, 79, 103, 111	syl3anc 1323	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → (((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∧ (𝑝↑(𝑝 pCnt (#‘𝐵))) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))) → (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))))
113	107, 112	mpan2d 709	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) ∧ 𝑥 ∈ 𝐵) → ((𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵))) → (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))))
114	113	ss2rabdv 3662	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
115	47	elpw 4136	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))} ↔ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
116	114, 115	sylibr 224	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑝 ∈ (𝐴 ∖ {𝑎})) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
117	31	reseq1i 5352	. . . . . . . . . 10 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}) ↾ (𝐴 ∖ {𝑎}))
118		difss 3715	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑎}) ⊆ 𝐴
119		resmpt 5408	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ {𝑎}) ⊆ 𝐴 → ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}))
120	118, 119	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))}) ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))})
121	117, 120	eqtri 2643	. . . . . . . . 9 ⊢ (𝑆 ↾ (𝐴 ∖ {𝑎})) = (𝑝 ∈ (𝐴 ∖ {𝑎}) ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))})
122	116, 121	fmptd 6340	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 ↾ (𝐴 ∖ {𝑎})):(𝐴 ∖ {𝑎})⟶𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
123		frn 6010	. . . . . . . 8 ⊢ ((𝑆 ↾ (𝐴 ∖ {𝑎})):(𝐴 ∖ {𝑎})⟶𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))} → ran (𝑆 ↾ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
124	122, 123	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ran (𝑆 ↾ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
125	57, 124	syl5eqss 3628	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
126		sspwuni 4577	. . . . . 6 ⊢ ((𝑆 “ (𝐴 ∖ {𝑎})) ⊆ 𝒫 {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))} ↔ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
127	125, 126	sylib 208	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
128	101	nnzd 11425	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℤ)
129	28, 17	oddvdssubg 18179	. . . . . 6 ⊢ ((𝐺 ∈ Abel ∧ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵)))) ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))} ∈ (SubGrp‘𝐺))
130	52, 128, 129	syl2anc 692	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))} ∈ (SubGrp‘𝐺))
131	3	mrcsscl 16201	. . . . 5 ⊢ (((SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐴 ∖ {𝑎})) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))} ∧ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))} ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
132	56, 127, 130, 131	syl3anc 1323	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))})
133		ss2in 3818	. . . 4 ⊢ (((𝑆‘𝑎) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))} ∧ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎}))) ⊆ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))}) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))}))
134	51, 132, 133	syl2anc 692	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))}))
135		eqid 2621	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))}
136		eqid 2621	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))} = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))}
137	71	simp2d 1072	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑎↑(𝑎 pCnt (#‘𝐵))) gcd ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))) = 1)
138		eqid 2621	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
139	17, 28, 135, 136, 52, 73, 101, 137, 98, 2, 138	ablfacrp 18386	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))}) = {(0_g‘𝐺)} ∧ ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))} (LSSum‘𝐺){𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))}) = 𝐵))
140	139	simpld 475	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ({𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑎↑(𝑎 pCnt (#‘𝐵)))} ∩ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ ((#‘𝐵) / (𝑎↑(𝑎 pCnt (#‘𝐵))))}) = {(0_g‘𝐺)})
141	134, 140	sseqtrd 3620	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑆‘𝑎) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐴 ∖ {𝑎})))) ⊆ {(0_g‘𝐺)})
142	1, 2, 3, 6, 13, 32, 39, 141	dmdprdd 18319	1 ⊢ (𝜑 → 𝐺dom DProd 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1036 = wceq 1480 ∈ wcel 1987 ≠ wne 2790 {crab 2911 Vcvv 3186 ∖ cdif 3552 ∩ cin 3554 ⊆ wss 3555 ∅c0 3891 𝒫 cpw 4130 {csn 4148 ∪ cuni 4402 class class class wbr 4613 ↦ cmpt 4673 dom cdm 5074 ran crn 5075 ↾ cres 5076 “ cima 5077 ⟶wf 5843 ‘cfv 5847 (class class class)co 6604 Fincfn 7899 0cc0 9880 1c1 9881 · cmul 9885 / cdiv 10628 ℕcn 10964 ℕ₀cn0 11236 ℤcz 11321 ↑cexp 12800 #chash 13057 ∥ cdvds 14907 gcd cgcd 15140 ℙcprime 15309 pCnt cpc 15465 Basecbs 15781 0_gc0g 16021 Moorecmre 16163 mrClscmrc 16164 ACScacs 16166 Grpcgrp 17343 SubGrpcsubg 17509 Cntzccntz 17669 odcod 17865 LSSumclsm 17970 Abelcabl 18115 DProd cdprd 18313

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-8 1989 ax-9 1996 ax-10 2016 ax-11 2031 ax-12 2044 ax-13 2245 ax-ext 2601 ax-rep 4731 ax-sep 4741 ax-nul 4749 ax-pow 4803 ax-pr 4867 ax-un 6902 ax-inf2 8482 ax-cnex 9936 ax-resscn 9937 ax-1cn 9938 ax-icn 9939 ax-addcl 9940 ax-addrcl 9941 ax-mulcl 9942 ax-mulrcl 9943 ax-mulcom 9944 ax-addass 9945 ax-mulass 9946 ax-distr 9947 ax-i2m1 9948 ax-1ne0 9949 ax-1rid 9950 ax-rnegex 9951 ax-rrecex 9952 ax-cnre 9953 ax-pre-lttri 9954 ax-pre-lttrn 9955 ax-pre-ltadd 9956 ax-pre-mulgt0 9957 ax-pre-sup 9958

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-fal 1486 df-ex 1702 df-nf 1707 df-sb 1878 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2750 df-ne 2791 df-nel 2894 df-ral 2912 df-rex 2913 df-reu 2914 df-rmo 2915 df-rab 2916 df-v 3188 df-sbc 3418 df-csb 3515 df-dif 3558 df-un 3560 df-in 3562 df-ss 3569 df-pss 3571 df-nul 3892 df-if 4059 df-pw 4132 df-sn 4149 df-pr 4151 df-tp 4153 df-op 4155 df-uni 4403 df-int 4441 df-iun 4487 df-iin 4488 df-disj 4584 df-br 4614 df-opab 4674 df-mpt 4675 df-tr 4713 df-eprel 4985 df-id 4989 df-po 4995 df-so 4996 df-fr 5033 df-se 5034 df-we 5035 df-xp 5080 df-rel 5081 df-cnv 5082 df-co 5083 df-dm 5084 df-rn 5085 df-res 5086 df-ima 5087 df-pred 5639 df-ord 5685 df-on 5686 df-lim 5687 df-suc 5688 df-iota 5810 df-fun 5849 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854 df-fv 5855 df-isom 5856 df-riota 6565 df-ov 6607 df-oprab 6608 df-mpt2 6609 df-om 7013 df-1st 7113 df-2nd 7114 df-wrecs 7352 df-recs 7413 df-rdg 7451 df-1o 7505 df-2o 7506 df-oadd 7509 df-omul 7510 df-er 7687 df-ec 7689 df-qs 7693 df-map 7804 df-ixp 7853 df-en 7900 df-dom 7901 df-sdom 7902 df-fin 7903 df-sup 8292 df-inf 8293 df-oi 8359 df-card 8709 df-acn 8712 df-pnf 10020 df-mnf 10021 df-xr 10022 df-ltxr 10023 df-le 10024 df-sub 10212 df-neg 10213 df-div 10629 df-nn 10965 df-2 11023 df-3 11024 df-n0 11237 df-z 11322 df-uz 11632 df-q 11733 df-rp 11777 df-fz 12269 df-fzo 12407 df-fl 12533 df-mod 12609 df-seq 12742 df-exp 12801 df-hash 13058 df-cj 13773 df-re 13774 df-im 13775 df-sqrt 13909 df-abs 13910 df-clim 14153 df-sum 14351 df-dvds 14908 df-gcd 15141 df-prm 15310 df-pc 15466 df-ndx 15784 df-slot 15785 df-base 15786 df-sets 15787 df-ress 15788 df-plusg 15875 df-0g 16023 df-mre 16167 df-mrc 16168 df-acs 16170 df-mgm 17163 df-sgrp 17205 df-mnd 17216 df-submnd 17257 df-grp 17346 df-minusg 17347 df-sbg 17348 df-mulg 17462 df-subg 17512 df-eqg 17514 df-cntz 17671 df-od 17869 df-lsm 17972 df-cmn 18116 df-abl 18117 df-dprd 18315

This theorem is referenced by: ablfac1c 18391 ablfac1eu 18393 ablfaclem2 18406 ablfaclem3 18407

W3C validator