Theorem evlslem1 22107

Description: Lemma for evlseu 22108, 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 2736	. . 3 ⊢ (1r‘𝑃) = (1r‘𝑃)
3		eqid 2736	. . 3 ⊢ (1r‘𝑆) = (1r‘𝑆)
4		eqid 2736	. . 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 20244	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
10	6, 7, 9	mplringd 22044	. . 3 ⊢ (𝜑 → 𝑃 ∈ Ring)
11		evlslem1.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ CRing)
12	11	crngringd 20244	. . 3 ⊢ (𝜑 → 𝑆 ∈ Ring)
13		2fveq3 6910	. . . . . 6 ⊢ (𝑥 = (1r‘𝑅) → (𝐸‘(𝐴‘𝑥)) = (𝐸‘(𝐴‘(1r‘𝑅))))
14		fveq2 6905	. . . . . 6 ⊢ (𝑥 = (1r‘𝑅) → (𝐹‘𝑥) = (𝐹‘(1r‘𝑅)))
15	13, 14	eqeq12d 2752	. . . . 5 ⊢ (𝑥 = (1r‘𝑅) → ((𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥) ↔ (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅))))
16		evlslem1.d	. . . . . . . . 9 ⊢ 𝐷 = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
17		eqid 2736	. . . . . . . . 9 ⊢ (0g‘𝑅) = (0g‘𝑅)
18		eqid 2736	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
19		evlslem1.a	. . . . . . . . 9 ⊢ 𝐴 = (algSc‘𝑃)
20	7	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐼 ∈ 𝑊)
21	9	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
22		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅))
23	6, 16, 17, 18, 19, 20, 21, 22	mplascl 22089	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐴‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅))))
24	23	fveq2d 6909	. . . . . . 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 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing)
31	11	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing)
32		evlslem1.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
33	32	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
34		evlslem1.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
35	34	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼⟶𝐶)
36	16	psrbag0 22087	. . . . . . . . . 10 ⊢ (𝐼 ∈ 𝑊 → (𝐼 × {0}) ∈ 𝐷)
37	7, 36	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 × {0}) ∈ 𝐷)
38	37	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷)
39	6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 20, 30, 31, 33, 35, 17, 38, 22	evlslem3 22105	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g‘𝑅)))) = ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))))
40		0zd 12627	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 0 ∈ ℤ)
41		fvexd 6920	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ V)
42		fconstmpt 5746	. . . . . . . . . . . . . . 15 ⊢ (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0)
43	42	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐼 × {0}) = (𝑥 ∈ 𝐼 ↦ 0))
44	34	feqmptd 6976	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐼 ↦ (𝐺‘𝑥)))
45	7, 40, 41, 43, 44	offval2 7718	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))))
46	34	ffvelcdmda 7103	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐺‘𝑥) ∈ 𝐶)
47	26, 25	mgpbas 20143	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (Base‘𝑇)
48	26, 3	ringidval 20181	. . . . . . . . . . . . . . . 16 ⊢ (1r‘𝑆) = (0g‘𝑇)
49	47, 48, 27	mulg0 19093	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑥) ∈ 𝐶 → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆))
50	46, 49	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (0 ↑ (𝐺‘𝑥)) = (1r‘𝑆))
51	50	mpteq2dva 5241	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (0 ↑ (𝐺‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))
52	45, 51	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐼 × {0}) ∘f ↑ 𝐺) = (𝑥 ∈ 𝐼 ↦ (1r‘𝑆)))
53	52	oveq2d 7448	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))))
54	26	crngmgp 20239	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
55	11, 54	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ CMnd)
56	55	cmnmndd 19823	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ Mnd)
57	48	gsumz 18850	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆))
58	56, 7, 57	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 Σg (𝑥 ∈ 𝐼 ↦ (1r‘𝑆))) = (1r‘𝑆))
59	53, 58	eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (1r‘𝑆))
60	59	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺)) = (1r‘𝑆))
61	60	oveq2d 7448	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))) = ((𝐹‘𝑥) · (1r‘𝑆)))
62	18, 25	rhmf 20486	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶)
63	32, 62	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶𝐶)
64	63	ffvelcdmda 7103	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ 𝐶)
65	25, 5, 3	ringridm 20268	. . . . . . . . 9 ⊢ ((𝑆 ∈ Ring ∧ (𝐹‘𝑥) ∈ 𝐶) → ((𝐹‘𝑥) · (1r‘𝑆)) = (𝐹‘𝑥))
66	12, 64, 65	syl2an2r 685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (1r‘𝑆)) = (𝐹‘𝑥))
67	61, 66	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f ↑ 𝐺))) = (𝐹‘𝑥))
68	24, 39, 67	3eqtrd 2780	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥))
69	68	ralrimiva 3145	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴‘𝑥)) = (𝐹‘𝑥))
70		eqid 2736	. . . . . . 7 ⊢ (1r‘𝑅) = (1r‘𝑅)
71	18, 70	ringidcl 20263	. . . . . 6 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ (Base‘𝑅))
72	9, 71	syl 17	. . . . 5 ⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅))
73	15, 69, 72	rspcdva 3622	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐹‘(1r‘𝑅)))
74	6	mplassa 22043	. . . . . . . . 9 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
75	7, 8, 74	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ AssAlg)
76		eqid 2736	. . . . . . . . 9 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
77	19, 76	asclrhm 21911	. . . . . . . 8 ⊢ (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
78	75, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
79	6, 7, 8	mplsca 22034	. . . . . . . 8 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
80	79	oveq1d 7447	. . . . . . 7 ⊢ (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
81	78, 80	eleqtrrd 2843	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (𝑅 RingHom 𝑃))
82	70, 2	rhm1 20490	. . . . . 6 ⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r‘𝑅)) = (1r‘𝑃))
83	81, 82	syl 17	. . . . 5 ⊢ (𝜑 → (𝐴‘(1r‘𝑅)) = (1r‘𝑃))
84	83	fveq2d 6909	. . . 4 ⊢ (𝜑 → (𝐸‘(𝐴‘(1r‘𝑅))) = (𝐸‘(1r‘𝑃)))
85	70, 3	rhm1 20490	. . . . 5 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
86	32, 85	syl 17	. . . 4 ⊢ (𝜑 → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
87	73, 84, 86	3eqtr3d 2784	. . 3 ⊢ (𝜑 → (𝐸‘(1r‘𝑃)) = (1r‘𝑆))
88		eqid 2736	. . . . 5 ⊢ (+g‘𝑃) = (+g‘𝑃)
89		eqid 2736	. . . . 5 ⊢ (+g‘𝑆) = (+g‘𝑆)
90	10	ringgrpd 20240	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Grp)
91	12	ringgrpd 20240	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ Grp)
92		eqid 2736	. . . . . . 7 ⊢ (0g‘𝑆) = (0g‘𝑆)
93		ringcmn 20280	. . . . . . . . 9 ⊢ (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
94	12, 93	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ CMnd)
95	94	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CMnd)
96		ovex 7465	. . . . . . . . 9 ⊢ (ℕ0 ↑m 𝐼) ∈ V
97	16, 96	rabex2 5340	. . . . . . . 8 ⊢ 𝐷 ∈ V
98	97	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐷 ∈ V)
99	7	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐼 ∈ 𝑊)
100	8	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑅 ∈ CRing)
101	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑆 ∈ CRing)
102	32	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
103	34	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝐺:𝐼⟶𝐶)
104		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ 𝐵)
105	6, 1, 25, 16, 26, 27, 5, 28, 29, 99, 100, 101, 102, 103, 104	evlslem6 22106	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
106	105	simpld 494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
107	105	simprd 495	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
108	25, 92, 95, 98, 106, 107	gsumcl 19934	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝐵) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ 𝐶)
109	108, 29	fmptd 7133	. . . . 5 ⊢ (𝜑 → 𝐸:𝐵⟶𝐶)
110		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (+g‘𝑅) = (+g‘𝑅)
111		simplrl 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 ∈ 𝐵)
112		simplrr 777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 ∈ 𝐵)
113	6, 1, 110, 88, 111, 112	mpladd 22030	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥(+g‘𝑃)𝑦) = (𝑥 ∘f (+g‘𝑅)𝑦))
114	113	fveq1d 6907	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏))
115		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
116	6, 18, 1, 16, 115	mplelf 22019	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥:𝐷⟶(Base‘𝑅))
117	116	ffnd 6736	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 Fn 𝐷)
118	117	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑥 Fn 𝐷)
119		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
120	6, 18, 1, 16, 119	mplelf 22019	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦:𝐷⟶(Base‘𝑅))
121	120	ffnd 6736	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 Fn 𝐷)
122	121	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑦 Fn 𝐷)
123	97	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐷 ∈ V)
124		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐷)
125		fnfvof 7715	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 Fn 𝐷 ∧ 𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏 ∈ 𝐷)) → ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
126	118, 122, 123, 124, 125	syl22anc 838	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∘f (+g‘𝑅)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
127	114, 126	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝑥(+g‘𝑃)𝑦)‘𝑏) = ((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏)))
128	127	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))))
129		rhmghm 20485	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
130	32, 129	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ (𝑅 GrpHom 𝑆))
131	130	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
132	116	ffvelcdmda 7103	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑥‘𝑏) ∈ (Base‘𝑅))
133	120	ffvelcdmda 7103	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑦‘𝑏) ∈ (Base‘𝑅))
134	18, 110, 89	ghmlin 19240	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥‘𝑏) ∈ (Base‘𝑅) ∧ (𝑦‘𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
135	131, 132, 133, 134	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥‘𝑏)(+g‘𝑅)(𝑦‘𝑏))) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
136	128, 135	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))))
137	136	oveq1d 7447	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
138	12	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ Ring)
139	63	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐹:(Base‘𝑅)⟶𝐶)
140	139, 132	ffvelcdmd 7104	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑥‘𝑏)) ∈ 𝐶)
141	139, 133	ffvelcdmd 7104	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝐹‘(𝑦‘𝑏)) ∈ 𝐶)
142	55	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝑇 ∈ CMnd)
143	34	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → 𝐺:𝐼⟶𝐶)
144	16, 47, 27, 142, 124, 143	psrbagev2 22103	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶)
145	25, 89, 5	ringdir 20260	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥‘𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
146	138, 140, 141, 144, 145	syl13anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → (((𝐹‘(𝑥‘𝑏))(+g‘𝑆)(𝐹‘(𝑦‘𝑏))) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
147	137, 146	eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
148	147	mpteq2dva 5241	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
149	97	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ V)
150		ovexd 7467	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V)
151		ovexd 7467	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) ∈ V)
152		eqidd 2737	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
153		eqidd 2737	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
154	149, 150, 151, 152, 153	offval2 7718	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑏 ∈ 𝐷 ↦ (((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))(+g‘𝑆)((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
155	148, 154	eqtr4d 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
156	155	oveq2d 7448	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
157	94	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CMnd)
158	7	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐼 ∈ 𝑊)
159	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CRing)
160	11	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑆 ∈ CRing)
161	32	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
162	34	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺:𝐼⟶𝐶)
163	6, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 115	evlslem6 22106	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
164	163	simpld 494	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
165	6, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 119	evlslem6 22106	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶 ∧ (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆)))
166	165	simpld 494	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))):𝐷⟶𝐶)
167	163	simprd 495	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
168	165	simprd 495	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) finSupp (0g‘𝑆))
169	25, 92, 89, 157, 149, 164, 166, 167, 168	gsumadd 19942	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg ((𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) ∘f (+g‘𝑆)(𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
170	156, 169	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
171	90	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Grp)
172	1, 88	grpcl 18960	. . . . . . . 8 ⊢ ((𝑃 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵)
173	171, 115, 119, 172	syl3anc 1372	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑃)𝑦) ∈ 𝐵)
174		fveq1 6904	. . . . . . . . . . . 12 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑝‘𝑏) = ((𝑥(+g‘𝑃)𝑦)‘𝑏))
175	174	fveq2d 6909	. . . . . . . . . . 11 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝐹‘(𝑝‘𝑏)) = (𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)))
176	175	oveq1d 7447	. . . . . . . . . 10 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
177	176	mpteq2dv 5243	. . . . . . . . 9 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
178	177	oveq2d 7448	. . . . . . . 8 ⊢ (𝑝 = (𝑥(+g‘𝑃)𝑦) → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
179		ovex 7465	. . . . . . . 8 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
180	178, 29, 179	fvmpt 7015	. . . . . . 7 ⊢ ((𝑥(+g‘𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
181	173, 180	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘((𝑥(+g‘𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
182		fveq1 6904	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑥 → (𝑝‘𝑏) = (𝑥‘𝑏))
183	182	fveq2d 6909	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑥 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑥‘𝑏)))
184	183	oveq1d 7447	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑥 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
185	184	mpteq2dv 5243	. . . . . . . . . 10 ⊢ (𝑝 = 𝑥 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
186	185	oveq2d 7448	. . . . . . . . 9 ⊢ (𝑝 = 𝑥 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
187		ovex 7465	. . . . . . . . 9 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
188	186, 29, 187	fvmpt 7015	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐵 → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
189	115, 188	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑥) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
190		fveq1 6904	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑦 → (𝑝‘𝑏) = (𝑦‘𝑏))
191	190	fveq2d 6909	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑦 → (𝐹‘(𝑝‘𝑏)) = (𝐹‘(𝑦‘𝑏)))
192	191	oveq1d 7447	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑦 → ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))) = ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))
193	192	mpteq2dv 5243	. . . . . . . . . 10 ⊢ (𝑝 = 𝑦 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))
194	193	oveq2d 7448	. . . . . . . . 9 ⊢ (𝑝 = 𝑦 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
195		ovex 7465	. . . . . . . . 9 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
196	194, 29, 195	fvmpt 7015	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐵 → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
197	196	ad2antll 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘𝑦) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))))
198	189, 197	oveq12d 7450	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)) = ((𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑥‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))(+g‘𝑆)(𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑦‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺)))))))
199	170, 181, 198	3eqtr4d 2786	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(+g‘𝑃)𝑦)) = ((𝐸‘𝑥)(+g‘𝑆)(𝐸‘𝑦)))
200	1, 25, 88, 89, 90, 91, 109, 199	isghmd 19244	. . . 4 ⊢ (𝜑 → 𝐸 ∈ (𝑃 GrpHom 𝑆))
201		eqid 2736	. . . . . . . . . . 11 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
202	201, 26	rhmmhm 20480	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
203	32, 202	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
204	203	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
205		simprll 778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥 ∈ 𝐵)
206	6, 18, 1, 16, 205	mplelf 22019	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑥:𝐷⟶(Base‘𝑅))
207		simprrl 780	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑧 ∈ 𝐷)
208	206, 207	ffvelcdmd 7104	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑥‘𝑧) ∈ (Base‘𝑅))
209		simprlr 779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦 ∈ 𝐵)
210	6, 18, 1, 16, 209	mplelf 22019	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑦:𝐷⟶(Base‘𝑅))
211		simprrr 781	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑤 ∈ 𝐷)
212	210, 211	ffvelcdmd 7104	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑦‘𝑤) ∈ (Base‘𝑅))
213	201, 18	mgpbas 20143	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
214		eqid 2736	. . . . . . . . . 10 ⊢ (.r‘𝑅) = (.r‘𝑅)
215	201, 214	mgpplusg 20142	. . . . . . . . 9 ⊢ (.r‘𝑅) = (+g‘(mulGrp‘𝑅))
216	26, 5	mgpplusg 20142	. . . . . . . . 9 ⊢ · = (+g‘𝑇)
217	213, 215, 216	mhmlin 18807	. . . . . . . 8 ⊢ ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))))
218	204, 208, 212, 217	syl3anc 1372	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) = ((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))))
219	56	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → 𝑇 ∈ Mnd)
220		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 ∈ 𝐷)
221	16	psrbagf 21939	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0)
222	220, 221	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧:𝐼⟶ℕ0)
223	222	ffvelcdmda 7103	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) ∈ ℕ0)
224	16	psrbagf 21939	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ 𝐷 → 𝑤:𝐼⟶ℕ0)
225	224	ad2antll 729	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤:𝐼⟶ℕ0)
226	225	ffvelcdmda 7103	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) ∈ ℕ0)
227	34	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺:𝐼⟶𝐶)
228	227	ffvelcdmda 7103	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ 𝐶)
229	47, 27, 216	mulgnn0dir 19123	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ Mnd ∧ ((𝑧‘𝑣) ∈ ℕ0 ∧ (𝑤‘𝑣) ∈ ℕ0 ∧ (𝐺‘𝑣) ∈ 𝐶)) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
230	219, 223, 226, 228, 229	syl13anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣)) = (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
231	230	mpteq2dva 5241	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))))
232	7	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐼 ∈ 𝑊)
233		ovexd 7467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) + (𝑤‘𝑣)) ∈ V)
234		fvexd 6920	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) ∈ V)
235	222	ffnd 6736	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑧 Fn 𝐼)
236	225	ffnd 6736	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 Fn 𝐼)
237		inidm 4226	. . . . . . . . . . . . 13 ⊢ (𝐼 ∩ 𝐼) = 𝐼
238		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑧‘𝑣) = (𝑧‘𝑣))
239		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝑤‘𝑣) = (𝑤‘𝑣))
240	235, 236, 232, 232, 237, 238, 239	offval 7707	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f + 𝑤) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) + (𝑤‘𝑣))))
241	34	feqmptd 6976	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣)))
242	241	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 = (𝑣 ∈ 𝐼 ↦ (𝐺‘𝑣)))
243	232, 233, 234, 240, 242	offval2 7718	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) + (𝑤‘𝑣)) ↑ (𝐺‘𝑣))))
244		ovexd 7467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑧‘𝑣) ↑ (𝐺‘𝑣)) ∈ V)
245		ovexd 7467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → ((𝑤‘𝑣) ↑ (𝐺‘𝑣)) ∈ V)
246	34	ffnd 6736	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 Fn 𝐼)
247	246	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝐺 Fn 𝐼)
248		eqidd 2737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) ∧ 𝑣 ∈ 𝐼) → (𝐺‘𝑣) = (𝐺‘𝑣))
249	235, 247, 232, 232, 237, 238, 248	offval 7707	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑧‘𝑣) ↑ (𝐺‘𝑣))))
250	236, 247, 232, 232, 237, 239, 248	offval 7707	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) = (𝑣 ∈ 𝐼 ↦ ((𝑤‘𝑣) ↑ (𝐺‘𝑣))))
251	232, 244, 245, 249, 250	offval2 7718	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)) = (𝑣 ∈ 𝐼 ↦ (((𝑧‘𝑣) ↑ (𝐺‘𝑣)) · ((𝑤‘𝑣) ↑ (𝐺‘𝑣)))))
252	231, 243, 251	3eqtr4d 2786	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺) = ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺)))
253	252	oveq2d 7448	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))))
254	55	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑇 ∈ CMnd)
255	16, 47, 27, 48, 254, 220, 227	psrbagev1 22102	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆)))
256	255	simpld 494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺):𝐼⟶𝐶)
257		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → 𝑤 ∈ 𝐷)
258	16, 47, 27, 48, 254, 257, 227	psrbagev1 22102	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → ((𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶 ∧ (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆)))
259	258	simpld 494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺):𝐼⟶𝐶)
260	255	simprd 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑧 ∘f ↑ 𝐺) finSupp (1r‘𝑆))
261	258	simprd 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑤 ∘f ↑ 𝐺) finSupp (1r‘𝑆))
262	47, 48, 216, 254, 232, 256, 259, 260, 261	gsumadd 19942	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f ↑ 𝐺) ∘f · (𝑤 ∘f ↑ 𝐺))) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
263	253, 262	eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
264	263	adantrl 716	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺)) = ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
265	218, 264	oveq12d 7450	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
266	55	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑇 ∈ CMnd)
267	63	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶)
268	267, 208	ffvelcdmd 7104	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑥‘𝑧)) ∈ 𝐶)
269	267, 212	ffvelcdmd 7104	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐹‘(𝑦‘𝑤)) ∈ 𝐶)
270	16, 47, 27, 254, 220, 227	psrbagev2 22103	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶)
271	270	adantrl 716	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶)
272	16, 47, 27, 254, 257, 227	psrbagev2 22103	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷)) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)
273	272	adantrl 716	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)
274	47, 216	cmn4 19820	. . . . . . 7 ⊢ ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥‘𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦‘𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤 ∘f ↑ 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
275	266, 268, 269, 271, 273, 274	syl122anc 1380	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (((𝐹‘(𝑥‘𝑧)) · (𝐹‘(𝑦‘𝑤))) · ((𝑇 Σg (𝑧 ∘f ↑ 𝐺)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
276	265, 275	eqtrd 2776	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐹‘((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤))) · (𝑇 Σg ((𝑧 ∘f + 𝑤) ∘f ↑ 𝐺))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
277	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐼 ∈ 𝑊)
278	8	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ CRing)
279	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑆 ∈ CRing)
280	32	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆))
281	34	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝐺:𝐼⟶𝐶)
282	16	psrbagaddcl 21945	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) → (𝑧 ∘f + 𝑤) ∈ 𝐷)
283	282	ad2antll 729	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝑧 ∘f + 𝑤) ∈ 𝐷)
284	9	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → 𝑅 ∈ Ring)
285	18, 214	ringcl 20248	. . . . . . 7 ⊢ ((𝑅 ∈ Ring ∧ (𝑥‘𝑧) ∈ (Base‘𝑅) ∧ (𝑦‘𝑤) ∈ (Base‘𝑅)) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅))
286	284, 208, 212, 285	syl3anc 1372	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)) ∈ (Base‘𝑅))
287	6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 283, 286	evlslem3 22105	. . . . 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 22105	. . . . . 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 22105	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅)))) = ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺))))
290	288, 289	oveq12d 7450	. . . . 5 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))) = (((𝐹‘(𝑥‘𝑧)) · (𝑇 Σg (𝑧 ∘f ↑ 𝐺))) · ((𝐹‘(𝑦‘𝑤)) · (𝑇 Σg (𝑤 ∘f ↑ 𝐺)))))
291	276, 287, 290	3eqtr4d 2786	. . . 4 ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷))) → (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = (𝑧 ∘f + 𝑤), ((𝑥‘𝑧)(.r‘𝑅)(𝑦‘𝑤)), (0g‘𝑅)))) = ((𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑧, (𝑥‘𝑧), (0g‘𝑅)))) · (𝐸‘(𝑣 ∈ 𝐷 ↦ if(𝑣 = 𝑤, (𝑦‘𝑤), (0g‘𝑅))))))
292	6, 1, 5, 17, 16, 7, 8, 11, 200, 291	evlslem2 22104	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐸‘(𝑥(.r‘𝑃)𝑦)) = ((𝐸‘𝑥) · (𝐸‘𝑦)))
293	1, 2, 3, 4, 5, 10, 12, 87, 292, 25, 88, 89, 109, 199	isrhmd 20489	. 2 ⊢ (𝜑 → 𝐸 ∈ (𝑃 RingHom 𝑆))
294		ovex 7465	. . . . . 6 ⊢ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘(𝑝‘𝑏)) · (𝑇 Σg (𝑏 ∘f ↑ 𝐺))))) ∈ V
295	294, 29	fnmpti 6710	. . . . 5 ⊢ 𝐸 Fn 𝐵
296	295	a1i 11	. . . 4 ⊢ (𝜑 → 𝐸 Fn 𝐵)
297	18, 1	rhmf 20486	. . . . . 6 ⊢ (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵)
298	81, 297	syl 17	. . . . 5 ⊢ (𝜑 → 𝐴:(Base‘𝑅)⟶𝐵)
299	298	ffnd 6736	. . . 4 ⊢ (𝜑 → 𝐴 Fn (Base‘𝑅))
300	298	frnd 6743	. . . 4 ⊢ (𝜑 → ran 𝐴 ⊆ 𝐵)
301		fnco 6685	. . . 4 ⊢ ((𝐸 Fn 𝐵 ∧ 𝐴 Fn (Base‘𝑅) ∧ ran 𝐴 ⊆ 𝐵) → (𝐸 ∘ 𝐴) Fn (Base‘𝑅))
302	296, 299, 300, 301	syl3anc 1372	. . 3 ⊢ (𝜑 → (𝐸 ∘ 𝐴) Fn (Base‘𝑅))
303	63	ffnd 6736	. . 3 ⊢ (𝜑 → 𝐹 Fn (Base‘𝑅))
304		fvco2 7005	. . . . 5 ⊢ ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥)))
305	299, 304	sylan 580	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐸‘(𝐴‘𝑥)))
306	305, 68	eqtrd 2776	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸 ∘ 𝐴)‘𝑥) = (𝐹‘𝑥))
307	302, 303, 306	eqfnfvd 7053	. 2 ⊢ (𝜑 → (𝐸 ∘ 𝐴) = 𝐹)
308	6, 28, 1, 7, 9	mvrf2 22014	. . . . 5 ⊢ (𝜑 → 𝑉:𝐼⟶𝐵)
309	308	ffnd 6736	. . . 4 ⊢ (𝜑 → 𝑉 Fn 𝐼)
310	308	frnd 6743	. . . 4 ⊢ (𝜑 → ran 𝑉 ⊆ 𝐵)
311		fnco 6685	. . . 4 ⊢ ((𝐸 Fn 𝐵 ∧ 𝑉 Fn 𝐼 ∧ ran 𝑉 ⊆ 𝐵) → (𝐸 ∘ 𝑉) Fn 𝐼)
312	296, 309, 310, 311	syl3anc 1372	. . 3 ⊢ (𝜑 → (𝐸 ∘ 𝑉) Fn 𝐼)
313		fvco2 7005	. . . . 5 ⊢ ((𝑉 Fn 𝐼 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥)))
314	309, 313	sylan 580	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐸‘(𝑉‘𝑥)))
315	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊)
316	8	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CRing)
317		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
318	28, 16, 17, 70, 315, 316, 317	mvrval 22003	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅))))
319	318	fveq2d 6909	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))))
320	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ CRing)
321	32	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆))
322	34	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐺:𝐼⟶𝐶)
323	16	psrbagsn 22088	. . . . . . . 8 ⊢ (𝐼 ∈ 𝑊 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
324	7, 323	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
325	324	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
326	72	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (1r‘𝑅) ∈ (Base‘𝑅))
327	6, 1, 25, 18, 16, 26, 27, 5, 28, 29, 315, 316, 320, 321, 322, 17, 325, 326	evlslem3 22105	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r‘𝑅), (0g‘𝑅)))) = ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))))
328	86	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆))
329		1nn0 12544	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ0
330		0nn0 12543	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ0
331	329, 330	ifcli 4572	. . . . . . . . . . . . 13 ⊢ if(𝑧 = 𝑥, 1, 0) ∈ ℕ0
332	331	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, 1, 0) ∈ ℕ0)
333	34	ffvelcdmda 7103	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶)
334		eqidd 2737	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))
335	34	feqmptd 6976	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐼 ↦ (𝐺‘𝑧)))
336	7, 332, 333, 334, 335	offval2 7718	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))))
337		oveq1 7439	. . . . . . . . . . . . . 14 ⊢ (1 = if(𝑧 = 𝑥, 1, 0) → (1 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))
338	337	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (1 = if(𝑧 = 𝑥, 1, 0) → ((1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
339		oveq1 7439	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑧 = 𝑥, 1, 0) → (0 ↑ (𝐺‘𝑧)) = (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)))
340	339	eqeq1d 2738	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑧 = 𝑥, 1, 0) → ((0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
341	333	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (𝐺‘𝑧) ∈ 𝐶)
342	47, 27	mulg1 19100	. . . . . . . . . . . . . . 15 ⊢ ((𝐺‘𝑧) ∈ 𝐶 → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧))
343	341, 342	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = (𝐺‘𝑧))
344		iftrue 4530	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧))
345	344	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑧))
346	343, 345	eqtr4d 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ 𝑧 = 𝑥) → (1 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
347	47, 48, 27	mulg0 19093	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑧) ∈ 𝐶 → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
348	333, 347	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
349	348	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = (1r‘𝑆))
350		iffalse 4533	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
351	350	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
352	349, 351	eqtr4d 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
353	338, 340, 346, 352	ifbothda 4563	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧)) = if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
354	353	mpteq2dva 5241	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) ↑ (𝐺‘𝑧))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
355	336, 354	eqtrd 2776	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
356	355	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))))
357	356	oveq2d 7448	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))))
358	56	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑇 ∈ Mnd)
359	333	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (𝐺‘𝑧) ∈ 𝐶)
360	25, 3	ringidcl 20263	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Ring → (1r‘𝑆) ∈ 𝐶)
361	12, 360	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (1r‘𝑆) ∈ 𝐶)
362	361	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (1r‘𝑆) ∈ 𝐶)
363	359, 362	ifcld 4571	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) ∈ 𝐶)
364	363	fmpttd 7134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))):𝐼⟶𝐶)
365		eldifsnneq 4790	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥)
366	365, 350	syl 17	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
367	366	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (1r‘𝑆))
368	367, 315	suppss2 8226	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) supp (1r‘𝑆)) ⊆ {𝑥})
369	47, 48, 358, 315, 317, 364, 368	gsumpt 19981	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))) = ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥))
370		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥))
371	344, 370	eqtrd 2776	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)) = (𝐺‘𝑥))
372		eqid 2736	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆))) = (𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))
373		fvex 6918	. . . . . . . . . 10 ⊢ (𝐺‘𝑥) ∈ V
374	371, 372, 373	fvmpt 7015	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐼 → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥))
375	374	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, (𝐺‘𝑧), (1r‘𝑆)))‘𝑥) = (𝐺‘𝑥))
376	357, 369, 375	3eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺)) = (𝐺‘𝑥))
377	328, 376	oveq12d 7450	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) = ((1r‘𝑆) · (𝐺‘𝑥)))
378	25, 5, 3	ringlidm 20267	. . . . . . 7 ⊢ ((𝑆 ∈ Ring ∧ (𝐺‘𝑥) ∈ 𝐶) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥))
379	12, 46, 378	syl2an2r 685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((1r‘𝑆) · (𝐺‘𝑥)) = (𝐺‘𝑥))
380	377, 379	eqtrd 2776	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐹‘(1r‘𝑅)) · (𝑇 Σg ((𝑧 ∈ 𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f ↑ 𝐺))) = (𝐺‘𝑥))
381	319, 327, 380	3eqtrd 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐸‘(𝑉‘𝑥)) = (𝐺‘𝑥))
382	314, 381	eqtrd 2776	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐸 ∘ 𝑉)‘𝑥) = (𝐺‘𝑥))
383	312, 246, 382	eqfnfvd 7053	. 2 ⊢ (𝜑 → (𝐸 ∘ 𝑉) = 𝐺)
384	293, 307, 383	3jca 1128	1 ⊢ (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸 ∘ 𝐴) = 𝐹 ∧ (𝐸 ∘ 𝑉) = 𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  {crab 3435  Vcvv 3479   ∖ cdif 3947   ⊆ wss 3950  ifcif 4524  {csn 4625   class class class wbr 5142   ↦ cmpt 5224   × cxp 5682  ^◡ccnv 5683  ran crn 5685   “ cima 5687   ∘ ccom 5688   Fn wfn 6555  ⟶wf 6556  ‘cfv 6560  (class class class)co 7432   ∘_f cof 7696   ↑_m cmap 8867  Fincfn 8986   finSupp cfsupp 9402  0cc0 11156  1c1 11157   + caddc 11159  ℕcn 12267  ℕ₀cn0 12528  ℤcz 12615  Basecbs 17248  +_gcplusg 17298  ._rcmulr 17299  Scalarcsca 17301  0_gc0g 17485   Σ_g cgsu 17486  Mndcmnd 18748   MndHom cmhm 18795  Grpcgrp 18952  ._gcmg 19086   GrpHom cghm 19231  CMndccmn 19799  mulGrpcmgp 20138  1_rcur 20179  Ringcrg 20231  CRingccrg 20232   RingHom crh 20470  AssAlgcasa 21871  algSccascl 21873   mVar cmvr 21926   mPoly cmpl 21927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-of 7698  df-ofr 7699  df-om 7889  df-1st 8015  df-2nd 8016  df-supp 8187  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-er 8746  df-map 8869  df-pm 8870  df-ixp 8939  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fsupp 9403  df-sup 9483  df-oi 9551  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12529  df-z 12616  df-dec 12736  df-uz 12880  df-fz 13549  df-fzo 13696  df-seq 14044  df-hash 14371  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17249  df-ress 17276  df-plusg 17311  df-mulr 17312  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-hom 17322  df-cco 17323  df-0g 17487  df-gsum 17488  df-prds 17493  df-pws 17495  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-mhm 18797  df-submnd 18798  df-grp 18955  df-minusg 18956  df-sbg 18957  df-mulg 19087  df-subg 19142  df-ghm 19232  df-cntz 19336  df-cmn 19801  df-abl 19802  df-mgp 20139  df-rng 20151  df-ur 20180  df-ring 20233  df-cring 20234  df-rhm 20473  df-subrng 20547  df-subrg 20571  df-lmod 20861  df-lss 20931  df-assa 21874  df-ascl 21876  df-psr 21930  df-mvr 21931  df-mpl 21932

This theorem is referenced by:  evlseu  22108  evlsval3  42574