dprdf1o - Metamath Proof Explorer

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

Theorem dprdf1o 20167

Description: Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.)

**Hypotheses**
Ref	Expression
dprdf1o.1	⊢ (𝜑 → 𝐺dom DProd 𝑆)
dprdf1o.2	⊢ (𝜑 → dom 𝑆 = 𝐼)
dprdf1o.3	⊢ (𝜑 → 𝐹:𝐽–1-1-onto→𝐼)

**Assertion**
Ref	Expression
dprdf1o	⊢ (𝜑 → (𝐺dom DProd (𝑆 ∘ 𝐹) ∧ (𝐺 DProd (𝑆 ∘ 𝐹)) = (𝐺 DProd 𝑆)))

Proof of Theorem dprdf1o Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2762	. . 3 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
2		eqid 2762	. . 3 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
3		eqid 2762	. . 3 ⊢ (mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺))
4		dprdf1o.1	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
5		dprdgrp 20140	. . . 4 ⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp)
6	4, 5	syl 18	. . 3 ⊢ (𝜑 → 𝐺 ∈ Grp)
7		dprdf1o.3	. . . . 5 ⊢ (𝜑 → 𝐹:𝐽–1-1-onto→𝐼)
8		f1of1 6820	. . . . 5 ⊢ (𝐹:𝐽–1-1-onto→𝐼 → 𝐹:𝐽–1-1→𝐼)
9	7, 8	syl 18	. . . 4 ⊢ (𝜑 → 𝐹:𝐽–1-1→𝐼)
10		dprdf1o.2	. . . . 5 ⊢ (𝜑 → dom 𝑆 = 𝐼)
11	4, 10	dprddomcld 20136	. . . 4 ⊢ (𝜑 → 𝐼 ∈ V)
12		f1dmex 7958	. . . 4 ⊢ ((𝐹:𝐽–1-1→𝐼 ∧ 𝐼 ∈ V) → 𝐽 ∈ V)
13	9, 11, 12	syl2anc 596	. . 3 ⊢ (𝜑 → 𝐽 ∈ V)
14	4, 10	dprdf2 20142	. . . 4 ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺))
15		f1of 6821	. . . . 5 ⊢ (𝐹:𝐽–1-1-onto→𝐼 → 𝐹:𝐽⟶𝐼)
16	7, 15	syl 18	. . . 4 ⊢ (𝜑 → 𝐹:𝐽⟶𝐼)
17		fco 6731	. . . 4 ⊢ ((𝑆:𝐼⟶(SubGrp‘𝐺) ∧ 𝐹:𝐽⟶𝐼) → (𝑆 ∘ 𝐹):𝐽⟶(SubGrp‘𝐺))
18	14, 16, 17	syl2anc 596	. . 3 ⊢ (𝜑 → (𝑆 ∘ 𝐹):𝐽⟶(SubGrp‘𝐺))
19	4	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → 𝐺dom DProd 𝑆)
20	10	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → dom 𝑆 = 𝐼)
21	16	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → 𝐹:𝐽⟶𝐼)
22		simpr1 1213	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ∈ 𝐽)
23	21, 22	ffvelcdmd 7082	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → (𝐹‘𝑥) ∈ 𝐼)
24		simpr2 1214	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → 𝑦 ∈ 𝐽)
25	21, 24	ffvelcdmd 7082	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → (𝐹‘𝑦) ∈ 𝐼)
26		simpr3 1215	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → 𝑥 ≠ 𝑦)
27	9	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → 𝐹:𝐽–1-1→𝐼)
28		f1fveq 7263	. . . . . . . 8 ⊢ ((𝐹:𝐽–1-1→𝐼 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝑥 = 𝑦))
29	27, 22, 24, 28	syl12anc 850	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝑥 = 𝑦))
30	29	necon3bid 3001	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ 𝑥 ≠ 𝑦))
31	26, 30	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → (𝐹‘𝑥) ≠ (𝐹‘𝑦))
32	19, 20, 23, 25, 31, 1	dprdcntz 20143	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘(𝐹‘𝑥)) ⊆ ((Cntz‘𝐺)‘(𝑆‘(𝐹‘𝑦))))
33		fvco3 6982	. . . . 5 ⊢ ((𝐹:𝐽⟶𝐼 ∧ 𝑥 ∈ 𝐽) → ((𝑆 ∘ 𝐹)‘𝑥) = (𝑆‘(𝐹‘𝑥)))
34	21, 22, 33	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → ((𝑆 ∘ 𝐹)‘𝑥) = (𝑆‘(𝐹‘𝑥)))
35		fvco3 6982	. . . . . 6 ⊢ ((𝐹:𝐽⟶𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑆 ∘ 𝐹)‘𝑦) = (𝑆‘(𝐹‘𝑦)))
36	21, 24, 35	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → ((𝑆 ∘ 𝐹)‘𝑦) = (𝑆‘(𝐹‘𝑦)))
37	36	fveq2d 6886	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → ((Cntz‘𝐺)‘((𝑆 ∘ 𝐹)‘𝑦)) = ((Cntz‘𝐺)‘(𝑆‘(𝐹‘𝑦))))
38	32, 34, 37	3sstr4d 3989	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ≠ 𝑦)) → ((𝑆 ∘ 𝐹)‘𝑥) ⊆ ((Cntz‘𝐺)‘((𝑆 ∘ 𝐹)‘𝑦)))
39	16, 33	sylan 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ((𝑆 ∘ 𝐹)‘𝑥) = (𝑆‘(𝐹‘𝑥)))
40		imaco 6251	. . . . . . . . 9 ⊢ ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥})) = (𝑆 “ (𝐹 “ (𝐽 ∖ {𝑥})))
41	7	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝐹:𝐽–1-1-onto→𝐼)
42		dff1o3 6828	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐽–1-1-onto→𝐼 ↔ (𝐹:𝐽–onto→𝐼 ∧ Fun ^◡𝐹))
43	42	simprbi 503	. . . . . . . . . . . 12 ⊢ (𝐹:𝐽–1-1-onto→𝐼 → Fun ^◡𝐹)
44		imadif 6621	. . . . . . . . . . . 12 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐽 ∖ {𝑥})) = ((𝐹 “ 𝐽) ∖ (𝐹 “ {𝑥})))
45	41, 43, 44	3syl 19	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ (𝐽 ∖ {𝑥})) = ((𝐹 “ 𝐽) ∖ (𝐹 “ {𝑥})))
46		f1ofo 6829	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐽–1-1-onto→𝐼 → 𝐹:𝐽–onto→𝐼)
47		foima 6798	. . . . . . . . . . . . 13 ⊢ (𝐹:𝐽–onto→𝐼 → (𝐹 “ 𝐽) = 𝐼)
48	41, 46, 47	3syl 19	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝐽) = 𝐼)
49		f1ofn 6822	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐽–1-1-onto→𝐼 → 𝐹 Fn 𝐽)
50	7, 49	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 Fn 𝐽)
51		fnsnfv 6961	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝐽 ∧ 𝑥 ∈ 𝐽) → {(𝐹‘𝑥)} = (𝐹 “ {𝑥}))
52	50, 51	sylan 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → {(𝐹‘𝑥)} = (𝐹 “ {𝑥}))
53	52	eqcomd 2768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ {𝑥}) = {(𝐹‘𝑥)})
54	48, 53	difeq12d 4078	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ((𝐹 “ 𝐽) ∖ (𝐹 “ {𝑥})) = (𝐼 ∖ {(𝐹‘𝑥)}))
55	45, 54	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ (𝐽 ∖ {𝑥})) = (𝐼 ∖ {(𝐹‘𝑥)}))
56	55	imaeq2d 6060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝑆 “ (𝐹 “ (𝐽 ∖ {𝑥}))) = (𝑆 “ (𝐼 ∖ {(𝐹‘𝑥)})))
57	40, 56	eqtrid 2809	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥})) = (𝑆 “ (𝐼 ∖ {(𝐹‘𝑥)})))
58	57	unieqd 4883	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ∪ ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥})) = ∪ (𝑆 “ (𝐼 ∖ {(𝐹‘𝑥)})))
59	58	fveq2d 6886	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥}))) = ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {(𝐹‘𝑥)}))))
60	39, 59	ineq12d 4170	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (((𝑆 ∘ 𝐹)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥})))) = ((𝑆‘(𝐹‘𝑥)) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {(𝐹‘𝑥)})))))
61	4	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝐺dom DProd 𝑆)
62	10	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → dom 𝑆 = 𝐼)
63	16	ffvelcdmda 7081	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹‘𝑥) ∈ 𝐼)
64	61, 62, 63, 2, 3	dprddisj 20144	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ((𝑆‘(𝐹‘𝑥)) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {(𝐹‘𝑥)})))) = {(0_g‘𝐺)})
65	60, 64	eqtrd 2797	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (((𝑆 ∘ 𝐹)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥})))) = {(0_g‘𝐺)})
66		eqimss 3992	. . . 4 ⊢ ((((𝑆 ∘ 𝐹)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥})))) = {(0_g‘𝐺)} → (((𝑆 ∘ 𝐹)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
67	65, 66	syl 18	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (((𝑆 ∘ 𝐹)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆 ∘ 𝐹) “ (𝐽 ∖ {𝑥})))) ⊆ {(0_g‘𝐺)})
68	1, 2, 3, 6, 13, 18, 38, 67	dmdprdd 20134	. 2 ⊢ (𝜑 → 𝐺dom DProd (𝑆 ∘ 𝐹))
69		rnco2 6254	. . . . . 6 ⊢ ran (𝑆 ∘ 𝐹) = (𝑆 “ ran 𝐹)
70		forn 6796	. . . . . . . . 9 ⊢ (𝐹:𝐽–onto→𝐼 → ran 𝐹 = 𝐼)
71	7, 46, 70	3syl 19	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 = 𝐼)
72	71	imaeq2d 6060	. . . . . . 7 ⊢ (𝜑 → (𝑆 “ ran 𝐹) = (𝑆 “ 𝐼))
73		ffn 6706	. . . . . . . 8 ⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → 𝑆 Fn 𝐼)
74		fnima 6666	. . . . . . . 8 ⊢ (𝑆 Fn 𝐼 → (𝑆 “ 𝐼) = ran 𝑆)
75	14, 73, 74	3syl 19	. . . . . . 7 ⊢ (𝜑 → (𝑆 “ 𝐼) = ran 𝑆)
76	72, 75	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → (𝑆 “ ran 𝐹) = ran 𝑆)
77	69, 76	eqtrid 2809	. . . . 5 ⊢ (𝜑 → ran (𝑆 ∘ 𝐹) = ran 𝑆)
78	77	unieqd 4883	. . . 4 ⊢ (𝜑 → ∪ ran (𝑆 ∘ 𝐹) = ∪ ran 𝑆)
79	78	fveq2d 6886	. . 3 ⊢ (𝜑 → ((mrCls‘(SubGrp‘𝐺))‘∪ ran (𝑆 ∘ 𝐹)) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran 𝑆))
80	3	dprdspan 20162	. . . 4 ⊢ (𝐺dom DProd (𝑆 ∘ 𝐹) → (𝐺 DProd (𝑆 ∘ 𝐹)) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran (𝑆 ∘ 𝐹)))
81	68, 80	syl 18	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑆 ∘ 𝐹)) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran (𝑆 ∘ 𝐹)))
82	3	dprdspan 20162	. . . 4 ⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran 𝑆))
83	4, 82	syl 18	. . 3 ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran 𝑆))
84	79, 81, 83	3eqtr4d 2807	. 2 ⊢ (𝜑 → (𝐺 DProd (𝑆 ∘ 𝐹)) = (𝐺 DProd 𝑆))
85	68, 84	jca 521	1 ⊢ (𝜑 → (𝐺dom DProd (𝑆 ∘ 𝐹) ∧ (𝐺 DProd (𝑆 ∘ 𝐹)) = (𝐺 DProd 𝑆)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 Vcvv 3453 ∖ cdif 3899 ∩ cin 3901 ⊆ wss 3902 {csn 4587 ∪ cuni 4870 class class class wbr 5107 ^◡ccnv 5658 dom cdm 5659 ran crn 5660 “ cima 5662 ∘ ccom 5663 Fun wfun 6531 Fn wfn 6532 ⟶wf 6533 –1-1→wf1 6534 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 (class class class)co 7417 0_gc0g 17530 mrClscmrc 17673 Grpcgrp 19063 SubGrpcsubg 19249 Cntzccntz 19448 DProd cdprd 20128

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 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 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-oi 9486 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-n0 12533 df-z 12620 df-uz 12892 df-fz 13566 df-fzo 13714 df-seq 14070 df-hash 14399 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-0g 17532 df-gsum 17533 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-mhm 18897 df-submnd 18898 df-grp 19066 df-minusg 19067 df-sbg 19068 df-mulg 19197 df-subg 19252 df-ghm 19347 df-gim 19392 df-cntz 19450 df-oppg 19479 df-cmn 19915 df-dprd 20130

This theorem is used by: dprdf1 20168 ablfaclem2 20221

W3C validator