evlslem1

Description: Lemma for evlseu , 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)

	Ref	Expression
Hypotheses	evlslem1.p	$⊢ P = I mPoly R$
	evlslem1.b	$⊢ B = {Base}_{P}$
	evlslem1.c	$⊢ C = {Base}_{S}$
	evlslem1.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	evlslem1.t	$⊢ T = {mulGrp}_{S}$
	evlslem1.x	$⊢ \underset{˙}{\times} = \cdot_{T}$
	evlslem1.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	evlslem1.v	$⊢ V = I mVar R$
	evlslem1.e	$⊢ E = (p \in B ⟼ \underset{b \in D}{\sum_{S}} (F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
	evlslem1.i	$⊢ φ \to I \in W$
	evlslem1.r	$⊢ φ \to R \in CRing$
	evlslem1.s	$⊢ φ \to S \in CRing$
	evlslem1.f	$⊢ φ \to F \in (R RingHom S)$
	evlslem1.g	$⊢ φ \to G : I ⟶ C$
	evlslem1.a	$⊢ A = algSc (P)$
Assertion	evlslem1	$⊢ φ \to (E \in (P RingHom S) \land E \circ A = F \land E \circ V = G)$

Proof

Step	Hyp	Ref	Expression
1		evlslem1.p	$⊢ P = I mPoly R$
2		evlslem1.b	$⊢ B = {Base}_{P}$
3		evlslem1.c	$⊢ C = {Base}_{S}$
4		evlslem1.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
5		evlslem1.t	$⊢ T = {mulGrp}_{S}$
6		evlslem1.x	$⊢ \underset{˙}{\times} = \cdot_{T}$
7		evlslem1.m	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
8		evlslem1.v	$⊢ V = I mVar R$
9		evlslem1.e	$⊢ E = (p \in B ⟼ \underset{b \in D}{\sum_{S}} (F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
10		evlslem1.i	$⊢ φ \to I \in W$
11		evlslem1.r	$⊢ φ \to R \in CRing$
12		evlslem1.s	$⊢ φ \to S \in CRing$
13		evlslem1.f	$⊢ φ \to F \in (R RingHom S)$
14		evlslem1.g	$⊢ φ \to G : I ⟶ C$
15		evlslem1.a	$⊢ A = algSc (P)$
16		eqid	$⊢ 1_{P} = 1_{P}$
17		eqid	$⊢ 1_{S} = 1_{S}$
18		eqid	$⊢ \cdot_{P} = \cdot_{P}$
19	11	crngringd	$⊢ φ \to R \in Ring$
20	1 10 19	mplringd	$⊢ φ \to P \in Ring$
21	12	crngringd	$⊢ φ \to S \in Ring$
22		2fveq3	$⊢ x = 1_{R} \to E (A (x)) = E (A (1_{R}))$
23		fveq2	$⊢ x = 1_{R} \to F (x) = F (1_{R})$
24	22 23	eqeq12d	$⊢ x = 1_{R} \to (E (A (x)) = F (x) \leftrightarrow E (A (1_{R})) = F (1_{R}))$
25		eqid	$⊢ 0_{R} = 0_{R}$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27	10	adantr	$⊢ (φ \land x \in {Base}_{R}) \to I \in W$
28	19	adantr	$⊢ (φ \land x \in {Base}_{R}) \to R \in Ring$
29		simpr	$⊢ (φ \land x \in {Base}_{R}) \to x \in {Base}_{R}$
30	1 4 25 26 15 27 28 29	mplascl	$⊢ (φ \land x \in {Base}_{R}) \to A (x) = (y \in D ⟼ if (y = I \times \{0\}, x, 0_{R}))$
31	30	fveq2d	$⊢ (φ \land x \in {Base}_{R}) \to E (A (x)) = E ((y \in D ⟼ if (y = I \times \{0\}, x, 0_{R})))$
32	11	adantr	$⊢ (φ \land x \in {Base}_{R}) \to R \in CRing$
33	12	adantr	$⊢ (φ \land x \in {Base}_{R}) \to S \in CRing$
34	13	adantr	$⊢ (φ \land x \in {Base}_{R}) \to F \in (R RingHom S)$
35	14	adantr	$⊢ (φ \land x \in {Base}_{R}) \to G : I ⟶ C$
36	4	psrbag0	$⊢ I \in W \to I \times \{0\} \in D$
37	10 36	syl	$⊢ φ \to I \times \{0\} \in D$
38	37	adantr	$⊢ (φ \land x \in {Base}_{R}) \to I \times \{0\} \in D$
39	1 2 3 26 4 5 6 7 8 9 27 32 33 34 35 25 38 29	evlslem3	$⊢ (φ \land x \in {Base}_{R}) \to E ((y \in D ⟼ if (y = I \times \{0\}, x, 0_{R}))) = F (x) \underset{˙}{\cdot} (\sum_{T}, ((I \times \{0\}) {\underset{˙}{\times}}_{f} G))$
40		0zd	$⊢ (φ \land x \in I) \to 0 \in ℤ$
41		fvexd	$⊢ (φ \land x \in I) \to G (x) \in V$
42		fconstmpt	$⊢ I \times \{0\} = (x \in I ⟼ 0)$
43	42	a1i	$⊢ φ \to I \times \{0\} = (x \in I ⟼ 0)$
44	14	feqmptd	$⊢ φ \to G = (x \in I ⟼ G (x))$
45	10 40 41 43 44	offval2	$⊢ φ \to (I \times \{0\}) {\underset{˙}{\times}}_{f} G = (x \in I ⟼ 0 \underset{˙}{\times} G (x))$
46	14	ffvelcdmda	$⊢ (φ \land x \in I) \to G (x) \in C$
47	5 3	mgpbas	$⊢ C = {Base}_{T}$
48	5 17	ringidval	$⊢ 1_{S} = 0_{T}$
49	47 48 6	mulg0	$⊢ G (x) \in C \to 0 \underset{˙}{\times} G (x) = 1_{S}$
50	46 49	syl	$⊢ (φ \land x \in I) \to 0 \underset{˙}{\times} G (x) = 1_{S}$
51	50	mpteq2dva	$⊢ φ \to (x \in I ⟼ 0 \underset{˙}{\times} G (x)) = (x \in I ⟼ 1_{S})$
52	45 51	eqtrd	$⊢ φ \to (I \times \{0\}) {\underset{˙}{\times}}_{f} G = (x \in I ⟼ 1_{S})$
53	52	oveq2d	$⊢ φ \to \sum_{T} ((I \times \{0\}) {\underset{˙}{\times}}_{f} G) = \underset{x \in I}{\sum_{T}} 1_{S}$
54	5	crngmgp	$⊢ S \in CRing \to T \in CMnd$
55	12 54	syl	$⊢ φ \to T \in CMnd$
56	55	cmnmndd	$⊢ φ \to T \in Mnd$
57	48	gsumz	$⊢ (T \in Mnd \land I \in W) \to \underset{x \in I}{\sum_{T}} 1_{S} = 1_{S}$
58	56 10 57	syl2anc	$⊢ φ \to \underset{x \in I}{\sum_{T}} 1_{S} = 1_{S}$
59	53 58	eqtrd	$⊢ φ \to \sum_{T} ((I \times \{0\}) {\underset{˙}{\times}}_{f} G) = 1_{S}$
60	59	adantr	$⊢ (φ \land x \in {Base}_{R}) \to \sum_{T} ((I \times \{0\}) {\underset{˙}{\times}}_{f} G) = 1_{S}$
61	60	oveq2d	$⊢ (φ \land x \in {Base}_{R}) \to F (x) \underset{˙}{\cdot} (\sum_{T}, ((I \times \{0\}) {\underset{˙}{\times}}_{f} G)) = F (x) \underset{˙}{\cdot} 1_{S}$
62	26 3	rhmf	$⊢ F \in (R RingHom S) \to F : {Base}_{R} ⟶ C$
63	13 62	syl	$⊢ φ \to F : {Base}_{R} ⟶ C$
64	63	ffvelcdmda	$⊢ (φ \land x \in {Base}_{R}) \to F (x) \in C$
65	3 7 17	ringridm	$⊢ (S \in Ring \land F (x) \in C) \to F (x) \underset{˙}{\cdot} 1_{S} = F (x)$
66	21 64 65	syl2an2r	$⊢ (φ \land x \in {Base}_{R}) \to F (x) \underset{˙}{\cdot} 1_{S} = F (x)$
67	61 66	eqtrd	$⊢ (φ \land x \in {Base}_{R}) \to F (x) \underset{˙}{\cdot} (\sum_{T}, ((I \times \{0\}) {\underset{˙}{\times}}_{f} G)) = F (x)$
68	31 39 67	3eqtrd	$⊢ (φ \land x \in {Base}_{R}) \to E (A (x)) = F (x)$
69	68	ralrimiva	$⊢ φ \to \forall x \in {Base}_{R} E (A (x)) = F (x)$
70		eqid	$⊢ 1_{R} = 1_{R}$
71	26 70	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
72	19 71	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
73	24 69 72	rspcdva	$⊢ φ \to E (A (1_{R})) = F (1_{R})$
74	1	mplassa	$⊢ (I \in W \land R \in CRing) \to P \in AssAlg$
75	10 11 74	syl2anc	$⊢ φ \to P \in AssAlg$
76		eqid	$⊢ Scalar (P) = Scalar (P)$
77	15 76	asclrhm	$⊢ P \in AssAlg \to A \in (Scalar (P) RingHom P)$
78	75 77	syl	$⊢ φ \to A \in (Scalar (P) RingHom P)$
79	1 10 11	mplsca	$⊢ φ \to R = Scalar (P)$
80	79	oveq1d	$⊢ φ \to R RingHom P = Scalar (P) RingHom P$
81	78 80	eleqtrrd	$⊢ φ \to A \in (R RingHom P)$
82	70 16	rhm1	$⊢ A \in (R RingHom P) \to A (1_{R}) = 1_{P}$
83	81 82	syl	$⊢ φ \to A (1_{R}) = 1_{P}$
84	83	fveq2d	$⊢ φ \to E (A (1_{R})) = E (1_{P})$
85	70 17	rhm1	$⊢ F \in (R RingHom S) \to F (1_{R}) = 1_{S}$
86	13 85	syl	$⊢ φ \to F (1_{R}) = 1_{S}$
87	73 84 86	3eqtr3d	$⊢ φ \to E (1_{P}) = 1_{S}$
88		eqid	$⊢ +_{P} = +_{P}$
89		eqid	$⊢ +_{S} = +_{S}$
90	20	ringgrpd	$⊢ φ \to P \in Grp$
91	21	ringgrpd	$⊢ φ \to S \in Grp$
92		eqid	$⊢ 0_{S} = 0_{S}$
93		ringcmn	$⊢ S \in Ring \to S \in CMnd$
94	21 93	syl	$⊢ φ \to S \in CMnd$
95	94	adantr	$⊢ (φ \land p \in B) \to S \in CMnd$
96		ovex	$⊢ {ℕ_{0}}^{I} \in V$
97	4 96	rabex2	$⊢ D \in V$
98	97	a1i	$⊢ (φ \land p \in B) \to D \in V$
99	10	adantr	$⊢ (φ \land p \in B) \to I \in W$
100	11	adantr	$⊢ (φ \land p \in B) \to R \in CRing$
101	12	adantr	$⊢ (φ \land p \in B) \to S \in CRing$
102	13	adantr	$⊢ (φ \land p \in B) \to F \in (R RingHom S)$
103	14	adantr	$⊢ (φ \land p \in B) \to G : I ⟶ C$
104		simpr	$⊢ (φ \land p \in B) \to p \in B$
105	1 2 3 4 5 6 7 8 9 99 100 101 102 103 104	evlslem6	$⊢ (φ \land p \in B) \to ((b \in D ⟼ F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) : D ⟶ C \land {finSupp}_{0_{S}} ((b \in D ⟼ F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))))$
106	105	simpld	$⊢ (φ \land p \in B) \to (b \in D ⟼ F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) : D ⟶ C$
107	105	simprd	$⊢ (φ \land p \in B) \to {finSupp}_{0_{S}} ((b \in D ⟼ F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
108	3 92 95 98 106 107	gsumcl	$⊢ (φ \land p \in B) \to \underset{b \in D}{\sum_{S}} (F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) \in C$
109	108 9	fmptd	$⊢ φ \to E : B ⟶ C$
110		eqid	$⊢ +_{R} = +_{R}$
111		simplrl	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to x \in B$
112		simplrr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to y \in B$
113	1 2 110 88 111 112	mpladd	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to x +_{P} y = x {+_{R}}_{f} y$
114	113	fveq1d	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to (x +_{P} y) (b) = (x {+_{R}}_{f} y) (b)$
115		simprl	$⊢ (φ \land (x \in B \land y \in B)) \to x \in B$
116	1 26 2 4 115	mplelf	$⊢ (φ \land (x \in B \land y \in B)) \to x : D ⟶ {Base}_{R}$
117	116	ffnd	$⊢ (φ \land (x \in B \land y \in B)) \to x Fn D$
118	117	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to x Fn D$
119		simprr	$⊢ (φ \land (x \in B \land y \in B)) \to y \in B$
120	1 26 2 4 119	mplelf	$⊢ (φ \land (x \in B \land y \in B)) \to y : D ⟶ {Base}_{R}$
121	120	ffnd	$⊢ (φ \land (x \in B \land y \in B)) \to y Fn D$
122	121	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to y Fn D$
123	97	a1i	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to D \in V$
124		simpr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to b \in D$
125		fnfvof	$⊢ ((x Fn D \land y Fn D) \land (D \in V \land b \in D)) \to (x {+_{R}}_{f} y) (b) = x (b) +_{R} y (b)$
126	118 122 123 124 125	syl22anc	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to (x {+_{R}}_{f} y) (b) = x (b) +_{R} y (b)$
127	114 126	eqtrd	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to (x +_{P} y) (b) = x (b) +_{R} y (b)$
128	127	fveq2d	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F ((x +_{P} y) (b)) = F (x (b) +_{R} y (b))$
129		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
130	13 129	syl	$⊢ φ \to F \in (R GrpHom S)$
131	130	ad2antrr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F \in (R GrpHom S)$
132	116	ffvelcdmda	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to x (b) \in {Base}_{R}$
133	120	ffvelcdmda	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to y (b) \in {Base}_{R}$
134	26 110 89	ghmlin	$⊢ (F \in (R GrpHom S) \land x (b) \in {Base}_{R} \land y (b) \in {Base}_{R}) \to F (x (b) +_{R} y (b)) = F (x (b)) +_{S} F (y (b))$
135	131 132 133 134	syl3anc	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F (x (b) +_{R} y (b)) = F (x (b)) +_{S} F (y (b))$
136	128 135	eqtrd	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F ((x +_{P} y) (b)) = F (x (b)) +_{S} F (y (b))$
137	136	oveq1d	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) = (F (x (b)) +_{S} F (y (b))) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))$
138	21	ad2antrr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to S \in Ring$
139	63	ad2antrr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F : {Base}_{R} ⟶ C$
140	139 132	ffvelcdmd	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F (x (b)) \in C$
141	139 133	ffvelcdmd	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F (y (b)) \in C$
142	55	ad2antrr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to T \in CMnd$
143	14	ad2antrr	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to G : I ⟶ C$
144	4 47 6 142 124 143	psrbagev2	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to \sum_{T} (b {\underset{˙}{\times}}_{f} G) \in C$
145	3 89 7	ringdir	$⊢ (S \in Ring \land (F (x (b)) \in C \land F (y (b)) \in C \land \sum_{T} (b {\underset{˙}{\times}}_{f} G) \in C)) \to (F (x (b)) +_{S} F (y (b))) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) = (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) +_{S} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
146	138 140 141 144 145	syl13anc	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to (F (x (b)) +_{S} F (y (b))) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) = (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) +_{S} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
147	137 146	eqtrd	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) = (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) +_{S} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
148	147	mpteq2dva	$⊢ (φ \land (x \in B \land y \in B)) \to (b \in D ⟼ F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (b \in D ⟼ (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) +_{S} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
149	97	a1i	$⊢ (φ \land (x \in B \land y \in B)) \to D \in V$
150		ovexd	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) \in V$
151		ovexd	$⊢ ((φ \land (x \in B \land y \in B)) \land b \in D) \to F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) \in V$
152		eqidd	$⊢ (φ \land (x \in B \land y \in B)) \to (b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
153		eqidd	$⊢ (φ \land (x \in B \land y \in B)) \to (b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
154	149 150 151 152 153	offval2	$⊢ (φ \land (x \in B \land y \in B)) \to (b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) {+_{S}}_{f} (b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (b \in D ⟼ (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) +_{S} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
155	148 154	eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to (b \in D ⟼ F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) {+_{S}}_{f} (b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
156	155	oveq2d	$⊢ (φ \land (x \in B \land y \in B)) \to \underset{b \in D}{\sum_{S}} (F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = \sum_{S} ((b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) {+_{S}}_{f} (b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
157	94	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to S \in CMnd$
158	10	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to I \in W$
159	11	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to R \in CRing$
160	12	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to S \in CRing$
161	13	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to F \in (R RingHom S)$
162	14	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to G : I ⟶ C$
163	1 2 3 4 5 6 7 8 9 158 159 160 161 162 115	evlslem6	$⊢ (φ \land (x \in B \land y \in B)) \to ((b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) : D ⟶ C \land {finSupp}_{0_{S}} ((b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))))$
164	163	simpld	$⊢ (φ \land (x \in B \land y \in B)) \to (b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) : D ⟶ C$
165	1 2 3 4 5 6 7 8 9 158 159 160 161 162 119	evlslem6	$⊢ (φ \land (x \in B \land y \in B)) \to ((b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) : D ⟶ C \land {finSupp}_{0_{S}} ((b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))))$
166	165	simpld	$⊢ (φ \land (x \in B \land y \in B)) \to (b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) : D ⟶ C$
167	163	simprd	$⊢ (φ \land (x \in B \land y \in B)) \to {finSupp}_{0_{S}} ((b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
168	165	simprd	$⊢ (φ \land (x \in B \land y \in B)) \to {finSupp}_{0_{S}} ((b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
169	3 92 89 157 149 164 166 167 168	gsumadd	$⊢ (φ \land (x \in B \land y \in B)) \to \sum_{S} ((b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) {+_{S}}_{f} (b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))) = (\underset{b \in D}{\sum_{S}}, (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))) +_{S} (\underset{b \in D}{\sum_{S}}, (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
170	156 169	eqtrd	$⊢ (φ \land (x \in B \land y \in B)) \to \underset{b \in D}{\sum_{S}} (F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (\underset{b \in D}{\sum_{S}}, (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))) +_{S} (\underset{b \in D}{\sum_{S}}, (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
171	90	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to P \in Grp$
172	2 88	grpcl	$⊢ (P \in Grp \land x \in B \land y \in B) \to x +_{P} y \in B$
173	171 115 119 172	syl3anc	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{P} y \in B$
174		fveq1	$⊢ p = x +_{P} y \to p (b) = (x +_{P} y) (b)$
175	174	fveq2d	$⊢ p = x +_{P} y \to F (p (b)) = F ((x +_{P} y) (b))$
176	175	oveq1d	$⊢ p = x +_{P} y \to F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) = F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))$
177	176	mpteq2dv	$⊢ p = x +_{P} y \to (b \in D ⟼ F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (b \in D ⟼ F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
178	177	oveq2d	$⊢ p = x +_{P} y \to \underset{b \in D}{\sum_{S}} (F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = \underset{b \in D}{\sum_{S}} (F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
179		ovex	$⊢ \underset{b \in D}{\sum_{S}} (F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) \in V$
180	178 9 179	fvmpt	$⊢ x +_{P} y \in B \to E (x +_{P} y) = \underset{b \in D}{\sum_{S}} (F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
181	173 180	syl	$⊢ (φ \land (x \in B \land y \in B)) \to E (x +_{P} y) = \underset{b \in D}{\sum_{S}} (F ((x +_{P} y) (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
182		fveq1	$⊢ p = x \to p (b) = x (b)$
183	182	fveq2d	$⊢ p = x \to F (p (b)) = F (x (b))$
184	183	oveq1d	$⊢ p = x \to F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) = F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))$
185	184	mpteq2dv	$⊢ p = x \to (b \in D ⟼ F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (b \in D ⟼ F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
186	185	oveq2d	$⊢ p = x \to \underset{b \in D}{\sum_{S}} (F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = \underset{b \in D}{\sum_{S}} (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
187		ovex	$⊢ \underset{b \in D}{\sum_{S}} (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) \in V$
188	186 9 187	fvmpt	$⊢ x \in B \to E (x) = \underset{b \in D}{\sum_{S}} (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
189	115 188	syl	$⊢ (φ \land (x \in B \land y \in B)) \to E (x) = \underset{b \in D}{\sum_{S}} (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
190		fveq1	$⊢ p = y \to p (b) = y (b)$
191	190	fveq2d	$⊢ p = y \to F (p (b)) = F (y (b))$
192	191	oveq1d	$⊢ p = y \to F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)) = F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))$
193	192	mpteq2dv	$⊢ p = y \to (b \in D ⟼ F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = (b \in D ⟼ F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
194	193	oveq2d	$⊢ p = y \to \underset{b \in D}{\sum_{S}} (F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) = \underset{b \in D}{\sum_{S}} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
195		ovex	$⊢ \underset{b \in D}{\sum_{S}} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) \in V$
196	194 9 195	fvmpt	$⊢ y \in B \to E (y) = \underset{b \in D}{\sum_{S}} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
197	196	ad2antll	$⊢ (φ \land (x \in B \land y \in B)) \to E (y) = \underset{b \in D}{\sum_{S}} (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))$
198	189 197	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to E (x) +_{S} E (y) = (\underset{b \in D}{\sum_{S}}, (F (x (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G)))) +_{S} (\underset{b \in D}{\sum_{S}}, (F (y (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))))$
199	170 181 198	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to E (x +_{P} y) = E (x) +_{S} E (y)$
200	2 3 88 89 90 91 109 199	isghmd	$⊢ φ \to E \in (P GrpHom S)$
201		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
202	201 5	rhmmhm	$⊢ F \in (R RingHom S) \to F \in ({mulGrp}_{R} MndHom T)$
203	13 202	syl	$⊢ φ \to F \in ({mulGrp}_{R} MndHom T)$
204	203	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to F \in ({mulGrp}_{R} MndHom T)$
205		simprll	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to x \in B$
206	1 26 2 4 205	mplelf	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to x : D ⟶ {Base}_{R}$
207		simprrl	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to z \in D$
208	206 207	ffvelcdmd	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to x (z) \in {Base}_{R}$
209		simprlr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to y \in B$
210	1 26 2 4 209	mplelf	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to y : D ⟶ {Base}_{R}$
211		simprrr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to w \in D$
212	210 211	ffvelcdmd	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to y (w) \in {Base}_{R}$
213	201 26	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
214		eqid	$⊢ \cdot_{R} = \cdot_{R}$
215	201 214	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
216	5 7	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{T}$
217	213 215 216	mhmlin	$⊢ (F \in ({mulGrp}_{R} MndHom T) \land x (z) \in {Base}_{R} \land y (w) \in {Base}_{R}) \to F (x (z) \cdot_{R} y (w)) = F (x (z)) \underset{˙}{\cdot} F (y (w))$
218	204 208 212 217	syl3anc	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to F (x (z) \cdot_{R} y (w)) = F (x (z)) \underset{˙}{\cdot} F (y (w))$
219	56	ad2antrr	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to T \in Mnd$
220		simprl	$⊢ (φ \land (z \in D \land w \in D)) \to z \in D$
221	4	psrbagf	$⊢ z \in D \to z : I ⟶ ℕ_{0}$
222	220 221	syl	$⊢ (φ \land (z \in D \land w \in D)) \to z : I ⟶ ℕ_{0}$
223	222	ffvelcdmda	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to z (v) \in ℕ_{0}$
224	4	psrbagf	$⊢ w \in D \to w : I ⟶ ℕ_{0}$
225	224	ad2antll	$⊢ (φ \land (z \in D \land w \in D)) \to w : I ⟶ ℕ_{0}$
226	225	ffvelcdmda	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to w (v) \in ℕ_{0}$
227	14	adantr	$⊢ (φ \land (z \in D \land w \in D)) \to G : I ⟶ C$
228	227	ffvelcdmda	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to G (v) \in C$
229	47 6 216	mulgnn0dir	$⊢ (T \in Mnd \land (z (v) \in ℕ_{0} \land w (v) \in ℕ_{0} \land G (v) \in C)) \to (z (v) + w (v)) \underset{˙}{\times} G (v) = (z (v) \underset{˙}{\times} G (v)) \underset{˙}{\cdot} (w (v) \underset{˙}{\times} G (v))$
230	219 223 226 228 229	syl13anc	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to (z (v) + w (v)) \underset{˙}{\times} G (v) = (z (v) \underset{˙}{\times} G (v)) \underset{˙}{\cdot} (w (v) \underset{˙}{\times} G (v))$
231	230	mpteq2dva	$⊢ (φ \land (z \in D \land w \in D)) \to (v \in I ⟼ (z (v) + w (v)) \underset{˙}{\times} G (v)) = (v \in I ⟼ (z (v) \underset{˙}{\times} G (v)) \underset{˙}{\cdot} (w (v) \underset{˙}{\times} G (v)))$
232	10	adantr	$⊢ (φ \land (z \in D \land w \in D)) \to I \in W$
233		ovexd	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to z (v) + w (v) \in V$
234		fvexd	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to G (v) \in V$
235	222	ffnd	$⊢ (φ \land (z \in D \land w \in D)) \to z Fn I$
236	225	ffnd	$⊢ (φ \land (z \in D \land w \in D)) \to w Fn I$
237		inidm	$⊢ I \cap I = I$
238		eqidd	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to z (v) = z (v)$
239		eqidd	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to w (v) = w (v)$
240	235 236 232 232 237 238 239	offval	$⊢ (φ \land (z \in D \land w \in D)) \to z +_{f} w = (v \in I ⟼ z (v) + w (v))$
241	14	feqmptd	$⊢ φ \to G = (v \in I ⟼ G (v))$
242	241	adantr	$⊢ (φ \land (z \in D \land w \in D)) \to G = (v \in I ⟼ G (v))$
243	232 233 234 240 242	offval2	$⊢ (φ \land (z \in D \land w \in D)) \to (z +_{f} w) {\underset{˙}{\times}}_{f} G = (v \in I ⟼ (z (v) + w (v)) \underset{˙}{\times} G (v))$
244		ovexd	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to z (v) \underset{˙}{\times} G (v) \in V$
245		ovexd	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to w (v) \underset{˙}{\times} G (v) \in V$
246	14	ffnd	$⊢ φ \to G Fn I$
247	246	adantr	$⊢ (φ \land (z \in D \land w \in D)) \to G Fn I$
248		eqidd	$⊢ ((φ \land (z \in D \land w \in D)) \land v \in I) \to G (v) = G (v)$
249	235 247 232 232 237 238 248	offval	$⊢ (φ \land (z \in D \land w \in D)) \to z {\underset{˙}{\times}}_{f} G = (v \in I ⟼ z (v) \underset{˙}{\times} G (v))$
250	236 247 232 232 237 239 248	offval	$⊢ (φ \land (z \in D \land w \in D)) \to w {\underset{˙}{\times}}_{f} G = (v \in I ⟼ w (v) \underset{˙}{\times} G (v))$
251	232 244 245 249 250	offval2	$⊢ (φ \land (z \in D \land w \in D)) \to (z {\underset{˙}{\times}}_{f} G) {\underset{˙}{\cdot}}_{f} (w {\underset{˙}{\times}}_{f} G) = (v \in I ⟼ (z (v) \underset{˙}{\times} G (v)) \underset{˙}{\cdot} (w (v) \underset{˙}{\times} G (v)))$
252	231 243 251	3eqtr4d	$⊢ (φ \land (z \in D \land w \in D)) \to (z +_{f} w) {\underset{˙}{\times}}_{f} G = (z {\underset{˙}{\times}}_{f} G) {\underset{˙}{\cdot}}_{f} (w {\underset{˙}{\times}}_{f} G)$
253	252	oveq2d	$⊢ (φ \land (z \in D \land w \in D)) \to \sum_{T} ((z +_{f} w) {\underset{˙}{\times}}_{f} G) = \sum_{T} ((z {\underset{˙}{\times}}_{f} G) {\underset{˙}{\cdot}}_{f} (w {\underset{˙}{\times}}_{f} G))$
254	55	adantr	$⊢ (φ \land (z \in D \land w \in D)) \to T \in CMnd$
255	4 47 6 48 254 220 227	psrbagev1	$⊢ (φ \land (z \in D \land w \in D)) \to ((z {\underset{˙}{\times}}_{f} G) : I ⟶ C \land {finSupp}_{1_{S}} ((z {\underset{˙}{\times}}_{f} G)))$
256	255	simpld	$⊢ (φ \land (z \in D \land w \in D)) \to (z {\underset{˙}{\times}}_{f} G) : I ⟶ C$
257		simprr	$⊢ (φ \land (z \in D \land w \in D)) \to w \in D$
258	4 47 6 48 254 257 227	psrbagev1	$⊢ (φ \land (z \in D \land w \in D)) \to ((w {\underset{˙}{\times}}_{f} G) : I ⟶ C \land {finSupp}_{1_{S}} ((w {\underset{˙}{\times}}_{f} G)))$
259	258	simpld	$⊢ (φ \land (z \in D \land w \in D)) \to (w {\underset{˙}{\times}}_{f} G) : I ⟶ C$
260	255	simprd	$⊢ (φ \land (z \in D \land w \in D)) \to {finSupp}_{1_{S}} ((z {\underset{˙}{\times}}_{f} G))$
261	258	simprd	$⊢ (φ \land (z \in D \land w \in D)) \to {finSupp}_{1_{S}} ((w {\underset{˙}{\times}}_{f} G))$
262	47 48 216 254 232 256 259 260 261	gsumadd	$⊢ (φ \land (z \in D \land w \in D)) \to \sum_{T} ((z {\underset{˙}{\times}}_{f} G) {\underset{˙}{\cdot}}_{f} (w {\underset{˙}{\times}}_{f} G)) = (\sum_{T}, (z {\underset{˙}{\times}}_{f} G)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G))$
263	253 262	eqtrd	$⊢ (φ \land (z \in D \land w \in D)) \to \sum_{T} ((z +_{f} w) {\underset{˙}{\times}}_{f} G) = (\sum_{T}, (z {\underset{˙}{\times}}_{f} G)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G))$
264	263	adantrl	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to \sum_{T} ((z +_{f} w) {\underset{˙}{\times}}_{f} G) = (\sum_{T}, (z {\underset{˙}{\times}}_{f} G)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G))$
265	218 264	oveq12d	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to F (x (z) \cdot_{R} y (w)) \underset{˙}{\cdot} (\sum_{T}, ((z +_{f} w) {\underset{˙}{\times}}_{f} G)) = (F (x (z)) \underset{˙}{\cdot} F (y (w))) \underset{˙}{\cdot} ((\sum_{T}, (z {\underset{˙}{\times}}_{f} G)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G)))$
266	55	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to T \in CMnd$
267	63	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to F : {Base}_{R} ⟶ C$
268	267 208	ffvelcdmd	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to F (x (z)) \in C$
269	267 212	ffvelcdmd	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to F (y (w)) \in C$
270	4 47 6 254 220 227	psrbagev2	$⊢ (φ \land (z \in D \land w \in D)) \to \sum_{T} (z {\underset{˙}{\times}}_{f} G) \in C$
271	270	adantrl	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to \sum_{T} (z {\underset{˙}{\times}}_{f} G) \in C$
272	4 47 6 254 257 227	psrbagev2	$⊢ (φ \land (z \in D \land w \in D)) \to \sum_{T} (w {\underset{˙}{\times}}_{f} G) \in C$
273	272	adantrl	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to \sum_{T} (w {\underset{˙}{\times}}_{f} G) \in C$
274	47 216	cmn4	$⊢ (T \in CMnd \land (F (x (z)) \in C \land F (y (w)) \in C) \land (\sum_{T} (z {\underset{˙}{\times}}_{f} G) \in C \land \sum_{T} (w {\underset{˙}{\times}}_{f} G) \in C)) \to (F (x (z)) \underset{˙}{\cdot} F (y (w))) \underset{˙}{\cdot} ((\sum_{T}, (z {\underset{˙}{\times}}_{f} G)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G))) = (F (x (z)) \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\times}}_{f} G))) \underset{˙}{\cdot} (F (y (w)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G)))$
275	266 268 269 271 273 274	syl122anc	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to (F (x (z)) \underset{˙}{\cdot} F (y (w))) \underset{˙}{\cdot} ((\sum_{T}, (z {\underset{˙}{\times}}_{f} G)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G))) = (F (x (z)) \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\times}}_{f} G))) \underset{˙}{\cdot} (F (y (w)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G)))$
276	265 275	eqtrd	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to F (x (z) \cdot_{R} y (w)) \underset{˙}{\cdot} (\sum_{T}, ((z +_{f} w) {\underset{˙}{\times}}_{f} G)) = (F (x (z)) \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\times}}_{f} G))) \underset{˙}{\cdot} (F (y (w)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G)))$
277	10	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to I \in W$
278	11	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to R \in CRing$
279	12	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to S \in CRing$
280	13	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to F \in (R RingHom S)$
281	14	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to G : I ⟶ C$
282	4	psrbagaddcl	$⊢ (z \in D \land w \in D) \to z +_{f} w \in D$
283	282	ad2antll	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to z +_{f} w \in D$
284	19	adantr	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to R \in Ring$
285	26 214	ringcl	$⊢ (R \in Ring \land x (z) \in {Base}_{R} \land y (w) \in {Base}_{R}) \to x (z) \cdot_{R} y (w) \in {Base}_{R}$
286	284 208 212 285	syl3anc	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to x (z) \cdot_{R} y (w) \in {Base}_{R}$
287	1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 283 286	evlslem3	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to E ((v \in D ⟼ if (v = z +_{f} w, x (z) \cdot_{R} y (w), 0_{R}))) = F (x (z) \cdot_{R} y (w)) \underset{˙}{\cdot} (\sum_{T}, ((z +_{f} w) {\underset{˙}{\times}}_{f} G))$
288	1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 207 208	evlslem3	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to E ((v \in D ⟼ if (v = z, x (z), 0_{R}))) = F (x (z)) \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\times}}_{f} G))$
289	1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 211 212	evlslem3	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to E ((v \in D ⟼ if (v = w, y (w), 0_{R}))) = F (y (w)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G))$
290	288 289	oveq12d	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to E ((v \in D ⟼ if (v = z, x (z), 0_{R}))) \underset{˙}{\cdot} E ((v \in D ⟼ if (v = w, y (w), 0_{R}))) = (F (x (z)) \underset{˙}{\cdot} (\sum_{T}, (z {\underset{˙}{\times}}_{f} G))) \underset{˙}{\cdot} (F (y (w)) \underset{˙}{\cdot} (\sum_{T}, (w {\underset{˙}{\times}}_{f} G)))$
291	276 287 290	3eqtr4d	$⊢ (φ \land ((x \in B \land y \in B) \land (z \in D \land w \in D))) \to E ((v \in D ⟼ if (v = z +_{f} w, x (z) \cdot_{R} y (w), 0_{R}))) = E ((v \in D ⟼ if (v = z, x (z), 0_{R}))) \underset{˙}{\cdot} E ((v \in D ⟼ if (v = w, y (w), 0_{R})))$
292	1 2 7 25 4 10 11 12 200 291	evlslem2	$⊢ (φ \land (x \in B \land y \in B)) \to E (x \cdot_{P} y) = E (x) \underset{˙}{\cdot} E (y)$
293	2 16 17 18 7 20 21 87 292 3 88 89 109 199	isrhmd	$⊢ φ \to E \in (P RingHom S)$
294		ovex	$⊢ \underset{b \in D}{\sum_{S}} (F (p (b)) \underset{˙}{\cdot} (\sum_{T}, (b {\underset{˙}{\times}}_{f} G))) \in V$
295	294 9	fnmpti	$⊢ E Fn B$
296	295	a1i	$⊢ φ \to E Fn B$
297	26 2	rhmf	$⊢ A \in (R RingHom P) \to A : {Base}_{R} ⟶ B$
298	81 297	syl	$⊢ φ \to A : {Base}_{R} ⟶ B$
299	298	ffnd	$⊢ φ \to A Fn {Base}_{R}$
300	298	frnd	$⊢ φ \to ran A \subseteq B$
301		fnco	$⊢ (E Fn B \land A Fn {Base}_{R} \land ran A \subseteq B) \to (E \circ A) Fn {Base}_{R}$
302	296 299 300 301	syl3anc	$⊢ φ \to (E \circ A) Fn {Base}_{R}$
303	63	ffnd	$⊢ φ \to F Fn {Base}_{R}$
304		fvco2	$⊢ (A Fn {Base}_{R} \land x \in {Base}_{R}) \to (E \circ A) (x) = E (A (x))$
305	299 304	sylan	$⊢ (φ \land x \in {Base}_{R}) \to (E \circ A) (x) = E (A (x))$
306	305 68	eqtrd	$⊢ (φ \land x \in {Base}_{R}) \to (E \circ A) (x) = F (x)$
307	302 303 306	eqfnfvd	$⊢ φ \to E \circ A = F$
308	1 8 2 10 19	mvrf2	$⊢ φ \to V : I ⟶ B$
309	308	ffnd	$⊢ φ \to V Fn I$
310	308	frnd	$⊢ φ \to ran V \subseteq B$
311		fnco	$⊢ (E Fn B \land V Fn I \land ran V \subseteq B) \to (E \circ V) Fn I$
312	296 309 310 311	syl3anc	$⊢ φ \to (E \circ V) Fn I$
313		fvco2	$⊢ (V Fn I \land x \in I) \to (E \circ V) (x) = E (V (x))$
314	309 313	sylan	$⊢ (φ \land x \in I) \to (E \circ V) (x) = E (V (x))$
315	10	adantr	$⊢ (φ \land x \in I) \to I \in W$
316	11	adantr	$⊢ (φ \land x \in I) \to R \in CRing$
317		simpr	$⊢ (φ \land x \in I) \to x \in I$
318	8 4 25 70 315 316 317	mvrval	$⊢ (φ \land x \in I) \to V (x) = (y \in D ⟼ if (y = (z \in I ⟼ if (z = x, 1, 0)), 1_{R}, 0_{R}))$
319	318	fveq2d	$⊢ (φ \land x \in I) \to E (V (x)) = E ((y \in D ⟼ if (y = (z \in I ⟼ if (z = x, 1, 0)), 1_{R}, 0_{R})))$
320	12	adantr	$⊢ (φ \land x \in I) \to S \in CRing$
321	13	adantr	$⊢ (φ \land x \in I) \to F \in (R RingHom S)$
322	14	adantr	$⊢ (φ \land x \in I) \to G : I ⟶ C$
323	4	psrbagsn	$⊢ I \in W \to (z \in I ⟼ if (z = x, 1, 0)) \in D$
324	10 323	syl	$⊢ φ \to (z \in I ⟼ if (z = x, 1, 0)) \in D$
325	324	adantr	$⊢ (φ \land x \in I) \to (z \in I ⟼ if (z = x, 1, 0)) \in D$
326	72	adantr	$⊢ (φ \land x \in I) \to 1_{R} \in {Base}_{R}$
327	1 2 3 26 4 5 6 7 8 9 315 316 320 321 322 25 325 326	evlslem3	$⊢ (φ \land x \in I) \to E ((y \in D ⟼ if (y = (z \in I ⟼ if (z = x, 1, 0)), 1_{R}, 0_{R}))) = F (1_{R}) \underset{˙}{\cdot} (\sum_{T}, ((z \in I ⟼ if (z = x, 1, 0)) {\underset{˙}{\times}}_{f} G))$
328	86	adantr	$⊢ (φ \land x \in I) \to F (1_{R}) = 1_{S}$
329		1nn0	$⊢ 1 \in ℕ_{0}$
330		0nn0	$⊢ 0 \in ℕ_{0}$
331	329 330	ifcli	$⊢ if (z = x, 1, 0) \in ℕ_{0}$
332	331	a1i	$⊢ (φ \land z \in I) \to if (z = x, 1, 0) \in ℕ_{0}$
333	14	ffvelcdmda	$⊢ (φ \land z \in I) \to G (z) \in C$
334		eqidd	$⊢ φ \to (z \in I ⟼ if (z = x, 1, 0)) = (z \in I ⟼ if (z = x, 1, 0))$
335	14	feqmptd	$⊢ φ \to G = (z \in I ⟼ G (z))$
336	10 332 333 334 335	offval2	$⊢ φ \to (z \in I ⟼ if (z = x, 1, 0)) {\underset{˙}{\times}}_{f} G = (z \in I ⟼ if (z = x, 1, 0) \underset{˙}{\times} G (z))$
337		oveq1	$⊢ 1 = if (z = x, 1, 0) \to 1 \underset{˙}{\times} G (z) = if (z = x, 1, 0) \underset{˙}{\times} G (z)$
338	337	eqeq1d	$⊢ 1 = if (z = x, 1, 0) \to (1 \underset{˙}{\times} G (z) = if (z = x, G (z), 1_{S}) \leftrightarrow if (z = x, 1, 0) \underset{˙}{\times} G (z) = if (z = x, G (z), 1_{S}))$
339		oveq1	$⊢ 0 = if (z = x, 1, 0) \to 0 \underset{˙}{\times} G (z) = if (z = x, 1, 0) \underset{˙}{\times} G (z)$
340	339	eqeq1d	$⊢ 0 = if (z = x, 1, 0) \to (0 \underset{˙}{\times} G (z) = if (z = x, G (z), 1_{S}) \leftrightarrow if (z = x, 1, 0) \underset{˙}{\times} G (z) = if (z = x, G (z), 1_{S}))$
341	333	adantr	$⊢ ((φ \land z \in I) \land z = x) \to G (z) \in C$
342	47 6	mulg1	$⊢ G (z) \in C \to 1 \underset{˙}{\times} G (z) = G (z)$
343	341 342	syl	$⊢ ((φ \land z \in I) \land z = x) \to 1 \underset{˙}{\times} G (z) = G (z)$
344		iftrue	$⊢ z = x \to if (z = x, G (z), 1_{S}) = G (z)$
345	344	adantl	$⊢ ((φ \land z \in I) \land z = x) \to if (z = x, G (z), 1_{S}) = G (z)$
346	343 345	eqtr4d	$⊢ ((φ \land z \in I) \land z = x) \to 1 \underset{˙}{\times} G (z) = if (z = x, G (z), 1_{S})$
347	47 48 6	mulg0	$⊢ G (z) \in C \to 0 \underset{˙}{\times} G (z) = 1_{S}$
348	333 347	syl	$⊢ (φ \land z \in I) \to 0 \underset{˙}{\times} G (z) = 1_{S}$
349	348	adantr	$⊢ ((φ \land z \in I) \land \neg z = x) \to 0 \underset{˙}{\times} G (z) = 1_{S}$
350		iffalse	$⊢ \neg z = x \to if (z = x, G (z), 1_{S}) = 1_{S}$
351	350	adantl	$⊢ ((φ \land z \in I) \land \neg z = x) \to if (z = x, G (z), 1_{S}) = 1_{S}$
352	349 351	eqtr4d	$⊢ ((φ \land z \in I) \land \neg z = x) \to 0 \underset{˙}{\times} G (z) = if (z = x, G (z), 1_{S})$
353	338 340 346 352	ifbothda	$⊢ (φ \land z \in I) \to if (z = x, 1, 0) \underset{˙}{\times} G (z) = if (z = x, G (z), 1_{S})$
354	353	mpteq2dva	$⊢ φ \to (z \in I ⟼ if (z = x, 1, 0) \underset{˙}{\times} G (z)) = (z \in I ⟼ if (z = x, G (z), 1_{S}))$
355	336 354	eqtrd	$⊢ φ \to (z \in I ⟼ if (z = x, 1, 0)) {\underset{˙}{\times}}_{f} G = (z \in I ⟼ if (z = x, G (z), 1_{S}))$
356	355	adantr	$⊢ (φ \land x \in I) \to (z \in I ⟼ if (z = x, 1, 0)) {\underset{˙}{\times}}_{f} G = (z \in I ⟼ if (z = x, G (z), 1_{S}))$
357	356	oveq2d	$⊢ (φ \land x \in I) \to \sum_{T} ((z \in I ⟼ if (z = x, 1, 0)) {\underset{˙}{\times}}_{f} G) = \underset{z \in I}{\sum_{T}} if (z = x, G (z), 1_{S})$
358	56	adantr	$⊢ (φ \land x \in I) \to T \in Mnd$
359	333	adantlr	$⊢ ((φ \land x \in I) \land z \in I) \to G (z) \in C$
360	3 17	ringidcl	$⊢ S \in Ring \to 1_{S} \in C$
361	21 360	syl	$⊢ φ \to 1_{S} \in C$
362	361	ad2antrr	$⊢ ((φ \land x \in I) \land z \in I) \to 1_{S} \in C$
363	359 362	ifcld	$⊢ ((φ \land x \in I) \land z \in I) \to if (z = x, G (z), 1_{S}) \in C$
364	363	fmpttd	$⊢ (φ \land x \in I) \to (z \in I ⟼ if (z = x, G (z), 1_{S})) : I ⟶ C$
365		eldifsnneq	$⊢ z \in (I ∖ \{x\}) \to \neg z = x$
366	365 350	syl	$⊢ z \in (I ∖ \{x\}) \to if (z = x, G (z), 1_{S}) = 1_{S}$
367	366	adantl	$⊢ ((φ \land x \in I) \land z \in (I ∖ \{x\})) \to if (z = x, G (z), 1_{S}) = 1_{S}$
368	367 315	suppss2	$⊢ (φ \land x \in I) \to (z \in I ⟼ if (z = x, G (z), 1_{S})) supp 1_{S} \subseteq \{x\}$
369	47 48 358 315 317 364 368	gsumpt	$⊢ (φ \land x \in I) \to \underset{z \in I}{\sum_{T}} if (z = x, G (z), 1_{S}) = (z \in I ⟼ if (z = x, G (z), 1_{S})) (x)$
370		fveq2	$⊢ z = x \to G (z) = G (x)$
371	344 370	eqtrd	$⊢ z = x \to if (z = x, G (z), 1_{S}) = G (x)$
372		eqid	$⊢ (z \in I ⟼ if (z = x, G (z), 1_{S})) = (z \in I ⟼ if (z = x, G (z), 1_{S}))$
373		fvex	$⊢ G (x) \in V$
374	371 372 373	fvmpt	$⊢ x \in I \to (z \in I ⟼ if (z = x, G (z), 1_{S})) (x) = G (x)$
375	374	adantl	$⊢ (φ \land x \in I) \to (z \in I ⟼ if (z = x, G (z), 1_{S})) (x) = G (x)$
376	357 369 375	3eqtrd	$⊢ (φ \land x \in I) \to \sum_{T} ((z \in I ⟼ if (z = x, 1, 0)) {\underset{˙}{\times}}_{f} G) = G (x)$
377	328 376	oveq12d	$⊢ (φ \land x \in I) \to F (1_{R}) \underset{˙}{\cdot} (\sum_{T}, ((z \in I ⟼ if (z = x, 1, 0)) {\underset{˙}{\times}}_{f} G)) = 1_{S} \underset{˙}{\cdot} G (x)$
378	3 7 17	ringlidm	$⊢ (S \in Ring \land G (x) \in C) \to 1_{S} \underset{˙}{\cdot} G (x) = G (x)$
379	21 46 378	syl2an2r	$⊢ (φ \land x \in I) \to 1_{S} \underset{˙}{\cdot} G (x) = G (x)$
380	377 379	eqtrd	$⊢ (φ \land x \in I) \to F (1_{R}) \underset{˙}{\cdot} (\sum_{T}, ((z \in I ⟼ if (z = x, 1, 0)) {\underset{˙}{\times}}_{f} G)) = G (x)$
381	319 327 380	3eqtrd	$⊢ (φ \land x \in I) \to E (V (x)) = G (x)$
382	314 381	eqtrd	$⊢ (φ \land x \in I) \to (E \circ V) (x) = G (x)$
383	312 246 382	eqfnfvd	$⊢ φ \to E \circ V = G$
384	293 307 383	3jca	$⊢ φ \to (E \in (P RingHom S) \land E \circ A = F \land E \circ V = G)$

Metamath Proof Explorer

Theorem evlslem1

Proof