Theorem evlslem1 20289

Description: Lemma for evlseu 20290, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.)

Hypotheses

Ref	Expression
evlslem1.p	⊢ 𝑃 = (𝐼 mPoly 𝑅)
evlslem1.b	⊢ 𝐵 = (Base‘𝑃)
evlslem1.c	⊢ 𝐶 = (Base‘𝑆)
evlslem1.d	⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
evlslem1.t	⊢ 𝑇 = (mulGrp‘𝑆)
evlslem1.x	⊢ ↑ = (.g‘𝑇)
evlslem1.m	⊢ · = (.r‘𝑆)
evlslem1.v	⊢ 𝑉 = (𝐼 mVar 𝑅)
evlslem1.e	⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
evlslem1.i	⊢ (𝜑 → 𝐼 ∈ V)
evlslem1.r	⊢ (𝜑 → 𝑅 ∈ CRing)
evlslem1.s	⊢ (𝜑 → 𝑆 ∈ CRing)
evlslem1.f	⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
evlslem1.g	⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
evlslem1.a	⊢ 𝐴 = (algSc‘𝑃)

Assertion

Ref	Expression
evlslem1	⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺))

Distinct variable groups:   𝑝,𝑏,𝐵   𝐶,𝑏,𝑝   𝜑,𝑏,𝑝   𝐹,𝑏,𝑝   𝑇,𝑏,𝑝   𝐷,𝑏,𝑝   ℎ,𝑏,𝐼,𝑝   𝑅,𝑏,ℎ,𝑝   𝐺,𝑏,𝑝   𝑃,𝑏,𝑝   𝑆,𝑏,𝑝   · ,𝑏,𝑝   ↑ ,𝑏,𝑝

Allowed substitution hints:   𝜑(ℎ)   𝐴(ℎ,𝑝,𝑏)   𝐵(ℎ)   𝐶(ℎ)   𝐷(ℎ)   𝑃(ℎ)   𝑆(ℎ)   𝑇(ℎ)   · (ℎ)   𝐸(ℎ,𝑝,𝑏)   ↑ (ℎ)   𝐹(ℎ)   𝐺(ℎ)   𝑉(ℎ,𝑝,𝑏)

Proof of Theorem evlslem1

Dummy variables 𝑥 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlslem1.b	. . 3 ⊢ 𝐵 = (Base‘𝑃)
2		eqid 2821	. . 3 ⊢ (1r‘𝑃) = (1r‘𝑃)
3		eqid 2821	. . 3 ⊢ (1r‘𝑆) = (1r‘𝑆)
4		eqid 2821	. . 3 ⊢ (.r‘𝑃) = (.r‘𝑃)
5		evlslem1.m	. . 3 ⊢ · = (.r‘𝑆)
6		evlslem1.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ V)
7		evlslem1.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CRing)
8		crngring 19302	. . . . 5 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
9	7, 8	syl 17	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
10		evlslem1.p	. . . . 5 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
11	10	mplring 20226	. . . 4 ⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring)
12	6, 9, 11	syl2anc 586	. . 3 ⊢ (𝜑 → 𝑃 ∈ Ring)
13		evlslem1.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ CRing)
14		crngring 19302	. . . 4 ⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring)
15	13, 14	syl 17	. . 3 ⊢ (𝜑 → 𝑆 ∈ Ring)
16		2fveq3 6669	. . . . . 6 ⊢ (𝑥 = (1r‘𝑅) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝐴‘(1r‘𝑅))))
17		fveq2 6664	. . . . . 6 ⊢ (𝑥 = (1r‘𝑅) → (𝐹‘𝑥) = (𝐹‘(1r‘𝑅)))
18	16, 17	eqeq12d 2837	. . . . 5 ⊢ (𝑥 = (1r‘𝑅) → ((𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥) ↔ (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅))))
19		evlslem1.d	. . . . . . . . 9 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
20		eqid 2821	. . . . . . . . 9 ⊢ (0g‘𝑅) = (0g‘𝑅)
21		eqid 2821	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
22		evlslem1.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑃)
23	6	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐼 ∈ V)
24	9	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
25		simpr 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅))
26	10, 19, 20, 21, 22, 23, 24, 25	mplascl 20270	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐴‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅))))
27	26	fveq2d 6668	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))))
28		evlslem1.c	. . . . . . . 8 ⊢ 𝐶 = (Base‘𝑆)
29		evlslem1.t	. . . . . . . 8 ⊢ 𝑇 = (mulGrp‘𝑆)
30		evlslem1.x	. . . . . . . 8 ⊢ ↑ = (.g‘𝑇)
31		evlslem1.v	. . . . . . . 8 ⊢ 𝑉 = (𝐼 mVar 𝑅)
32		evlslem1.e	. . . . . . . 8 ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
33	7	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing)
34	13	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing)
35		evlslem1.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
36	35	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
37		evlslem1.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
38	37	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼⟶𝐶)
39	19	psrbag0 20268	. . . . . . . . . 10 ⊢ (𝐼 ∈ V → (𝐼 × {0}) ∈ 𝐷)
40	6, 39	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷)
41	40	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷)
42	10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 23, 33, 34, 36, 38, 20, 41, 25	evlslem3 20287	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) = ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))))
43		0zd 11987	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℤ)
44		fvexd 6679	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ V)
45		fconstmpt 5608	. . . . . . . . . . . . . . 15 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
46	45	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0))
47	37	feqmptd 6727	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝐺‘𝑥)))
48	6, 43, 44, 46, 47	offval2 7420	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))))
49	37	ffvelrnda 6845	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ 𝐶)
50	29, 28	mgpbas 19239	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (Base‘𝑇)
51	29, 3	ringidval 19247	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝑆) = (0g‘𝑇)
52	50, 51, 30	mulg0 18225	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑥) ∈ 𝐶 → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆))
53	49, 52	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆))
54	53	mpteq2dva 5153	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))
55	48, 54	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))
56	55	oveq2d 7166	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))))
57	29	crngmgp 19299	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
58	13, 57	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ CMnd)
59		cmnmnd 18916	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ CMnd → 𝑇 ∈ Mnd)
60	58, 59	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ Mnd)
61	51	gsumz 17994	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ Mnd ∧ 𝐼 ∈ V) → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆))
62	60, 6, 61	syl2anc 586	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆))
63	56, 62	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (1r‘𝑆))
64	63	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (1r‘𝑆))
65	64	oveq2d 7166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))) = ((𝐹‘𝑥) · (1r‘𝑆)))
66	21, 28	rhmf 19472	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶)
67	35, 66	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶𝐶)
68	67	ffvelrnda 6845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ 𝐶)
69	28, 5, 3	ringridm 19316	. . . . . . . . 9 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝑥) ∈ 𝐶) → ((𝐹‘𝑥) · (1r‘𝑆)) = (𝐹‘𝑥))
70	15, 68, 69	syl2an2r 683	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (1r‘𝑆)) = (𝐹‘𝑥))
71	65, 70	eqtrd 2856	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))) = (𝐹‘𝑥))
72	27, 42, 71	3eqtrd 2860	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥))
73	72	ralrimiva 3182	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥))
74		eqid 2821	. . . . . . 7 ⊢ (1r‘𝑅) = (1r‘𝑅)
75	21, 74	ringidcl 19312	. . . . . 6 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ (Base‘𝑅))
76	9, 75	syl 17	. . . . 5 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
77	18, 73, 76	rspcdva 3624	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅)))
78	10	mplassa 20229	. . . . . . . . 9 ⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
79	6, 7, 78	syl2anc 586	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ AssAlg)
80		eqid 2821	. . . . . . . . 9 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
81	22, 80	asclrhm 20113	. . . . . . . 8 ⊢ (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
82	79, 81	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
83	10, 6, 7	mplsca 20219	. . . . . . . 8 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
84	83	oveq1d 7165	. . . . . . 7 ⊢ (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
85	82, 84	eleqtrrd 2916	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝑅 RingHom 𝑃))
86	74, 2	rhm1 19476	. . . . . 6 ⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r‘𝑅)) = (1r‘𝑃))
87	85, 86	syl 17	. . . . 5 ⊢ (𝜑 → (𝐴‘(1r‘𝑅)) = (1r‘𝑃))
88	87	fveq2d 6668	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐸‘(1r‘𝑃)))
89	74, 3	rhm1 19476	. . . . 5 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
90	35, 89	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
91	77, 88, 90	3eqtr3d 2864	. . 3 ⊢ (𝜑 → (𝐸‘(1r‘𝑃)) = (1r‘𝑆))
92		eqid 2821	. . . . 5 ⊢ (+g‘𝑃) = (+g‘𝑃)
93		eqid 2821	. . . . 5 ⊢ (+g‘𝑆) = (+g‘𝑆)
94		ringgrp 19296	. . . . . 6 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp)
95	12, 94	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Grp)
96		ringgrp 19296	. . . . . 6 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ Grp)
97	15, 96	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Grp)
98		eqid 2821	. . . . . . 7 ⊢ (0g‘𝑆) = (0g‘𝑆)
99		ringcmn 19325	. . . . . . . . 9 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
100	15, 99	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ CMnd)
101	100	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CMnd)
102		ovex 7183	. . . . . . . . 9 ⊢ (ℕ0 ↑m 𝐼) ∈ V
103	19, 102	rabex2 5229	. . . . . . . 8 ⊢ 𝐷 ∈ V
104	103	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐷 ∈ V)
105	6	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐼 ∈ V)
106	7	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑅 ∈ CRing)
107	13	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CRing)
108	35	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
109	37	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐺:𝐼⟶𝐶)
110		simpr 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵)
111	10, 1, 28, 19, 29, 30, 5, 31, 32, 105, 106, 107, 108, 109, 110	evlslem6 20288	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
112	111	simpld 497	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
113	111	simprd 498	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
114	28, 98, 101, 104, 112, 113	gsumcl 19029	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ 𝐶)
115	114, 32	fmptd 6872	. . . . 5 ⊢ (𝜑 → 𝐸:𝐵⟶𝐶)
116		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝑅) = (+g‘𝑅)
117		simplrl 775	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 ∈ 𝐵)
118		simplrr 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 ∈ 𝐵)
119	10, 1, 116, 92, 117, 118	mpladd 20216	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥(+g‘𝑃)𝑦) = (𝑥 ∘f (+g‘𝑅)𝑦))
120	119	fveq1d 6666	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏))
121		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
122	10, 21, 1, 19, 121	mplelf 20207	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥:𝐷⟶(Base‘𝑅))
123	122	ffnd 6509	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 Fn 𝐷)
124	123	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 Fn 𝐷)
125		simprr 771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
126	10, 21, 1, 19, 125	mplelf 20207	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦:𝐷⟶(Base‘𝑅))
127	126	ffnd 6509	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 Fn 𝐷)
128	127	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 Fn 𝐷)
129	103	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐷 ∈ V)
130		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷)
131		fnfvof 7417	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 Fn 𝐷 ∧ 𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏 ∈ 𝐷)) → ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
132	124, 128, 129, 130, 131	syl22anc 836	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
133	120, 132	eqtrd 2856	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
134	133	fveq2d 6668	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))))
135		rhmghm 19471	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
136	35, 135	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))
137	136	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
138	122	ffvelrnda 6845	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥‘𝑏) ∈ (Base‘𝑅))
139	126	ffvelrnda 6845	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑦‘𝑏) ∈ (Base‘𝑅))
140	21, 116, 93	ghmlin 18357	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥‘𝑏) ∈ (Base‘𝑅) ∧ (𝑦‘𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
141	137, 138, 139, 140	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
142	134, 141	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
143	142	oveq1d 7165	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
144	15	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring)
145	67	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹:(Base‘𝑅)⟶𝐶)
146	145, 138	ffvelrnd 6846	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑥‘𝑏)) ∈ 𝐶)
147	145, 139	ffvelrnd 6846	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑦‘𝑏)) ∈ 𝐶)
148	58	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd)
149	37	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶)
150	6	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ V)
151	19, 50, 30, 148, 130, 149, 150	psrbagev2 20285	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶)
152	28, 93, 5	ringdir 19311	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥‘𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
153	144, 146, 147, 151, 152	syl13anc 1368	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
154	143, 153	eqtrd 2856	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
155	154	mpteq2dva 5153	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
156	103	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ V)
157		ovexd 7185	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V)
158		ovexd 7185	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V)
159		eqidd 2822	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
160		eqidd 2822	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
161	156, 157, 158, 159, 160	offval2 7420	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
162	155, 161	eqtr4d 2859	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
163	162	oveq2d 7166	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
164	100	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CMnd)
165	6	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐼 ∈ V)
166	7	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CRing)
167	13	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CRing)
168	35	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
169	37	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺:𝐼⟶𝐶)
170	10, 1, 28, 19, 29, 30, 5, 31, 32, 165, 166, 167, 168, 169, 121	evlslem6 20288	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
171	170	simpld 497	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
172	10, 1, 28, 19, 29, 30, 5, 31, 32, 165, 166, 167, 168, 169, 125	evlslem6 20288	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
173	172	simpld 497	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
174	170	simprd 498	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
175	172	simprd 498	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
176	28, 98, 93, 164, 156, 171, 173, 174, 175	gsumadd 19037	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
177	163, 176	eqtrd 2856	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
178	95	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Grp)
179	1, 92	grpcl 18105	. . . . . . . 8 ⊢ ((𝑃 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵)
180	178, 121, 125, 179	syl3anc 1367	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵)
181		fveq1 6663	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑝‘𝑏) = ((𝑥(+g‘𝑃)𝑦)‘𝑏))
182	181	fveq2d 6668	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)))
183	182	oveq1d 7165	. . . . . . . . . 10 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
184	183	mpteq2dv 5154	. . . . . . . . 9 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
185	184	oveq2d 7166	. . . . . . . 8 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
186		ovex 7183	. . . . . . . 8 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
187	185, 32, 186	fvmpt 6762	. . . . . . 7 ⊢ ((𝑥(+g‘𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
188	180, 187	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
189		fveq1 6663	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑥 → (𝑝‘𝑏) = (𝑥‘𝑏))
190	189	fveq2d 6668	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑥 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑥‘𝑏)))
191	190	oveq1d 7165	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑥 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
192	191	mpteq2dv 5154	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
193	192	oveq2d 7166	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
194		ovex 7183	. . . . . . . . 9 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
195	193, 32, 194	fvmpt 6762	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐵 → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
196	121, 195	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
197		fveq1 6663	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑦 → (𝑝‘𝑏) = (𝑦‘𝑏))
198	197	fveq2d 6668	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑦 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑦‘𝑏)))
199	198	oveq1d 7165	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑦 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
200	199	mpteq2dv 5154	. . . . . . . . . 10 ⊢ (𝑝 = 𝑦 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
201	200	oveq2d 7166	. . . . . . . . 9 ⊢ (𝑝 = 𝑦 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
202		ovex 7183	. . . . . . . . 9 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
203	201, 32, 202	fvmpt 6762	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
204	203	ad2antll 727	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
205	196, 204	oveq12d 7168	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
206	177, 188, 205	3eqtr4d 2866	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)))
207	1, 28, 92, 93, 95, 97, 115, 206	isghmd 18361	. . . 4 ⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆))
208		eqid 2821	. . . . . . . . . . 11 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
209	208, 29	rhmmhm 19468	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
210	35, 209	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
211	210	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
212		simprll 777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥 ∈ 𝐵)
213	10, 21, 1, 19, 212	mplelf 20207	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥:𝐷⟶(Base‘𝑅))
214		simprrl 779	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑧 ∈ 𝐷)
215	213, 214	ffvelrnd 6846	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑥‘𝑧) ∈ (Base‘𝑅))
216		simprlr 778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦 ∈ 𝐵)
217	10, 21, 1, 19, 216	mplelf 20207	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦:𝐷⟶(Base‘𝑅))
218		simprrr 780	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑤 ∈ 𝐷)
219	217, 218	ffvelrnd 6846	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑦‘𝑤) ∈ (Base‘𝑅))
220	208, 21	mgpbas 19239	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
221		eqid 2821	. . . . . . . . . 10 ⊢ (.r‘𝑅) = (.r‘𝑅)
222	208, 221	mgpplusg 19237	. . . . . . . . 9 ⊢ (.r‘𝑅) = (+g‘(mulGrp‘𝑅))
223	29, 5	mgpplusg 19237	. . . . . . . . 9 ⊢ · = (+g‘𝑇)
224	220, 222, 223	mhmlin 17957	. . . . . . . 8 ⊢ ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))))
225	211, 215, 219, 224	syl3anc 1367	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))))
226	60	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → 𝑇 ∈ Mnd)
227		simprl 769	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 ∈ 𝐷)
228	19	psrbagf 20139	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ V ∧ 𝑧 ∈ 𝐷) → 𝑧:𝐼⟶ℕ0)
229	6, 227, 228	syl2an2r 683	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧:𝐼⟶ℕ0)
230	229	ffvelrnda 6845	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) ∈ ℕ0)
231		simprr 771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 ∈ 𝐷)
232	19	psrbagf 20139	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 ∈ V ∧ 𝑤 ∈ 𝐷) → 𝑤:𝐼⟶ℕ0)
233	6, 231, 232	syl2an2r 683	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤:𝐼⟶ℕ0)
234	233	ffvelrnda 6845	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) ∈ ℕ0)
235	37	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺:𝐼⟶𝐶)
236	235	ffvelrnda 6845	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ 𝐶)
237	50, 30, 223	mulgnn0dir 18251	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ Mnd ∧ ((𝑧‘𝑣) ∈ ℕ0 ∧ (𝑤‘𝑣) ∈ ℕ0 ∧ (𝐺‘𝑣) ∈ 𝐶)) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
238	226, 230, 234, 236, 237	syl13anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
239	238	mpteq2dva 5153	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))))
240	6	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐼 ∈ V)
241		ovexd 7185	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) + (𝑤‘𝑣)) ∈ V)
242		fvexd 6679	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ V)
243	229	ffnd 6509	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 Fn 𝐼)
244	233	ffnd 6509	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 Fn 𝐼)
245		inidm 4194	. . . . . . . . . . . . 13 ⊢ (𝐼 ∩ 𝐼) = 𝐼
246		eqidd 2822	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) = (𝑧‘𝑣))
247		eqidd 2822	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) = (𝑤‘𝑣))
248	243, 244, 240, 240, 245, 246, 247	offval 7410	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f + 𝑤) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) + (𝑤‘𝑣))))
249	37	feqmptd 6727	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣)))
250	249	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣)))
251	240, 241, 242, 248, 250	offval2 7420	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))))
252		ovexd 7185	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) ↑ (𝐺‘𝑣)) ∈ V)
253		ovexd 7185	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑤‘𝑣) ↑ (𝐺‘𝑣)) ∈ V)
254	37	ffnd 6509	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 Fn 𝐼)
255	254	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 Fn 𝐼)
256		eqidd 2822	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) = (𝐺‘𝑣))
257	243, 255, 240, 240, 245, 246, 256	offval 7410	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) ↑ (𝐺‘𝑣))))
258	244, 255, 240, 240, 245, 247, 256	offval 7410	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
259	240, 252, 253, 257, 258	offval2 7420	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))))
260	239, 251, 259	3eqtr4d 2866	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)))
261	260	oveq2d 7166	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))))
262	58	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑇 ∈ CMnd)
263	19, 50, 30, 51, 262, 227, 235, 240	psrbagev1 20284	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆)))
264	263	simpld 497	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶)
265	19, 50, 30, 51, 262, 231, 235, 240	psrbagev1 20284	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆)))
266	265	simpld 497	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶)
267	263	simprd 498	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆))
268	265	simprd 498	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆))
269	50, 51, 223, 262, 240, 264, 266, 267, 268	gsumadd 19037	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
270	261, 269	eqtrd 2856	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
271	270	adantrl 714	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
272	225, 271	oveq12d 7168	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
273	58	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑇 ∈ CMnd)
274	67	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶)
275	274, 215	ffvelrnd 6846	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑥‘𝑧)) ∈ 𝐶)
276	274, 219	ffvelrnd 6846	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑦‘𝑤)) ∈ 𝐶)
277	19, 50, 30, 262, 227, 235, 240	psrbagev2 20285	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶)
278	277	adantrl 714	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶)
279	19, 50, 30, 262, 231, 235, 240	psrbagev2 20285	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)
280	279	adantrl 714	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)
281	50, 223	cmn4 18920	. . . . . . 7 ⊢ ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥‘𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
282	273, 275, 276, 278, 280, 281	syl122anc 1375	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
283	272, 282	eqtrd 2856	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
284	6	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐼 ∈ V)
285	7	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ CRing)
286	13	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑆 ∈ CRing)
287	35	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆))
288	37	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐺:𝐼⟶𝐶)
289	19	psrbagaddcl 20144	. . . . . . 7 ⊢ ((𝐼 ∈ V ∧ 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (𝑧 ∘f + 𝑤) ∈ 𝐷)
290	284, 214, 218, 289	syl3anc 1367	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑧 ∘f + 𝑤) ∈ 𝐷)
291	9	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ Ring)
292	21, 221	ringcl 19305	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅))
293	291, 215, 219, 292	syl3anc 1367	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅))
294	10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 290, 293	evlslem3 20287	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))))
295	10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 214, 215	evlslem3 20287	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) = ((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))))
296	10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 284, 285, 286, 287, 288, 20, 218, 219	evlslem3 20287	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))) = ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
297	295, 296	oveq12d 7168	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
298	283, 294, 297	3eqtr4d 2866	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))))
299	10, 1, 5, 20, 19, 6, 7, 13, 207, 298	evlslem2 20286	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦)))
300	1, 2, 3, 4, 5, 12, 15, 91, 299, 28, 92, 93, 115, 206	isrhmd 19475	. 2 ⊢ (𝜑 → 𝐸 ∈ (𝑃 RingHom 𝑆))
301		ovex 7183	. . . . . 6 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
302	301, 32	fnmpti 6485	. . . . 5 ⊢ 𝐸 Fn 𝐵
303	302	a1i 11	. . . 4 ⊢ (𝜑 → 𝐸 Fn 𝐵)
304	21, 1	rhmf 19472	. . . . . 6 ⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵)
305	85, 304	syl 17	. . . . 5 ⊢ (𝜑 → 𝐴:(Base‘𝑅)⟶𝐵)
306	305	ffnd 6509	. . . 4 ⊢ (𝜑 → 𝐴 Fn (Base‘𝑅))
307	305	frnd 6515	. . . 4 ⊢ (𝜑 → ran 𝐴 ⊆ 𝐵)
308		fnco 6459	. . . 4 ⊢ ((𝐸 Fn 𝐵 ∧ 𝐴 Fn (Base‘𝑅) ∧ ran 𝐴 ⊆ 𝐵) → (𝐸 ∘ 𝐴) Fn (Base‘𝑅))
309	303, 306, 307, 308	syl3anc 1367	. . 3 ⊢ (𝜑 → (𝐸 ∘ 𝐴) Fn (Base‘𝑅))
310	67	ffnd 6509	. . 3 ⊢ (𝜑 → 𝐹 Fn (Base‘𝑅))
311		fvco2 6752	. . . . 5 ⊢ ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥)))
312	306, 311	sylan 582	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥)))
313	312, 72	eqtrd 2856	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐹‘𝑥))
314	309, 310, 313	eqfnfvd 6799	. 2 ⊢ (𝜑 → (𝐸 ∘ 𝐴) = 𝐹)
315	10, 31, 1, 6, 9	mvrf2 20266	. . . . 5 ⊢ (𝜑 → 𝑉:𝐼⟶𝐵)
316	315	ffnd 6509	. . . 4 ⊢ (𝜑 → 𝑉 Fn 𝐼)
317	315	frnd 6515	. . . 4 ⊢ (𝜑 → ran 𝑉 ⊆ 𝐵)
318		fnco 6459	. . . 4 ⊢ ((𝐸 Fn 𝐵 ∧ 𝑉 Fn 𝐼 ∧ ran 𝑉 ⊆ 𝐵) → (𝐸 ∘ 𝑉) Fn 𝐼)
319	303, 316, 317, 318	syl3anc 1367	. . 3 ⊢ (𝜑 → (𝐸 ∘ 𝑉) Fn 𝐼)
320		fvco2 6752	. . . . 5 ⊢ ((𝑉 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥)))
321	316, 320	sylan 582	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥)))
322	6	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ V)
323	7	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing)
324		simpr 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
325	31, 19, 20, 74, 322, 323, 324	mvrval 20195	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅))))
326	325	fveq2d 6668	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))))
327	13	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
328	35	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆))
329	37	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺:𝐼⟶𝐶)
330	19	psrbagsn 20269	. . . . . . . 8 ⊢ (𝐼 ∈ V → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
331	6, 330	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
332	331	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
333	76	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1r‘𝑅) ∈ (Base‘𝑅))
334	10, 1, 28, 21, 19, 29, 30, 5, 31, 32, 322, 323, 327, 328, 329, 20, 332, 333	evlslem3 20287	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) = ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))))
335	90	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
336		1nn0 11907	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
337		0nn0 11906	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
338	336, 337	ifcli 4512	. . . . . . . . . . . . 13 ⊢ if(𝑧 = 𝑥, 1, 0) ∈ ℕ0
339	338	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, 1, 0) ∈ ℕ0)
340	37	ffvelrnda 6845	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶)
341		eqidd 2822	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))
342	37	feqmptd 6727	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐼 ↦ (𝐺‘𝑧)))
343	6, 339, 340, 341, 342	offval2 7420	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))))
344		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (1 = if(𝑧 = 𝑥, 1, 0) → (1 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))
345	344	eqeq1d 2823	. . . . . . . . . . . . 13 ⊢ (1 = if(𝑧 = 𝑥, 1, 0) → ((1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
346		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑧 = 𝑥, 1, 0) → (0 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))
347	346	eqeq1d 2823	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑧 = 𝑥, 1, 0) → ((0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
348	340	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (𝐺‘𝑧) ∈ 𝐶)
349	50, 30	mulg1 18229	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑧) ∈ 𝐶 → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧))
350	348, 349	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧))
351		iftrue 4472	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧))
352	351	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧))
353	350, 352	eqtr4d 2859	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
354	50, 51, 30	mulg0 18225	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑧) ∈ 𝐶 → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
355	340, 354	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
356	355	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
357		iffalse 4475	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
358	357	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
359	356, 358	eqtr4d 2859	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
360	345, 347, 353, 359	ifbothda 4503	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
361	360	mpteq2dva 5153	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
362	343, 361	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
363	362	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
364	363	oveq2d 7166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))))
365	60	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ Mnd)
366	340	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶)
367	28, 3	ringidcl 19312	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Ring → (1r‘𝑆) ∈ 𝐶)
368	15, 367	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (1r‘𝑆) ∈ 𝐶)
369	368	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (1r‘𝑆) ∈ 𝐶)
370	366, 369	ifcld 4511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ∈ 𝐶)
371	370	fmpttd 6873	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))):𝐼⟶𝐶)
372		eldifsnneq 4716	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥)
373	372, 357	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
374	373	adantl 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
375	374, 322	suppss2 7858	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) supp (1r‘𝑆)) ⊆ {𝑥})
376	50, 51, 365, 322, 324, 371, 375	gsumpt 19076	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) = ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥))
377		fveq2 6664	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥))
378	351, 377	eqtrd 2856	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑥))
379		eqid 2821	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
380		fvex 6677	. . . . . . . . . 10 ⊢ (𝐺‘𝑥) ∈ V
381	378, 379, 380	fvmpt 6762	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐼 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥))
382	381	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥))
383	364, 376, 382	3eqtrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝐺‘𝑥))
384	335, 383	oveq12d 7168	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) = ((1r‘𝑆) · (𝐺‘𝑥)))
385	28, 5, 3	ringlidm 19315	. . . . . . 7 ⊢ ((𝑆 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐶) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥))
386	15, 49, 385	syl2an2r 683	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥))
387	384, 386	eqtrd 2856	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) = (𝐺‘𝑥))
388	326, 334, 387	3eqtrd 2860	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐺‘𝑥))
389	321, 388	eqtrd 2856	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐺‘𝑥))
390	319, 254, 389	eqfnfvd 6799	. 2 ⊢ (𝜑 → (𝐸 ∘ 𝑉) = 𝐺)
391	300, 314, 390	3jca 1124	1 ⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  {crab 3142  Vcvv 3494   ∖ cdif 3932   ⊆ wss 3935  ifcif 4466  {csn 4560   class class class wbr 5058   ↦ cmpt 5138   × cxp 5547  ^◡ccnv 5548  ran crn 5550   “ cima 5552   ∘ ccom 5553   Fn wfn 6344  ⟶wf 6345  ‘cfv 6349  (class class class)co 7150   ∘_f cof 7401   ↑_m cmap 8400  Fincfn 8503   finSupp cfsupp 8827  0cc0 10531  1c1 10532   + caddc 10534  ℕcn 11632  ℕ₀cn0 11891  ℤcz 11975  Basecbs 16477  +_gcplusg 16559  ._rcmulr 16560  Scalarcsca 16562  0_gc0g 16707   Σ_g cgsu 16708  Mndcmnd 17905   MndHom cmhm 17948  Grpcgrp 18097  ._gcmg 18218   GrpHom cghm 18349  CMndccmn 18900  mulGrpcmgp 19233  1_rcur 19245  Ringcrg 19291  CRingccrg 19292   RingHom crh 19458  AssAlgcasa 20076  algSccascl 20078   mVar cmvr 20126   mPoly cmpl 20127

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-iin 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-ofr 7404  df-om 7575  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8283  df-map 8402  df-pm 8403  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-uz 12238  df-fz 12887  df-fzo 13028  df-seq 13364  df-hash 13685  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-sca 16575  df-vsca 16576  df-tset 16578  df-0g 16709  df-gsum 16710  df-mre 16851  df-mrc 16852  df-acs 16854  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-mhm 17950  df-submnd 17951  df-grp 18100  df-minusg 18101  df-sbg 18102  df-mulg 18219  df-subg 18270  df-ghm 18350  df-cntz 18441  df-cmn 18902  df-abl 18903  df-mgp 19234  df-ur 19246  df-ring 19293  df-cring 19294  df-rnghom 19461  df-subrg 19527  df-lmod 19630  df-lss 19698  df-assa 20079  df-ascl 20081  df-psr 20130  df-mvr 20131  df-mpl 20132

This theorem is referenced by:  evlseu  20290