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

Metamath Proof Explorer

Theorem evlslem1

Proof