Theorem coe1fzgsumdlem 22209

Description: Lemma for coe1fzgsumd 22210 (induction step). (Contributed by AV, 8-Oct-2019.)

Hypotheses

Ref	Expression
coe1fzgsumd.p	⊢ 𝑃 = (Poly1‘𝑅)
coe1fzgsumd.b	⊢ 𝐵 = (Base‘𝑃)
coe1fzgsumd.r	⊢ (𝜑 → 𝑅 ∈ Ring)
coe1fzgsumd.k	⊢ (𝜑 → 𝐾 ∈ ℕ0)

Assertion

Ref	Expression
coe1fzgsumdlem	⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))))

Distinct variable groups:   𝑥,𝐵   𝑥,𝐾   𝑥,𝑚   𝑥,𝑎

Allowed substitution hints:   𝜑(𝑥,𝑚,𝑎)   𝐵(𝑚,𝑎)   𝑃(𝑥,𝑚,𝑎)   𝑅(𝑥,𝑚,𝑎)   𝐾(𝑚,𝑎)   𝑀(𝑥,𝑚,𝑎)

Proof of Theorem coe1fzgsumdlem

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ralunb 4187	. . 3 ⊢ (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 ↔ (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵))
2		nfcv 2898	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦𝑀
3		nfcsb1v 3914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑀
4		csbeq1a 3903	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → 𝑀 = ⦋𝑦 / 𝑥⦌𝑀)
5	2, 3, 4	cbvmpt 5253	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀) = (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌𝑀)
6	5	oveq2i 7425	. . . . . . . . . . . . . . 15 ⊢ (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) = (𝑃 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌𝑀))
7		coe1fzgsumd.b	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 = (Base‘𝑃)
8		eqid 2727	. . . . . . . . . . . . . . . 16 ⊢ (+g‘𝑃) = (+g‘𝑃)
9		coe1fzgsumd.r	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 ∈ Ring)
10		coe1fzgsumd.p	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑃 = (Poly1‘𝑅)
11	10	ply1ring 22153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
12	9, 11	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ Ring)
13		ringcmn 20207	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
14	12, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ CMnd)
15	14	3ad2ant3 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → 𝑃 ∈ CMnd)
16	15	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → 𝑃 ∈ CMnd)
17		simpll1 1210	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → 𝑚 ∈ Fin)
18		rspcsbela 4431	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑚 ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝐵)
19	18	expcom 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → (𝑦 ∈ 𝑚 → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝐵))
20	19	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) → (𝑦 ∈ 𝑚 → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝐵))
21	20	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (𝑦 ∈ 𝑚 → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝐵))
22	21	imp 406	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) ∧ 𝑦 ∈ 𝑚) → ⦋𝑦 / 𝑥⦌𝑀 ∈ 𝐵)
23		vex 3473	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ∈ V
24	23	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → 𝑎 ∈ V)
25		simpll2 1211	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ¬ 𝑎 ∈ 𝑚)
26		vsnid 4661	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ {𝑎}
27		rspcsbela 4431	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ {𝑎} ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ⦋𝑎 / 𝑥⦌𝑀 ∈ 𝐵)
28	26, 27	mpan 689	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵 → ⦋𝑎 / 𝑥⦌𝑀 ∈ 𝐵)
29	28	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ⦋𝑎 / 𝑥⦌𝑀 ∈ 𝐵)
30		csbeq1 3892	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑎 → ⦋𝑦 / 𝑥⦌𝑀 = ⦋𝑎 / 𝑥⦌𝑀)
31	7, 8, 16, 17, 22, 24, 25, 29, 30	gsumunsn 19906	. . . . . . . . . . . . . . 15 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (𝑃 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌𝑀)) = ((𝑃 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))
32	6, 31	eqtrid 2779	. . . . . . . . . . . . . 14 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) = ((𝑃 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))
33	2, 3, 4	cbvmpt 5253	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑚 ↦ 𝑀) = (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀)
34	33	eqcomi 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀) = (𝑥 ∈ 𝑚 ↦ 𝑀)
35	34	oveq2i 7425	. . . . . . . . . . . . . . 15 ⊢ (𝑃 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀)) = (𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))
36	35	oveq1i 7424	. . . . . . . . . . . . . 14 ⊢ ((𝑃 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀) = ((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀)
37	32, 36	eqtrdi 2783	. . . . . . . . . . . . 13 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) = ((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))
38	37	fveq2d 6895	. . . . . . . . . . . 12 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀))) = (coe1‘((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀)))
39	38	fveq1d 6893	. . . . . . . . . . 11 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = ((coe1‘((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))‘𝐾))
40	9	3ad2ant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → 𝑅 ∈ Ring)
41	40	ad2antrr 725	. . . . . . . . . . . 12 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
42		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵)
43	7, 16, 17, 42	gsummptcl 19913	. . . . . . . . . . . 12 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)) ∈ 𝐵)
44		coe1fzgsumd.k	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
45	44	3ad2ant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → 𝐾 ∈ ℕ0)
46	45	ad2antrr 725	. . . . . . . . . . . 12 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → 𝐾 ∈ ℕ0)
47		eqid 2727	. . . . . . . . . . . . 13 ⊢ (+g‘𝑅) = (+g‘𝑅)
48	10, 7, 8, 47	coe1addfv 22171	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Ring ∧ (𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)) ∈ 𝐵 ∧ ⦋𝑎 / 𝑥⦌𝑀 ∈ 𝐵) ∧ 𝐾 ∈ ℕ0) → ((coe1‘((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))‘𝐾) = (((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾)(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)))
49	41, 43, 29, 46, 48	syl31anc 1371	. . . . . . . . . . 11 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ((coe1‘((𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))(+g‘𝑃)⦋𝑎 / 𝑥⦌𝑀))‘𝐾) = (((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾)(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)))
50	39, 49	eqtrd 2767	. . . . . . . . . 10 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾)(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)))
51		oveq1 7421	. . . . . . . . . 10 ⊢ (((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))) → (((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾)(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)) = ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)))
52	50, 51	sylan9eq 2787	. . . . . . . . 9 ⊢ (((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) ∧ ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)))
53		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((coe1‘𝑀)‘𝐾)
54		nfcsb1v 3914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾)
55		csbeq1a 3903	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((coe1‘𝑀)‘𝐾) = ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾))
56	53, 54, 55	cbvmpt 5253	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)) = (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾))
57	56	oveq2i 7425	. . . . . . . . . . . 12 ⊢ (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))) = (𝑅 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾)))
58		eqid 2727	. . . . . . . . . . . . 13 ⊢ (Base‘𝑅) = (Base‘𝑅)
59		ringcmn 20207	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
60	9, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ CMnd)
61	60	3ad2ant3 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → 𝑅 ∈ CMnd)
62	61	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → 𝑅 ∈ CMnd)
63		csbfv12 6939	. . . . . . . . . . . . . . 15 ⊢ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾) = (⦋𝑦 / 𝑥⦌(coe1‘𝑀)‘⦋𝑦 / 𝑥⦌𝐾)
64		csbfv2g 6940	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌(coe1‘𝑀) = (coe1‘⦋𝑦 / 𝑥⦌𝑀))
65	64	elv 3475	. . . . . . . . . . . . . . . 16 ⊢ ⦋𝑦 / 𝑥⦌(coe1‘𝑀) = (coe1‘⦋𝑦 / 𝑥⦌𝑀)
66		csbconstg 3908	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ V → ⦋𝑦 / 𝑥⦌𝐾 = 𝐾)
67	66	elv 3475	. . . . . . . . . . . . . . . 16 ⊢ ⦋𝑦 / 𝑥⦌𝐾 = 𝐾
68	65, 67	fveq12i 6897	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑦 / 𝑥⦌(coe1‘𝑀)‘⦋𝑦 / 𝑥⦌𝐾) = ((coe1‘⦋𝑦 / 𝑥⦌𝑀)‘𝐾)
69	63, 68	eqtri 2755	. . . . . . . . . . . . . 14 ⊢ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾) = ((coe1‘⦋𝑦 / 𝑥⦌𝑀)‘𝐾)
70		eqid 2727	. . . . . . . . . . . . . . . . 17 ⊢ (coe1‘⦋𝑦 / 𝑥⦌𝑀) = (coe1‘⦋𝑦 / 𝑥⦌𝑀)
71	70, 7, 10, 58	coe1f 22117	. . . . . . . . . . . . . . . 16 ⊢ (⦋𝑦 / 𝑥⦌𝑀 ∈ 𝐵 → (coe1‘⦋𝑦 / 𝑥⦌𝑀):ℕ0⟶(Base‘𝑅))
72	22, 71	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) ∧ 𝑦 ∈ 𝑚) → (coe1‘⦋𝑦 / 𝑥⦌𝑀):ℕ0⟶(Base‘𝑅))
73	45	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) → 𝐾 ∈ ℕ0)
74	73	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) ∧ 𝑦 ∈ 𝑚) → 𝐾 ∈ ℕ0)
75	72, 74	ffvelcdmd 7089	. . . . . . . . . . . . . 14 ⊢ (((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) ∧ 𝑦 ∈ 𝑚) → ((coe1‘⦋𝑦 / 𝑥⦌𝑀)‘𝐾) ∈ (Base‘𝑅))
76	69, 75	eqeltrid 2832	. . . . . . . . . . . . 13 ⊢ (((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) ∧ 𝑦 ∈ 𝑚) → ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾) ∈ (Base‘𝑅))
77		eqid 2727	. . . . . . . . . . . . . . . 16 ⊢ (coe1‘⦋𝑎 / 𝑥⦌𝑀) = (coe1‘⦋𝑎 / 𝑥⦌𝑀)
78	77, 7, 10, 58	coe1f 22117	. . . . . . . . . . . . . . 15 ⊢ (⦋𝑎 / 𝑥⦌𝑀 ∈ 𝐵 → (coe1‘⦋𝑎 / 𝑥⦌𝑀):ℕ0⟶(Base‘𝑅))
79	29, 78	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (coe1‘⦋𝑎 / 𝑥⦌𝑀):ℕ0⟶(Base‘𝑅))
80	79, 46	ffvelcdmd 7089	. . . . . . . . . . . . 13 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾) ∈ (Base‘𝑅))
81		nfcv 2898	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝑎
82		nfcv 2898	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥coe1
83		nfcsb1v 3914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥⦋𝑎 / 𝑥⦌𝑀
84	82, 83	nffv 6901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(coe1‘⦋𝑎 / 𝑥⦌𝑀)
85		nfcv 2898	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝐾
86	84, 85	nffv 6901	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)
87		csbeq1a 3903	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑎 → 𝑀 = ⦋𝑎 / 𝑥⦌𝑀)
88	87	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑎 → (coe1‘𝑀) = (coe1‘⦋𝑎 / 𝑥⦌𝑀))
89	88	fveq1d 6893	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → ((coe1‘𝑀)‘𝐾) = ((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾))
90	81, 86, 89	csbhypf 3918	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾) = ((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾))
91	58, 47, 62, 17, 76, 24, 25, 80, 90	gsumunsn 19906	. . . . . . . . . . . 12 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (𝑅 Σg (𝑦 ∈ (𝑚 ∪ {𝑎}) ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾))) = ((𝑅 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾)))(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)))
92	57, 91	eqtrid 2779	. . . . . . . . . . 11 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))) = ((𝑅 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾)))(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)))
93	53, 54, 55	cbvmpt 5253	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)) = (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾))
94	93	eqcomi 2736	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾)) = (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))
95	94	oveq2i 7425	. . . . . . . . . . . 12 ⊢ (𝑅 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾))) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))
96	95	oveq1i 7424	. . . . . . . . . . 11 ⊢ ((𝑅 Σg (𝑦 ∈ 𝑚 ↦ ⦋𝑦 / 𝑥⦌((coe1‘𝑀)‘𝐾)))(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)) = ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾))
97	92, 96	eqtr2di 2784	. . . . . . . . . 10 ⊢ ((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))
98	97	adantr 480	. . . . . . . . 9 ⊢ (((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) ∧ ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → ((𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))(+g‘𝑅)((coe1‘⦋𝑎 / 𝑥⦌𝑀)‘𝐾)) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))
99	52, 98	eqtrd 2767	. . . . . . . 8 ⊢ (((((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) ∧ ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))
100	99	exp31 419	. . . . . . 7 ⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) → (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵 → (((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))) → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))))
101	100	com23 86	. . . . . 6 ⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) → (((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))) → (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))))
102	101	ex 412	. . . . 5 ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → (((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))) → (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))))
103	102	a2d 29	. . . 4 ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → (∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))))
104	103	imp4b 421	. . 3 ⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))))) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 ∧ ∀𝑥 ∈ {𝑎}𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))
105	1, 104	biimtrid 241	. 2 ⊢ (((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) ∧ (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))
106	105	ex 412	1 ⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  ∀wral 3056  Vcvv 3469  ⦋csb 3889   ∪ cun 3942  {csn 4624   ↦ cmpt 5225  ⟶wf 6538  ‘cfv 6542  (class class class)co 7414  Fincfn 8955  ℕ₀cn0 12494  Basecbs 17171  +_gcplusg 17224   Σ_g cgsu 17413  CMndccmn 19726  Ringcrg 20164  Poly₁cpl1 22083  coe₁cco1 22084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-ofr 7680  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-sup 9457  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-fz 13509  df-fzo 13652  df-seq 13991  df-hash 14314  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-hom 17248  df-cco 17249  df-0g 17414  df-gsum 17415  df-prds 17420  df-pws 17422  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-mhm 18731  df-submnd 18732  df-grp 18884  df-minusg 18885  df-mulg 19015  df-subg 19069  df-ghm 19159  df-cntz 19259  df-cmn 19728  df-abl 19729  df-mgp 20066  df-rng 20084  df-ur 20113  df-ring 20166  df-subrng 20472  df-subrg 20497  df-psr 21829  df-mpl 21831  df-opsr 21833  df-psr1 22086  df-ply1 22088  df-coe1 22089

This theorem is referenced by:  coe1fzgsumd  22210