Theorem evlslem1 22135

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

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	⊢ (𝜑 → 𝐼 ∈ 𝑊)
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 2762	. . 3 ⊢ (1r‘𝑃) = (1r‘𝑃)
3		eqid 2762	. . 3 ⊢ (1r‘𝑆) = (1r‘𝑆)
4		eqid 2762	. . 3 ⊢ (.r‘𝑃) = (.r‘𝑃)
5		evlslem1.m	. . 3 ⊢ · = (.r‘𝑆)
6		evlslem1.p	. . . 4 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
7		evlslem1.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
8		evlslem1.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CRing)
9	8	crngringd 20296	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
10	6, 7, 9	mplringd 22074	. . 3 ⊢ (𝜑 → 𝑃 ∈ Ring)
11		evlslem1.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ CRing)
12	11	crngringd 20296	. . 3 ⊢ (𝜑 → 𝑆 ∈ Ring)
13		2fveq3 6872	. . . . . 6 ⊢ (𝑥 = (1r‘𝑅) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝐴‘(1r‘𝑅))))
14		fveq2 6867	. . . . . 6 ⊢ (𝑥 = (1r‘𝑅) → (𝐹‘𝑥) = (𝐹‘(1r‘𝑅)))
15	13, 14	eqeq12d 2778	. . . . 5 ⊢ (𝑥 = (1r‘𝑅) → ((𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥) ↔ (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅))))
16		evlslem1.d	. . . . . . . . 9 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
17		eqid 2762	. . . . . . . . 9 ⊢ (0g‘𝑅) = (0g‘𝑅)
18		eqid 2762	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
19		evlslem1.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑃)
20	7	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐼 ∈ 𝑊)
21	9	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
22		simpr 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅))
23	6, 16, 17, 18, 19, 20, 21, 22	mplascl 22117	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐴‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅))))
24	23	fveq2d 6871	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))))
25		evlslem1.c	. . . . . . . 8 ⊢ 𝐶 = (Base‘𝑆)
26		evlslem1.t	. . . . . . . 8 ⊢ 𝑇 = (mulGrp‘𝑆)
27		evlslem1.x	. . . . . . . 8 ⊢ ↑ = (.g‘𝑇)
28		evlslem1.v	. . . . . . . 8 ⊢ 𝑉 = (𝐼 mVar 𝑅)
29		evlslem1.e	. . . . . . . 8 ⊢ 𝐸 = (𝑝 ∈ 𝐵 ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
30	8	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing)
31	11	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing)
32		evlslem1.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
33	32	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
34		evlslem1.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
35	34	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼⟶𝐶)
36	16	psrbag0 22115	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑊 → (𝐼 × {0}) ∈ 𝐷)
37	7, 36	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷)
38	37	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷)
39	6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 20, 30, 31, 33, 35, 17, 38, 22	evlslem3 22133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) = ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))))
40		0zd 12580	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℤ)
41		fvexd 6882	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ V)
42		fconstmpt 5709	. . . . . . . . . . . . . . 15 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
43	42	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0))
44	34	feqmptd 6935	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝐺‘𝑥)))
45	7, 40, 41, 43, 44	offval2 7680	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))))
46	34	ffvelcdmda 7065	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ 𝐶)
47	26, 25	mgpbas 20191	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (Base‘𝑇)
48	26, 3	ringidval 20233	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝑆) = (0g‘𝑇)
49	47, 48, 27	mulg0 19116	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑥) ∈ 𝐶 → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆))
50	46, 49	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆))
51	50	mpteq2dva 5193	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))
52	45, 51	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))
53	52	oveq2d 7412	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))))
54	26	crngmgp 20291	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
55	11, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ CMnd)
56	55	cmnmndd 19844	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ Mnd)
57	48	gsumz 18870	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆))
58	56, 7, 57	syl2anc 593	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆))
59	53, 58	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (1r‘𝑆))
60	59	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (1r‘𝑆))
61	60	oveq2d 7412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))) = ((𝐹‘𝑥) · (1r‘𝑆)))
62	18, 25	rhmf 20533	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶)
63	32, 62	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶𝐶)
64	63	ffvelcdmda 7065	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ 𝐶)
65	25, 5, 3	ringridm 20320	. . . . . . . . 9 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝑥) ∈ 𝐶) → ((𝐹‘𝑥) · (1r‘𝑆)) = (𝐹‘𝑥))
66	12, 64, 65	syl2an2r 695	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (1r‘𝑆)) = (𝐹‘𝑥))
67	61, 66	eqtrd 2797	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))) = (𝐹‘𝑥))
68	24, 39, 67	3eqtrd 2801	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥))
69	68	ralrimiva 3154	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥))
70		eqid 2762	. . . . . . 7 ⊢ (1r‘𝑅) = (1r‘𝑅)
71	18, 70	ringidcl 20315	. . . . . 6 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ (Base‘𝑅))
72	9, 71	syl 17	. . . . 5 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
73	15, 69, 72	rspcdva 3582	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅)))
74	6	mplassa 22073	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
75	7, 8, 74	syl2anc 593	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ AssAlg)
76		eqid 2762	. . . . . . . . 9 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
77	19, 76	asclrhm 21942	. . . . . . . 8 ⊢ (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
78	75, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
79	6, 7, 8	mplsca 22064	. . . . . . . 8 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
80	79	oveq1d 7411	. . . . . . 7 ⊢ (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
81	78, 80	eleqtrrd 2865	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝑅 RingHom 𝑃))
82	70, 2	rhm1 20538	. . . . . 6 ⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r‘𝑅)) = (1r‘𝑃))
83	81, 82	syl 17	. . . . 5 ⊢ (𝜑 → (𝐴‘(1r‘𝑅)) = (1r‘𝑃))
84	83	fveq2d 6871	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐸‘(1r‘𝑃)))
85	70, 3	rhm1 20538	. . . . 5 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
86	32, 85	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
87	73, 84, 86	3eqtr3d 2805	. . 3 ⊢ (𝜑 → (𝐸‘(1r‘𝑃)) = (1r‘𝑆))
88		eqid 2762	. . . . 5 ⊢ (+g‘𝑃) = (+g‘𝑃)
89		eqid 2762	. . . . 5 ⊢ (+g‘𝑆) = (+g‘𝑆)
90	10	ringgrpd 20292	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Grp)
91	12	ringgrpd 20292	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Grp)
92		eqid 2762	. . . . . . 7 ⊢ (0g‘𝑆) = (0g‘𝑆)
93		ringcmn 20332	. . . . . . . . 9 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
94	12, 93	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ CMnd)
95	94	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CMnd)
96		ovex 7429	. . . . . . . . 9 ⊢ (ℕ0 ↑m 𝐼) ∈ V
97	16, 96	rabex2 5297	. . . . . . . 8 ⊢ 𝐷 ∈ V
98	97	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐷 ∈ V)
99	7	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐼 ∈ 𝑊)
100	8	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑅 ∈ CRing)
101	11	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CRing)
102	32	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
103	34	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐺:𝐼⟶𝐶)
104		simpr 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵)
105	6, 1, 25, 16, 26, 27, 5, 28, 29, 99, 100, 101, 102, 103, 104	evlslem6 22134	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
106	105	simpld 498	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
107	105	simprd 499	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
108	25, 92, 95, 98, 106, 107	gsumcl 19955	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ 𝐶)
109	108, 29	fmptd 7095	. . . . 5 ⊢ (𝜑 → 𝐸:𝐵⟶𝐶)
110		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝑅) = (+g‘𝑅)
111		simplrl 786	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 ∈ 𝐵)
112		simplrr 787	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 ∈ 𝐵)
113	6, 1, 110, 88, 111, 112	mpladd 22060	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥(+g‘𝑃)𝑦) = (𝑥 ∘f (+g‘𝑅)𝑦))
114	113	fveq1d 6869	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏))
115		simprl 780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
116	6, 18, 1, 16, 115	mplelf 22049	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥:𝐷⟶(Base‘𝑅))
117	116	ffnd 6692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 Fn 𝐷)
118	117	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 Fn 𝐷)
119		simprr 782	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
120	6, 18, 1, 16, 119	mplelf 22049	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦:𝐷⟶(Base‘𝑅))
121	120	ffnd 6692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 Fn 𝐷)
122	121	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 Fn 𝐷)
123	97	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐷 ∈ V)
124		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷)
125		fnfvof 7677	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 Fn 𝐷 ∧ 𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏 ∈ 𝐷)) → ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
126	118, 122, 123, 124, 125	syl22anc 849	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
127	114, 126	eqtrd 2797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
128	127	fveq2d 6871	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))))
129		rhmghm 20532	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
130	32, 129	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))
131	130	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
132	116	ffvelcdmda 7065	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥‘𝑏) ∈ (Base‘𝑅))
133	120	ffvelcdmda 7065	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑦‘𝑏) ∈ (Base‘𝑅))
134	18, 110, 89	ghmlin 19261	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥‘𝑏) ∈ (Base‘𝑅) ∧ (𝑦‘𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
135	131, 132, 133, 134	syl3anc 1390	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
136	128, 135	eqtrd 2797	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
137	136	oveq1d 7411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
138	12	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring)
139	63	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹:(Base‘𝑅)⟶𝐶)
140	139, 132	ffvelcdmd 7066	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑥‘𝑏)) ∈ 𝐶)
141	139, 133	ffvelcdmd 7066	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑦‘𝑏)) ∈ 𝐶)
142	55	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd)
143	34	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶)
144	16, 47, 27, 142, 124, 143	psrbagev2 22131	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶)
145	25, 89, 5	ringdir 20312	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥‘𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
146	138, 140, 141, 144, 145	syl13anc 1391	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
147	137, 146	eqtrd 2797	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
148	147	mpteq2dva 5193	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
149	97	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ V)
150		ovexd 7431	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V)
151		ovexd 7431	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V)
152		eqidd 2763	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
153		eqidd 2763	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
154	149, 150, 151, 152, 153	offval2 7680	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
155	148, 154	eqtr4d 2800	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
156	155	oveq2d 7412	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
157	94	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CMnd)
158	7	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐼 ∈ 𝑊)
159	8	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CRing)
160	11	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CRing)
161	32	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
162	34	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺:𝐼⟶𝐶)
163	6, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 115	evlslem6 22134	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
164	163	simpld 498	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
165	6, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 119	evlslem6 22134	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
166	165	simpld 498	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
167	163	simprd 499	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
168	165	simprd 499	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
169	25, 92, 89, 157, 149, 164, 166, 167, 168	gsumadd 19963	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
170	156, 169	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
171	90	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Grp)
172	1, 88	grpcl 18983	. . . . . . . 8 ⊢ ((𝑃 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵)
173	171, 115, 119, 172	syl3anc 1390	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵)
174		fveq1 6866	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑝‘𝑏) = ((𝑥(+g‘𝑃)𝑦)‘𝑏))
175	174	fveq2d 6871	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)))
176	175	oveq1d 7411	. . . . . . . . . 10 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
177	176	mpteq2dv 5194	. . . . . . . . 9 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
178	177	oveq2d 7412	. . . . . . . 8 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
179		ovex 7429	. . . . . . . 8 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
180	178, 29, 179	fvmpt 6975	. . . . . . 7 ⊢ ((𝑥(+g‘𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
181	173, 180	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
182		fveq1 6866	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑥 → (𝑝‘𝑏) = (𝑥‘𝑏))
183	182	fveq2d 6871	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑥 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑥‘𝑏)))
184	183	oveq1d 7411	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑥 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
185	184	mpteq2dv 5194	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
186	185	oveq2d 7412	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
187		ovex 7429	. . . . . . . . 9 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
188	186, 29, 187	fvmpt 6975	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐵 → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
189	115, 188	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
190		fveq1 6866	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑦 → (𝑝‘𝑏) = (𝑦‘𝑏))
191	190	fveq2d 6871	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑦 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑦‘𝑏)))
192	191	oveq1d 7411	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑦 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
193	192	mpteq2dv 5194	. . . . . . . . . 10 ⊢ (𝑝 = 𝑦 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
194	193	oveq2d 7412	. . . . . . . . 9 ⊢ (𝑝 = 𝑦 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
195		ovex 7429	. . . . . . . . 9 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
196	194, 29, 195	fvmpt 6975	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
197	196	ad2antll 739	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
198	189, 197	oveq12d 7414	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
199	170, 181, 198	3eqtr4d 2807	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)))
200	1, 25, 88, 89, 90, 91, 109, 199	isghmd 19265	. . . 4 ⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆))
201		eqid 2762	. . . . . . . . . . 11 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
202	201, 26	rhmmhm 20528	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
203	32, 202	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
204	203	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
205		simprll 788	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥 ∈ 𝐵)
206	6, 18, 1, 16, 205	mplelf 22049	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥:𝐷⟶(Base‘𝑅))
207		simprrl 790	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑧 ∈ 𝐷)
208	206, 207	ffvelcdmd 7066	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑥‘𝑧) ∈ (Base‘𝑅))
209		simprlr 789	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦 ∈ 𝐵)
210	6, 18, 1, 16, 209	mplelf 22049	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦:𝐷⟶(Base‘𝑅))
211		simprrr 791	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑤 ∈ 𝐷)
212	210, 211	ffvelcdmd 7066	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑦‘𝑤) ∈ (Base‘𝑅))
213	201, 18	mgpbas 20191	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
214		eqid 2762	. . . . . . . . . 10 ⊢ (.r‘𝑅) = (.r‘𝑅)
215	201, 214	mgpplusg 20190	. . . . . . . . 9 ⊢ (.r‘𝑅) = (+g‘(mulGrp‘𝑅))
216	26, 5	mgpplusg 20190	. . . . . . . . 9 ⊢ · = (+g‘𝑇)
217	213, 215, 216	mhmlin 18827	. . . . . . . 8 ⊢ ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))))
218	204, 208, 212, 217	syl3anc 1390	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))))
219	56	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → 𝑇 ∈ Mnd)
220		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 ∈ 𝐷)
221	16	psrbagf 21970	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0)
222	220, 221	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧:𝐼⟶ℕ0)
223	222	ffvelcdmda 7065	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) ∈ ℕ0)
224	16	psrbagf 21970	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝐷 → 𝑤:𝐼⟶ℕ0)
225	224	ad2antll 739	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤:𝐼⟶ℕ0)
226	225	ffvelcdmda 7065	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) ∈ ℕ0)
227	34	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺:𝐼⟶𝐶)
228	227	ffvelcdmda 7065	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ 𝐶)
229	47, 27, 216	mulgnn0dir 19146	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ Mnd ∧ ((𝑧‘𝑣) ∈ ℕ0 ∧ (𝑤‘𝑣) ∈ ℕ0 ∧ (𝐺‘𝑣) ∈ 𝐶)) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
230	219, 223, 226, 228, 229	syl13anc 1391	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
231	230	mpteq2dva 5193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))))
232	7	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐼 ∈ 𝑊)
233		ovexd 7431	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) + (𝑤‘𝑣)) ∈ V)
234		fvexd 6882	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ V)
235	222	ffnd 6692	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 Fn 𝐼)
236	225	ffnd 6692	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 Fn 𝐼)
237		inidm 4178	. . . . . . . . . . . . 13 ⊢ (𝐼 ∩ 𝐼) = 𝐼
238		eqidd 2763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) = (𝑧‘𝑣))
239		eqidd 2763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) = (𝑤‘𝑣))
240	235, 236, 232, 232, 237, 238, 239	offval 7669	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f + 𝑤) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) + (𝑤‘𝑣))))
241	34	feqmptd 6935	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣)))
242	241	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣)))
243	232, 233, 234, 240, 242	offval2 7680	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))))
244		ovexd 7431	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) ↑ (𝐺‘𝑣)) ∈ V)
245		ovexd 7431	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑤‘𝑣) ↑ (𝐺‘𝑣)) ∈ V)
246	34	ffnd 6692	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 Fn 𝐼)
247	246	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 Fn 𝐼)
248		eqidd 2763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) = (𝐺‘𝑣))
249	235, 247, 232, 232, 237, 238, 248	offval 7669	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) ↑ (𝐺‘𝑣))))
250	236, 247, 232, 232, 237, 239, 248	offval 7669	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
251	232, 244, 245, 249, 250	offval2 7680	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))))
252	231, 243, 251	3eqtr4d 2807	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)))
253	252	oveq2d 7412	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))))
254	55	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑇 ∈ CMnd)
255	16, 47, 27, 48, 254, 220, 227	psrbagev1 22130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆)))
256	255	simpld 498	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶)
257		simprr 782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 ∈ 𝐷)
258	16, 47, 27, 48, 254, 257, 227	psrbagev1 22130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆)))
259	258	simpld 498	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶)
260	255	simprd 499	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆))
261	258	simprd 499	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆))
262	47, 48, 216, 254, 232, 256, 259, 260, 261	gsumadd 19963	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
263	253, 262	eqtrd 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
264	263	adantrl 726	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
265	218, 264	oveq12d 7414	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
266	55	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑇 ∈ CMnd)
267	63	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶)
268	267, 208	ffvelcdmd 7066	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑥‘𝑧)) ∈ 𝐶)
269	267, 212	ffvelcdmd 7066	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑦‘𝑤)) ∈ 𝐶)
270	16, 47, 27, 254, 220, 227	psrbagev2 22131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶)
271	270	adantrl 726	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶)
272	16, 47, 27, 254, 257, 227	psrbagev2 22131	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)
273	272	adantrl 726	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)
274	47, 216	cmn4 19841	. . . . . . 7 ⊢ ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥‘𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
275	266, 268, 269, 271, 273, 274	syl122anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
276	265, 275	eqtrd 2797	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
277	7	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐼 ∈ 𝑊)
278	8	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ CRing)
279	11	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑆 ∈ CRing)
280	32	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆))
281	34	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐺:𝐼⟶𝐶)
282	16	psrbagaddcl 21976	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (𝑧 ∘f + 𝑤) ∈ 𝐷)
283	282	ad2antll 739	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑧 ∘f + 𝑤) ∈ 𝐷)
284	9	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ Ring)
285	18, 214	ringcl 20300	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅))
286	284, 208, 212, 285	syl3anc 1390	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅))
287	6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 283, 286	evlslem3 22133	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))))
288	6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 207, 208	evlslem3 22133	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) = ((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))))
289	6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 211, 212	evlslem3 22133	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))) = ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
290	288, 289	oveq12d 7414	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
291	276, 287, 290	3eqtr4d 2807	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))))
292	6, 1, 5, 17, 16, 7, 8, 11, 200, 291	evlslem2 22132	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦)))
293	1, 2, 3, 4, 5, 10, 12, 87, 292, 25, 88, 89, 109, 199	isrhmd 20537	. 2 ⊢ (𝜑 → 𝐸 ∈ (𝑃 RingHom 𝑆))
294		ovex 7429	. . . . . 6 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
295	294, 29	fnmpti 6664	. . . . 5 ⊢ 𝐸 Fn 𝐵
296	295	a1i 11	. . . 4 ⊢ (𝜑 → 𝐸 Fn 𝐵)
297	18, 1	rhmf 20533	. . . . . 6 ⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵)
298	81, 297	syl 17	. . . . 5 ⊢ (𝜑 → 𝐴:(Base‘𝑅)⟶𝐵)
299	298	ffnd 6692	. . . 4 ⊢ (𝜑 → 𝐴 Fn (Base‘𝑅))
300	298	frnd 6700	. . . 4 ⊢ (𝜑 → ran 𝐴 ⊆ 𝐵)
301		fnco 6639	. . . 4 ⊢ ((𝐸 Fn 𝐵 ∧ 𝐴 Fn (Base‘𝑅) ∧ ran 𝐴 ⊆ 𝐵) → (𝐸 ∘ 𝐴) Fn (Base‘𝑅))
302	296, 299, 300, 301	syl3anc 1390	. . 3 ⊢ (𝜑 → (𝐸 ∘ 𝐴) Fn (Base‘𝑅))
303	63	ffnd 6692	. . 3 ⊢ (𝜑 → 𝐹 Fn (Base‘𝑅))
304		fvco2 6964	. . . . 5 ⊢ ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥)))
305	299, 304	sylan 589	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥)))
306	305, 68	eqtrd 2797	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐹‘𝑥))
307	302, 303, 306	eqfnfvd 7014	. 2 ⊢ (𝜑 → (𝐸 ∘ 𝐴) = 𝐹)
308	6, 28, 1, 7, 9	mvrf2 22044	. . . . 5 ⊢ (𝜑 → 𝑉:𝐼⟶𝐵)
309	308	ffnd 6692	. . . 4 ⊢ (𝜑 → 𝑉 Fn 𝐼)
310	308	frnd 6700	. . . 4 ⊢ (𝜑 → ran 𝑉 ⊆ 𝐵)
311		fnco 6639	. . . 4 ⊢ ((𝐸 Fn 𝐵 ∧ 𝑉 Fn 𝐼 ∧ ran 𝑉 ⊆ 𝐵) → (𝐸 ∘ 𝑉) Fn 𝐼)
312	296, 309, 310, 311	syl3anc 1390	. . 3 ⊢ (𝜑 → (𝐸 ∘ 𝑉) Fn 𝐼)
313		fvco2 6964	. . . . 5 ⊢ ((𝑉 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥)))
314	309, 313	sylan 589	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥)))
315	7	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊)
316	8	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing)
317		simpr 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
318	28, 16, 17, 70, 315, 316, 317	mvrval 22033	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅))))
319	318	fveq2d 6871	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))))
320	11	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
321	32	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆))
322	34	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺:𝐼⟶𝐶)
323	16	psrbagsn 22116	. . . . . . . 8 ⊢ (𝐼 ∈ 𝑊 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
324	7, 323	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
325	324	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
326	72	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1r‘𝑅) ∈ (Base‘𝑅))
327	6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 315, 316, 320, 321, 322, 17, 325, 326	evlslem3 22133	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) = ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))))
328	86	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
329		1nn0 12497	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
330		0nn0 12496	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
331	329, 330	ifcli 4528	. . . . . . . . . . . . 13 ⊢ if(𝑧 = 𝑥, 1, 0) ∈ ℕ0
332	331	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, 1, 0) ∈ ℕ0)
333	34	ffvelcdmda 7065	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶)
334		eqidd 2763	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))
335	34	feqmptd 6935	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐼 ↦ (𝐺‘𝑧)))
336	7, 332, 333, 334, 335	offval2 7680	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))))
337		oveq1 7403	. . . . . . . . . . . . . 14 ⊢ (1 = if(𝑧 = 𝑥, 1, 0) → (1 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))
338	337	eqeq1d 2764	. . . . . . . . . . . . 13 ⊢ (1 = if(𝑧 = 𝑥, 1, 0) → ((1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
339		oveq1 7403	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑧 = 𝑥, 1, 0) → (0 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))
340	339	eqeq1d 2764	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑧 = 𝑥, 1, 0) → ((0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
341	333	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (𝐺‘𝑧) ∈ 𝐶)
342	47, 27	mulg1 19123	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑧) ∈ 𝐶 → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧))
343	341, 342	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧))
344		iftrue 4486	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧))
345	344	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧))
346	343, 345	eqtr4d 2800	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
347	47, 48, 27	mulg0 19116	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑧) ∈ 𝐶 → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
348	333, 347	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
349	348	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
350		iffalse 4489	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
351	350	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
352	349, 351	eqtr4d 2800	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
353	338, 340, 346, 352	ifbothda 4519	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
354	353	mpteq2dva 5193	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
355	336, 354	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
356	355	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
357	356	oveq2d 7412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))))
358	56	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ Mnd)
359	333	adantlr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶)
360	25, 3	ringidcl 20315	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Ring → (1r‘𝑆) ∈ 𝐶)
361	12, 360	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (1r‘𝑆) ∈ 𝐶)
362	361	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (1r‘𝑆) ∈ 𝐶)
363	359, 362	ifcld 4527	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ∈ 𝐶)
364	363	fmpttd 7096	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))):𝐼⟶𝐶)
365		eldifsnneq 4751	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥)
366	365, 350	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
367	366	adantl 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
368	367, 315	suppss2 8180	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) supp (1r‘𝑆)) ⊆ {𝑥})
369	47, 48, 358, 315, 317, 364, 368	gsumpt 20002	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) = ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥))
370		fveq2 6867	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥))
371	344, 370	eqtrd 2797	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑥))
372		eqid 2762	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
373		fvex 6880	. . . . . . . . . 10 ⊢ (𝐺‘𝑥) ∈ V
374	371, 372, 373	fvmpt 6975	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐼 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥))
375	374	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥))
376	357, 369, 375	3eqtrd 2801	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝐺‘𝑥))
377	328, 376	oveq12d 7414	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) = ((1r‘𝑆) · (𝐺‘𝑥)))
378	25, 5, 3	ringlidm 20319	. . . . . . 7 ⊢ ((𝑆 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐶) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥))
379	12, 46, 378	syl2an2r 695	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥))
380	377, 379	eqtrd 2797	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) = (𝐺‘𝑥))
381	319, 327, 380	3eqtrd 2801	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐺‘𝑥))
382	314, 381	eqtrd 2797	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐺‘𝑥))
383	312, 246, 382	eqfnfvd 7014	. 2 ⊢ (𝜑 → (𝐸 ∘ 𝑉) = 𝐺)
384	293, 307, 383	3jca 1141	1 ⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  {crab 3414  Vcvv 3454   ∖ cdif 3901   ⊆ wss 3904  ifcif 4480  {csn 4582   class class class wbr 5100   ↦ cmpt 5181   × cxp 5645  ^◡ccnv 5646  ran crn 5648   “ cima 5650   ∘ ccom 5651   Fn wfn 6516  ⟶wf 6517  ‘cfv 6521  (class class class)co 7396   ∘_f cof 7658   ↑_m cmap 8808  Fincfn 8927   finSupp cfsupp 9307  0cc0 11073  1c1 11074   + caddc 11076  ℕcn 12210  ℕ₀cn0 12481  ℤcz 12568  Basecbs 17245  +_gcplusg 17286  ._rcmulr 17287  Scalarcsca 17289  0_gc0g 17468   Σ_g cgsu 17469  Mndcmnd 18768   MndHom cmhm 18815  Grpcgrp 18975  ._gcmg 19109   GrpHom cghm 19253  CMndccmn 19820  mulGrpcmgp 20186  1_rcur 20231  Ringcrg 20283  CRingccrg 20284   RingHom crh 20518  AssAlgcasa 21902  algSccascl 21904   mVar cmvr 21957   mPoly cmpl 21958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-iin 4952  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-isom 6530  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7660  df-ofr 7661  df-om 7847  df-1st 7970  df-2nd 7971  df-supp 8141  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-2o 8438  df-er 8678  df-map 8810  df-pm 8811  df-ixp 8880  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fsupp 9308  df-sup 9388  df-oi 9458  df-card 9897  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12482  df-z 12569  df-dec 12689  df-uz 12840  df-fz 13513  df-fzo 13660  df-seq 14015  df-hash 14344  df-struct 17183  df-sets 17200  df-slot 17218  df-ndx 17230  df-base 17246  df-ress 17267  df-plusg 17299  df-mulr 17300  df-sca 17302  df-vsca 17303  df-ip 17304  df-tset 17305  df-ple 17306  df-ds 17308  df-hom 17310  df-cco 17311  df-0g 17470  df-gsum 17471  df-prds 17476  df-pws 17478  df-mre 17614  df-mrc 17615  df-acs 17617  df-mgm 18674  df-sgrp 18753  df-mnd 18769  df-mhm 18817  df-submnd 18818  df-grp 18978  df-minusg 18979  df-sbg 18980  df-mulg 19110  df-subg 19165  df-ghm 19254  df-cntz 19357  df-cmn 19822  df-abl 19823  df-mgp 20187  df-rng 20199  df-ur 20232  df-ring 20285  df-cring 20286  df-rhm 20521  df-subrng 20596  df-subrg 20620  df-lmod 20929  df-lss 20999  df-assa 21905  df-ascl 21907  df-psr 21961  df-mvr 21962  df-mpl 21963

This theorem is referenced by:  evlseu  22136  evlsval3  22142