MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  evlslem1 Structured version   Visualization version   GIF version

Theorem evlslem1 22093
Description: Lemma for evlseu 22094, 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 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ 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.
StepHypRef Expression
1 evlslem1.b . . 3 𝐵 = (Base‘𝑃)
2 eqid 2726 . . 3 (1r𝑃) = (1r𝑃)
3 eqid 2726 . . 3 (1r𝑆) = (1r𝑆)
4 eqid 2726 . . 3 (.r𝑃) = (.r𝑃)
5 evlslem1.m . . 3 · = (.r𝑆)
6 evlslem1.p . . . 4 𝑃 = (𝐼 mPoly 𝑅)
7 evlslem1.i . . . 4 (𝜑𝐼𝑊)
8 evlslem1.r . . . . 5 (𝜑𝑅 ∈ CRing)
98crngringd 20225 . . . 4 (𝜑𝑅 ∈ Ring)
106, 7, 9mplringd 22028 . . 3 (𝜑𝑃 ∈ Ring)
11 evlslem1.s . . . 4 (𝜑𝑆 ∈ CRing)
1211crngringd 20225 . . 3 (𝜑𝑆 ∈ Ring)
13 2fveq3 6898 . . . . . 6 (𝑥 = (1r𝑅) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝐴‘(1r𝑅))))
14 fveq2 6893 . . . . . 6 (𝑥 = (1r𝑅) → (𝐹𝑥) = (𝐹‘(1r𝑅)))
1513, 14eqeq12d 2742 . . . . 5 (𝑥 = (1r𝑅) → ((𝐸‘(𝐴𝑥)) = (𝐹𝑥) ↔ (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅))))
16 evlslem1.d . . . . . . . . 9 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
17 eqid 2726 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
18 eqid 2726 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
19 evlslem1.a . . . . . . . . 9 𝐴 = (algSc‘𝑃)
207adantr 479 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐼𝑊)
219adantr 479 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
22 simpr 483 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅))
236, 16, 17, 18, 19, 20, 21, 22mplascl 22073 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐴𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅))))
2423fveq2d 6897 . . . . . . 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 𝐺))))))
308adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing)
3111adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing)
32 evlslem1.f . . . . . . . . 9 (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
3332adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
34 evlslem1.g . . . . . . . . 9 (𝜑𝐺:𝐼𝐶)
3534adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼𝐶)
3616psrbag0 22071 . . . . . . . . . 10 (𝐼𝑊 → (𝐼 × {0}) ∈ 𝐷)
377, 36syl 17 . . . . . . . . 9 (𝜑 → (𝐼 × {0}) ∈ 𝐷)
3837adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷)
396, 1, 25, 18, 16, 26, 27, 5, 28, 29, 20, 30, 31, 33, 35, 17, 38, 22evlslem3 22091 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))) = ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))))
40 0zd 12616 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → 0 ∈ ℤ)
41 fvexd 6908 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ V)
42 fconstmpt 5736 . . . . . . . . . . . . . . 15 (𝐼 × {0}) = (𝑥𝐼 ↦ 0)
4342a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 × {0}) = (𝑥𝐼 ↦ 0))
4434feqmptd 6963 . . . . . . . . . . . . . 14 (𝜑𝐺 = (𝑥𝐼 ↦ (𝐺𝑥)))
457, 40, 41, 43, 44offval2 7702 . . . . . . . . . . . . 13 (𝜑 → ((𝐼 × {0}) ∘f 𝐺) = (𝑥𝐼 ↦ (0 (𝐺𝑥))))
4634ffvelcdmda 7090 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ 𝐶)
4726, 25mgpbas 20119 . . . . . . . . . . . . . . . 16 𝐶 = (Base‘𝑇)
4826, 3ringidval 20162 . . . . . . . . . . . . . . . 16 (1r𝑆) = (0g𝑇)
4947, 48, 27mulg0 19064 . . . . . . . . . . . . . . 15 ((𝐺𝑥) ∈ 𝐶 → (0 (𝐺𝑥)) = (1r𝑆))
5046, 49syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (0 (𝐺𝑥)) = (1r𝑆))
5150mpteq2dva 5245 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝐼 ↦ (0 (𝐺𝑥))) = (𝑥𝐼 ↦ (1r𝑆)))
5245, 51eqtrd 2766 . . . . . . . . . . . 12 (𝜑 → ((𝐼 × {0}) ∘f 𝐺) = (𝑥𝐼 ↦ (1r𝑆)))
5352oveq2d 7432 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))))
5426crngmgp 20220 . . . . . . . . . . . . . 14 (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
5511, 54syl 17 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ CMnd)
5655cmnmndd 19798 . . . . . . . . . . . 12 (𝜑𝑇 ∈ Mnd)
5748gsumz 18821 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝐼𝑊) → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
5856, 7, 57syl2anc 582 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
5953, 58eqtrd 2766 . . . . . . . . . 10 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (1r𝑆))
6059adantr 479 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (1r𝑆))
6160oveq2d 7432 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))) = ((𝐹𝑥) · (1r𝑆)))
6218, 25rhmf 20463 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶)
6332, 62syl 17 . . . . . . . . . 10 (𝜑𝐹:(Base‘𝑅)⟶𝐶)
6463ffvelcdmda 7090 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐹𝑥) ∈ 𝐶)
6525, 5, 3ringridm 20245 . . . . . . . . 9 ((𝑆 ∈ Ring ∧ (𝐹𝑥) ∈ 𝐶) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
6612, 64, 65syl2an2r 683 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
6761, 66eqtrd 2766 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))) = (𝐹𝑥))
6824, 39, 673eqtrd 2770 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴𝑥)) = (𝐹𝑥))
6968ralrimiva 3136 . . . . 5 (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴𝑥)) = (𝐹𝑥))
70 eqid 2726 . . . . . . 7 (1r𝑅) = (1r𝑅)
7118, 70ringidcl 20241 . . . . . 6 (𝑅 ∈ Ring → (1r𝑅) ∈ (Base‘𝑅))
729, 71syl 17 . . . . 5 (𝜑 → (1r𝑅) ∈ (Base‘𝑅))
7315, 69, 72rspcdva 3608 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅)))
746mplassa 22027 . . . . . . . . 9 ((𝐼𝑊𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
757, 8, 74syl2anc 582 . . . . . . . 8 (𝜑𝑃 ∈ AssAlg)
76 eqid 2726 . . . . . . . . 9 (Scalar‘𝑃) = (Scalar‘𝑃)
7719, 76asclrhm 21883 . . . . . . . 8 (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
7875, 77syl 17 . . . . . . 7 (𝜑𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
796, 7, 8mplsca 22018 . . . . . . . 8 (𝜑𝑅 = (Scalar‘𝑃))
8079oveq1d 7431 . . . . . . 7 (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
8178, 80eleqtrrd 2829 . . . . . 6 (𝜑𝐴 ∈ (𝑅 RingHom 𝑃))
8270, 2rhm1 20467 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r𝑅)) = (1r𝑃))
8381, 82syl 17 . . . . 5 (𝜑 → (𝐴‘(1r𝑅)) = (1r𝑃))
8483fveq2d 6897 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐸‘(1r𝑃)))
8570, 3rhm1 20467 . . . . 5 (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r𝑅)) = (1r𝑆))
8632, 85syl 17 . . . 4 (𝜑 → (𝐹‘(1r𝑅)) = (1r𝑆))
8773, 84, 863eqtr3d 2774 . . 3 (𝜑 → (𝐸‘(1r𝑃)) = (1r𝑆))
88 eqid 2726 . . . . 5 (+g𝑃) = (+g𝑃)
89 eqid 2726 . . . . 5 (+g𝑆) = (+g𝑆)
9010ringgrpd 20221 . . . . 5 (𝜑𝑃 ∈ Grp)
9112ringgrpd 20221 . . . . 5 (𝜑𝑆 ∈ Grp)
92 eqid 2726 . . . . . . 7 (0g𝑆) = (0g𝑆)
93 ringcmn 20257 . . . . . . . . 9 (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
9412, 93syl 17 . . . . . . . 8 (𝜑𝑆 ∈ CMnd)
9594adantr 479 . . . . . . 7 ((𝜑𝑝𝐵) → 𝑆 ∈ CMnd)
96 ovex 7449 . . . . . . . . 9 (ℕ0m 𝐼) ∈ V
9716, 96rabex2 5333 . . . . . . . 8 𝐷 ∈ V
9897a1i 11 . . . . . . 7 ((𝜑𝑝𝐵) → 𝐷 ∈ V)
997adantr 479 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐼𝑊)
1008adantr 479 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑅 ∈ CRing)
10111adantr 479 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑆 ∈ CRing)
10232adantr 479 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
10334adantr 479 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐺:𝐼𝐶)
104 simpr 483 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑝𝐵)
1056, 1, 25, 16, 26, 27, 5, 28, 29, 99, 100, 101, 102, 103, 104evlslem6 22092 . . . . . . . 8 ((𝜑𝑝𝐵) → ((𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
106105simpld 493 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
107105simprd 494 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
10825, 92, 95, 98, 106, 107gsumcl 19909 . . . . . 6 ((𝜑𝑝𝐵) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ 𝐶)
109108, 29fmptd 7120 . . . . 5 (𝜑𝐸:𝐵𝐶)
110 eqid 2726 . . . . . . . . . . . . . . . . 17 (+g𝑅) = (+g𝑅)
111 simplrl 775 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥𝐵)
112 simplrr 776 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦𝐵)
1136, 1, 110, 88, 111, 112mpladd 22014 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥(+g𝑃)𝑦) = (𝑥f (+g𝑅)𝑦))
114113fveq1d 6895 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥f (+g𝑅)𝑦)‘𝑏))
115 simprl 769 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
1166, 18, 1, 16, 115mplelf 22003 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥:𝐷⟶(Base‘𝑅))
117116ffnd 6721 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 Fn 𝐷)
118117adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥 Fn 𝐷)
119 simprr 771 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
1206, 18, 1, 16, 119mplelf 22003 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦:𝐷⟶(Base‘𝑅))
121120ffnd 6721 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 Fn 𝐷)
122121adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦 Fn 𝐷)
12397a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐷 ∈ V)
124 simpr 483 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑏𝐷)
125 fnfvof 7699 . . . . . . . . . . . . . . . 16 (((𝑥 Fn 𝐷𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏𝐷)) → ((𝑥f (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
126118, 122, 123, 124, 125syl22anc 837 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥f (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
127114, 126eqtrd 2766 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
128127fveq2d 6897 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))))
129 rhmghm 20462 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
13032, 129syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ (𝑅 GrpHom 𝑆))
131130ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
132116ffvelcdmda 7090 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥𝑏) ∈ (Base‘𝑅))
133120ffvelcdmda 7090 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑦𝑏) ∈ (Base‘𝑅))
13418, 110, 89ghmlin 19211 . . . . . . . . . . . . . 14 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥𝑏) ∈ (Base‘𝑅) ∧ (𝑦𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
135131, 132, 133, 134syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
136128, 135eqtrd 2766 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
137136oveq1d 7431 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))))
13812ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑆 ∈ Ring)
13963ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹:(Base‘𝑅)⟶𝐶)
140139, 132ffvelcdmd 7091 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑥𝑏)) ∈ 𝐶)
141139, 133ffvelcdmd 7091 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑦𝑏)) ∈ 𝐶)
14255ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑇 ∈ CMnd)
14334ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐺:𝐼𝐶)
14416, 47, 27, 142, 124, 143psrbagev2 22088 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑇 Σg (𝑏f 𝐺)) ∈ 𝐶)
14525, 89, 5ringdir 20240 . . . . . . . . . . . 12 ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏f 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
146138, 140, 141, 144, 145syl13anc 1369 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
147137, 146eqtrd 2766 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
148147mpteq2dva 5245 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
14997a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐷 ∈ V)
150 ovexd 7451 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))) ∈ V)
151 ovexd 7451 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))) ∈ V)
152 eqidd 2727 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
153 eqidd 2727 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
154149, 150, 151, 152, 153offval2 7702 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
155148, 154eqtr4d 2769 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
156155oveq2d 7432 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
15794adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CMnd)
1587adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐼𝑊)
1598adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑅 ∈ CRing)
16011adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CRing)
16132adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
16234adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺:𝐼𝐶)
1636, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 115evlslem6 22092 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
164163simpld 493 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
1656, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 119evlslem6 22092 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
166165simpld 493 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
167163simprd 494 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
168165simprd 494 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
16925, 92, 89, 157, 149, 164, 166, 167, 168gsumadd 19917 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
170156, 169eqtrd 2766 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
17190adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑃 ∈ Grp)
1721, 88grpcl 18931 . . . . . . . 8 ((𝑃 ∈ Grp ∧ 𝑥𝐵𝑦𝐵) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
173171, 115, 119, 172syl3anc 1368 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
174 fveq1 6892 . . . . . . . . . . . 12 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑝𝑏) = ((𝑥(+g𝑃)𝑦)‘𝑏))
175174fveq2d 6897 . . . . . . . . . . 11 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝐹‘(𝑝𝑏)) = (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)))
176175oveq1d 7431 . . . . . . . . . 10 (𝑝 = (𝑥(+g𝑃)𝑦) → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
177176mpteq2dv 5247 . . . . . . . . 9 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
178177oveq2d 7432 . . . . . . . 8 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
179 ovex 7449 . . . . . . . 8 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
180178, 29, 179fvmpt 7001 . . . . . . 7 ((𝑥(+g𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
181173, 180syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
182 fveq1 6892 . . . . . . . . . . . . 13 (𝑝 = 𝑥 → (𝑝𝑏) = (𝑥𝑏))
183182fveq2d 6897 . . . . . . . . . . . 12 (𝑝 = 𝑥 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑥𝑏)))
184183oveq1d 7431 . . . . . . . . . . 11 (𝑝 = 𝑥 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
185184mpteq2dv 5247 . . . . . . . . . 10 (𝑝 = 𝑥 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
186185oveq2d 7432 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
187 ovex 7449 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
188186, 29, 187fvmpt 7001 . . . . . . . 8 (𝑥𝐵 → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
189115, 188syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
190 fveq1 6892 . . . . . . . . . . . . 13 (𝑝 = 𝑦 → (𝑝𝑏) = (𝑦𝑏))
191190fveq2d 6897 . . . . . . . . . . . 12 (𝑝 = 𝑦 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑦𝑏)))
192191oveq1d 7431 . . . . . . . . . . 11 (𝑝 = 𝑦 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
193192mpteq2dv 5247 . . . . . . . . . 10 (𝑝 = 𝑦 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
194193oveq2d 7432 . . . . . . . . 9 (𝑝 = 𝑦 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
195 ovex 7449 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
196194, 29, 195fvmpt 7001 . . . . . . . 8 (𝑦𝐵 → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
197196ad2antll 727 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
198189, 197oveq12d 7434 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐸𝑥)(+g𝑆)(𝐸𝑦)) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
199170, 181, 1983eqtr4d 2776 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = ((𝐸𝑥)(+g𝑆)(𝐸𝑦)))
2001, 25, 88, 89, 90, 91, 109, 199isghmd 19215 . . . 4 (𝜑𝐸 ∈ (𝑃 GrpHom 𝑆))
201 eqid 2726 . . . . . . . . . . 11 (mulGrp‘𝑅) = (mulGrp‘𝑅)
202201, 26rhmmhm 20457 . . . . . . . . . 10 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
20332, 202syl 17 . . . . . . . . 9 (𝜑𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
204203adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
205 simprll 777 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥𝐵)
2066, 18, 1, 16, 205mplelf 22003 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥:𝐷⟶(Base‘𝑅))
207 simprrl 779 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑧𝐷)
208206, 207ffvelcdmd 7091 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑥𝑧) ∈ (Base‘𝑅))
209 simprlr 778 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦𝐵)
2106, 18, 1, 16, 209mplelf 22003 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦:𝐷⟶(Base‘𝑅))
211 simprrr 780 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑤𝐷)
212210, 211ffvelcdmd 7091 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑦𝑤) ∈ (Base‘𝑅))
213201, 18mgpbas 20119 . . . . . . . . 9 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
214 eqid 2726 . . . . . . . . . 10 (.r𝑅) = (.r𝑅)
215201, 214mgpplusg 20117 . . . . . . . . 9 (.r𝑅) = (+g‘(mulGrp‘𝑅))
21626, 5mgpplusg 20117 . . . . . . . . 9 · = (+g𝑇)
217213, 215, 216mhmlin 18778 . . . . . . . 8 ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥𝑧) ∈ (Base‘𝑅) ∧ (𝑦𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
218204, 208, 212, 217syl3anc 1368 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
21956ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → 𝑇 ∈ Mnd)
220 simprl 769 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧𝐷)
22116psrbagf 21911 . . . . . . . . . . . . . . 15 (𝑧𝐷𝑧:𝐼⟶ℕ0)
222220, 221syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧:𝐼⟶ℕ0)
223222ffvelcdmda 7090 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) ∈ ℕ0)
22416psrbagf 21911 . . . . . . . . . . . . . . 15 (𝑤𝐷𝑤:𝐼⟶ℕ0)
225224ad2antll 727 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤:𝐼⟶ℕ0)
226225ffvelcdmda 7090 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) ∈ ℕ0)
22734adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺:𝐼𝐶)
228227ffvelcdmda 7090 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ 𝐶)
22947, 27, 216mulgnn0dir 19094 . . . . . . . . . . . . 13 ((𝑇 ∈ Mnd ∧ ((𝑧𝑣) ∈ ℕ0 ∧ (𝑤𝑣) ∈ ℕ0 ∧ (𝐺𝑣) ∈ 𝐶)) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
230219, 223, 226, 228, 229syl13anc 1369 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
231230mpteq2dva 5245 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
2327adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐼𝑊)
233 ovexd 7451 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) + (𝑤𝑣)) ∈ V)
234 fvexd 6908 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ V)
235222ffnd 6721 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧 Fn 𝐼)
236225ffnd 6721 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤 Fn 𝐼)
237 inidm 4217 . . . . . . . . . . . . 13 (𝐼𝐼) = 𝐼
238 eqidd 2727 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) = (𝑧𝑣))
239 eqidd 2727 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) = (𝑤𝑣))
240235, 236, 232, 232, 237, 238, 239offval 7691 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f + 𝑤) = (𝑣𝐼 ↦ ((𝑧𝑣) + (𝑤𝑣))))
24134feqmptd 6963 . . . . . . . . . . . . 13 (𝜑𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
242241adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
243232, 233, 234, 240, 242offval2 7702 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f + 𝑤) ∘f 𝐺) = (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))))
244 ovexd 7451 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) (𝐺𝑣)) ∈ V)
245 ovexd 7451 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑤𝑣) (𝐺𝑣)) ∈ V)
24634ffnd 6721 . . . . . . . . . . . . . 14 (𝜑𝐺 Fn 𝐼)
247246adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 Fn 𝐼)
248 eqidd 2727 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) = (𝐺𝑣))
249235, 247, 232, 232, 237, 238, 248offval 7691 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺) = (𝑣𝐼 ↦ ((𝑧𝑣) (𝐺𝑣))))
250236, 247, 232, 232, 237, 239, 248offval 7691 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺) = (𝑣𝐼 ↦ ((𝑤𝑣) (𝐺𝑣))))
251232, 244, 245, 249, 250offval2 7702 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f 𝐺) ∘f · (𝑤f 𝐺)) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
252231, 243, 2513eqtr4d 2776 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f + 𝑤) ∘f 𝐺) = ((𝑧f 𝐺) ∘f · (𝑤f 𝐺)))
253252oveq2d 7432 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = (𝑇 Σg ((𝑧f 𝐺) ∘f · (𝑤f 𝐺))))
25455adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑇 ∈ CMnd)
25516, 47, 27, 48, 254, 220, 227psrbagev1 22086 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f 𝐺):𝐼𝐶 ∧ (𝑧f 𝐺) finSupp (1r𝑆)))
256255simpld 493 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺):𝐼𝐶)
257 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤𝐷)
25816, 47, 27, 48, 254, 257, 227psrbagev1 22086 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑤f 𝐺):𝐼𝐶 ∧ (𝑤f 𝐺) finSupp (1r𝑆)))
259258simpld 493 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺):𝐼𝐶)
260255simprd 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺) finSupp (1r𝑆))
261258simprd 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺) finSupp (1r𝑆))
26247, 48, 216, 254, 232, 256, 259, 260, 261gsumadd 19917 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f 𝐺) ∘f · (𝑤f 𝐺))) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
263253, 262eqtrd 2766 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
264263adantrl 714 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
265218, 264oveq12d 7434 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))))
26655adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑇 ∈ CMnd)
26763adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶)
268267, 208ffvelcdmd 7091 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑥𝑧)) ∈ 𝐶)
269267, 212ffvelcdmd 7091 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑦𝑤)) ∈ 𝐶)
27016, 47, 27, 254, 220, 227psrbagev2 22088 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶)
271270adantrl 714 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶)
27216, 47, 27, 254, 257, 227psrbagev2 22088 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)
273272adantrl 714 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)
27447, 216cmn4 19795 . . . . . . 7 ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
275266, 268, 269, 271, 273, 274syl122anc 1376 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
276265, 275eqtrd 2766 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
2777adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐼𝑊)
2788adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ CRing)
27911adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑆 ∈ CRing)
28032adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆))
28134adantr 479 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐺:𝐼𝐶)
28216psrbagaddcl 21921 . . . . . . 7 ((𝑧𝐷𝑤𝐷) → (𝑧f + 𝑤) ∈ 𝐷)
283282ad2antll 727 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑧f + 𝑤) ∈ 𝐷)
2849adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ Ring)
28518, 214ringcl 20229 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝑥𝑧) ∈ (Base‘𝑅) ∧ (𝑦𝑤) ∈ (Base‘𝑅)) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ (Base‘𝑅))
286284, 208, 212, 285syl3anc 1368 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ (Base‘𝑅))
2876, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 283, 286evlslem3 22091 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧f + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺))))
2886, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 207, 208evlslem3 22091 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) = ((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))))
2896, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 211, 212evlslem3 22091 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅)))) = ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺))))
290288, 289oveq12d 7434 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
291276, 287, 2903eqtr4d 2776 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧f + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))))
2926, 1, 5, 17, 16, 7, 8, 11, 200, 291evlslem2 22090 . . 3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(.r𝑃)𝑦)) = ((𝐸𝑥) · (𝐸𝑦)))
2931, 2, 3, 4, 5, 10, 12, 87, 292, 25, 88, 89, 109, 199isrhmd 20466 . 2 (𝜑𝐸 ∈ (𝑃 RingHom 𝑆))
294 ovex 7449 . . . . . 6 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
295294, 29fnmpti 6696 . . . . 5 𝐸 Fn 𝐵
296295a1i 11 . . . 4 (𝜑𝐸 Fn 𝐵)
29718, 1rhmf 20463 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵)
29881, 297syl 17 . . . . 5 (𝜑𝐴:(Base‘𝑅)⟶𝐵)
299298ffnd 6721 . . . 4 (𝜑𝐴 Fn (Base‘𝑅))
300298frnd 6728 . . . 4 (𝜑 → ran 𝐴𝐵)
301 fnco 6670 . . . 4 ((𝐸 Fn 𝐵𝐴 Fn (Base‘𝑅) ∧ ran 𝐴𝐵) → (𝐸𝐴) Fn (Base‘𝑅))
302296, 299, 300, 301syl3anc 1368 . . 3 (𝜑 → (𝐸𝐴) Fn (Base‘𝑅))
30363ffnd 6721 . . 3 (𝜑𝐹 Fn (Base‘𝑅))
304 fvco2 6991 . . . . 5 ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
305299, 304sylan 578 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
306305, 68eqtrd 2766 . . 3 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐹𝑥))
307302, 303, 306eqfnfvd 7039 . 2 (𝜑 → (𝐸𝐴) = 𝐹)
3086, 28, 1, 7, 9mvrf2 21998 . . . . 5 (𝜑𝑉:𝐼𝐵)
309308ffnd 6721 . . . 4 (𝜑𝑉 Fn 𝐼)
310308frnd 6728 . . . 4 (𝜑 → ran 𝑉𝐵)
311 fnco 6670 . . . 4 ((𝐸 Fn 𝐵𝑉 Fn 𝐼 ∧ ran 𝑉𝐵) → (𝐸𝑉) Fn 𝐼)
312296, 309, 310, 311syl3anc 1368 . . 3 (𝜑 → (𝐸𝑉) Fn 𝐼)
313 fvco2 6991 . . . . 5 ((𝑉 Fn 𝐼𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
314309, 313sylan 578 . . . 4 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
3157adantr 479 . . . . . . 7 ((𝜑𝑥𝐼) → 𝐼𝑊)
3168adantr 479 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑅 ∈ CRing)
317 simpr 483 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑥𝐼)
31828, 16, 17, 70, 315, 316, 317mvrval 21987 . . . . . 6 ((𝜑𝑥𝐼) → (𝑉𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅))))
319318fveq2d 6897 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))))
32011adantr 479 . . . . . 6 ((𝜑𝑥𝐼) → 𝑆 ∈ CRing)
32132adantr 479 . . . . . 6 ((𝜑𝑥𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆))
32234adantr 479 . . . . . 6 ((𝜑𝑥𝐼) → 𝐺:𝐼𝐶)
32316psrbagsn 22072 . . . . . . . 8 (𝐼𝑊 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
3247, 323syl 17 . . . . . . 7 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
325324adantr 479 . . . . . 6 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
32672adantr 479 . . . . . 6 ((𝜑𝑥𝐼) → (1r𝑅) ∈ (Base‘𝑅))
3276, 1, 25, 18, 16, 26, 27, 5, 28, 29, 315, 316, 320, 321, 322, 17, 325, 326evlslem3 22091 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))) = ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))))
32886adantr 479 . . . . . . 7 ((𝜑𝑥𝐼) → (𝐹‘(1r𝑅)) = (1r𝑆))
329 1nn0 12534 . . . . . . . . . . . . . 14 1 ∈ ℕ0
330 0nn0 12533 . . . . . . . . . . . . . 14 0 ∈ ℕ0
331329, 330ifcli 4570 . . . . . . . . . . . . 13 if(𝑧 = 𝑥, 1, 0) ∈ ℕ0
332331a1i 11 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → if(𝑧 = 𝑥, 1, 0) ∈ ℕ0)
33334ffvelcdmda 7090 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
334 eqidd 2727 . . . . . . . . . . . 12 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))
33534feqmptd 6963 . . . . . . . . . . . 12 (𝜑𝐺 = (𝑧𝐼 ↦ (𝐺𝑧)))
3367, 332, 333, 334, 335offval2 7702 . . . . . . . . . . 11 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))))
337 oveq1 7423 . . . . . . . . . . . . . 14 (1 = if(𝑧 = 𝑥, 1, 0) → (1 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
338337eqeq1d 2728 . . . . . . . . . . . . 13 (1 = if(𝑧 = 𝑥, 1, 0) → ((1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
339 oveq1 7423 . . . . . . . . . . . . . 14 (0 = if(𝑧 = 𝑥, 1, 0) → (0 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
340339eqeq1d 2728 . . . . . . . . . . . . 13 (0 = if(𝑧 = 𝑥, 1, 0) → ((0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
341333adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (𝐺𝑧) ∈ 𝐶)
34247, 27mulg1 19071 . . . . . . . . . . . . . . 15 ((𝐺𝑧) ∈ 𝐶 → (1 (𝐺𝑧)) = (𝐺𝑧))
343341, 342syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = (𝐺𝑧))
344 iftrue 4529 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
345344adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
346343, 345eqtr4d 2769 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
34747, 48, 27mulg0 19064 . . . . . . . . . . . . . . . 16 ((𝐺𝑧) ∈ 𝐶 → (0 (𝐺𝑧)) = (1r𝑆))
348333, 347syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐼) → (0 (𝐺𝑧)) = (1r𝑆))
349348adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = (1r𝑆))
350 iffalse 4532 . . . . . . . . . . . . . . 15 𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
351350adantl 480 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
352349, 351eqtr4d 2769 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
353338, 340, 346, 352ifbothda 4561 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
354353mpteq2dva 5245 . . . . . . . . . . 11 (𝜑 → (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
355336, 354eqtrd 2766 . . . . . . . . . 10 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
356355adantr 479 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
357356oveq2d 7432 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺)) = (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))))
35856adantr 479 . . . . . . . . 9 ((𝜑𝑥𝐼) → 𝑇 ∈ Mnd)
359333adantlr 713 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
36025, 3ringidcl 20241 . . . . . . . . . . . . 13 (𝑆 ∈ Ring → (1r𝑆) ∈ 𝐶)
36112, 360syl 17 . . . . . . . . . . . 12 (𝜑 → (1r𝑆) ∈ 𝐶)
362361ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (1r𝑆) ∈ 𝐶)
363359, 362ifcld 4569 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ∈ 𝐶)
364363fmpttd 7121 . . . . . . . . 9 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))):𝐼𝐶)
365 eldifsnneq 4790 . . . . . . . . . . . 12 (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥)
366365, 350syl 17 . . . . . . . . . . 11 (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
367366adantl 480 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
368367, 315suppss2 8207 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) supp (1r𝑆)) ⊆ {𝑥})
36947, 48, 358, 315, 317, 364, 368gsumpt 19956 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))) = ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥))
370 fveq2 6893 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝐺𝑧) = (𝐺𝑥))
371344, 370eqtrd 2766 . . . . . . . . . 10 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑥))
372 eqid 2726 . . . . . . . . . 10 (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
373 fvex 6906 . . . . . . . . . 10 (𝐺𝑥) ∈ V
374371, 372, 373fvmpt 7001 . . . . . . . . 9 (𝑥𝐼 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
375374adantl 480 . . . . . . . 8 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
376357, 369, 3753eqtrd 2770 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺)) = (𝐺𝑥))
377328, 376oveq12d 7434 . . . . . 6 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))) = ((1r𝑆) · (𝐺𝑥)))
37825, 5, 3ringlidm 20244 . . . . . . 7 ((𝑆 ∈ Ring ∧ (𝐺𝑥) ∈ 𝐶) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
37912, 46, 378syl2an2r 683 . . . . . 6 ((𝜑𝑥𝐼) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
380377, 379eqtrd 2766 . . . . 5 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))) = (𝐺𝑥))
381319, 327, 3803eqtrd 2770 . . . 4 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐺𝑥))
382314, 381eqtrd 2766 . . 3 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐺𝑥))
383312, 246, 382eqfnfvd 7039 . 2 (𝜑 → (𝐸𝑉) = 𝐺)
384293, 307, 3833jca 1125 1 (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸𝐴) = 𝐹 ∧ (𝐸𝑉) = 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  w3a 1084   = wceq 1534  wcel 2099  {crab 3419  Vcvv 3462  cdif 3943  wss 3946  ifcif 4523  {csn 4623   class class class wbr 5145  cmpt 5228   × cxp 5672  ccnv 5673  ran crn 5675  cima 5677  ccom 5678   Fn wfn 6541  wf 6542  cfv 6546  (class class class)co 7416  f cof 7680  m cmap 8847  Fincfn 8966   finSupp cfsupp 9398  0cc0 11149  1c1 11150   + caddc 11152  cn 12258  0cn0 12518  cz 12604  Basecbs 17208  +gcplusg 17261  .rcmulr 17262  Scalarcsca 17264  0gc0g 17449   Σg cgsu 17450  Mndcmnd 18722   MndHom cmhm 18766  Grpcgrp 18923  .gcmg 19057   GrpHom cghm 19202  CMndccmn 19774  mulGrpcmgp 20113  1rcur 20160  Ringcrg 20212  CRingccrg 20213   RingHom crh 20447  AssAlgcasa 21844  algSccascl 21846   mVar cmvr 21898   mPoly cmpl 21899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-ofr 7683  df-om 7869  df-1st 7995  df-2nd 7996  df-supp 8167  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-er 8726  df-map 8849  df-pm 8850  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9399  df-sup 9478  df-oi 9546  df-card 9975  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12519  df-z 12605  df-dec 12724  df-uz 12869  df-fz 13533  df-fzo 13676  df-seq 14016  df-hash 14343  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-hom 17285  df-cco 17286  df-0g 17451  df-gsum 17452  df-prds 17457  df-pws 17459  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-mhm 18768  df-submnd 18769  df-grp 18926  df-minusg 18927  df-sbg 18928  df-mulg 19058  df-subg 19113  df-ghm 19203  df-cntz 19307  df-cmn 19776  df-abl 19777  df-mgp 20114  df-rng 20132  df-ur 20161  df-ring 20214  df-cring 20215  df-rhm 20450  df-subrng 20524  df-subrg 20549  df-lmod 20834  df-lss 20905  df-assa 21847  df-ascl 21849  df-psr 21902  df-mvr 21903  df-mpl 21904
This theorem is referenced by:  evlseu  22094  evlsval3  42249
  Copyright terms: Public domain W3C validator