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

Theorem evlslem1 22107
Description: Lemma for evlseu 22108, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.)
Hypotheses
Ref Expression
evlslem1.p 𝑃 = (𝐼 mPoly 𝑅)
evlslem1.b 𝐵 = (Base‘𝑃)
evlslem1.c 𝐶 = (Base‘𝑆)
evlslem1.d 𝐷 = { ∈ (ℕ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 2736 . . 3 (1r𝑃) = (1r𝑃)
3 eqid 2736 . . 3 (1r𝑆) = (1r𝑆)
4 eqid 2736 . . 3 (.r𝑃) = (.r𝑃)
5 evlslem1.m . . 3 · = (.r𝑆)
6 evlslem1.p . . . 4 𝑃 = (𝐼 mPoly 𝑅)
7 evlslem1.i . . . 4 (𝜑𝐼𝑊)
8 evlslem1.r . . . . 5 (𝜑𝑅 ∈ CRing)
98crngringd 20244 . . . 4 (𝜑𝑅 ∈ Ring)
106, 7, 9mplringd 22044 . . 3 (𝜑𝑃 ∈ Ring)
11 evlslem1.s . . . 4 (𝜑𝑆 ∈ CRing)
1211crngringd 20244 . . 3 (𝜑𝑆 ∈ Ring)
13 2fveq3 6910 . . . . . 6 (𝑥 = (1r𝑅) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝐴‘(1r𝑅))))
14 fveq2 6905 . . . . . 6 (𝑥 = (1r𝑅) → (𝐹𝑥) = (𝐹‘(1r𝑅)))
1513, 14eqeq12d 2752 . . . . 5 (𝑥 = (1r𝑅) → ((𝐸‘(𝐴𝑥)) = (𝐹𝑥) ↔ (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅))))
16 evlslem1.d . . . . . . . . 9 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
17 eqid 2736 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
18 eqid 2736 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
19 evlslem1.a . . . . . . . . 9 𝐴 = (algSc‘𝑃)
207adantr 480 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐼𝑊)
219adantr 480 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring)
22 simpr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅))
236, 16, 17, 18, 19, 20, 21, 22mplascl 22089 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐴𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅))))
2423fveq2d 6909 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))))
25 evlslem1.c . . . . . . . 8 𝐶 = (Base‘𝑆)
26 evlslem1.t . . . . . . . 8 𝑇 = (mulGrp‘𝑆)
27 evlslem1.x . . . . . . . 8 = (.g𝑇)
28 evlslem1.v . . . . . . . 8 𝑉 = (𝐼 mVar 𝑅)
29 evlslem1.e . . . . . . . 8 𝐸 = (𝑝𝐵 ↦ (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
308adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ CRing)
3111adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝑆 ∈ CRing)
32 evlslem1.f . . . . . . . . 9 (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
3332adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
34 evlslem1.g . . . . . . . . 9 (𝜑𝐺:𝐼𝐶)
3534adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → 𝐺:𝐼𝐶)
3616psrbag0 22087 . . . . . . . . . 10 (𝐼𝑊 → (𝐼 × {0}) ∈ 𝐷)
377, 36syl 17 . . . . . . . . 9 (𝜑 → (𝐼 × {0}) ∈ 𝐷)
3837adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐼 × {0}) ∈ 𝐷)
396, 1, 25, 18, 16, 26, 27, 5, 28, 29, 20, 30, 31, 33, 35, 17, 38, 22evlslem3 22105 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))) = ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))))
40 0zd 12627 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → 0 ∈ ℤ)
41 fvexd 6920 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ V)
42 fconstmpt 5746 . . . . . . . . . . . . . . 15 (𝐼 × {0}) = (𝑥𝐼 ↦ 0)
4342a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 × {0}) = (𝑥𝐼 ↦ 0))
4434feqmptd 6976 . . . . . . . . . . . . . 14 (𝜑𝐺 = (𝑥𝐼 ↦ (𝐺𝑥)))
457, 40, 41, 43, 44offval2 7718 . . . . . . . . . . . . 13 (𝜑 → ((𝐼 × {0}) ∘f 𝐺) = (𝑥𝐼 ↦ (0 (𝐺𝑥))))
4634ffvelcdmda 7103 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ 𝐶)
4726, 25mgpbas 20143 . . . . . . . . . . . . . . . 16 𝐶 = (Base‘𝑇)
4826, 3ringidval 20181 . . . . . . . . . . . . . . . 16 (1r𝑆) = (0g𝑇)
4947, 48, 27mulg0 19093 . . . . . . . . . . . . . . 15 ((𝐺𝑥) ∈ 𝐶 → (0 (𝐺𝑥)) = (1r𝑆))
5046, 49syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (0 (𝐺𝑥)) = (1r𝑆))
5150mpteq2dva 5241 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝐼 ↦ (0 (𝐺𝑥))) = (𝑥𝐼 ↦ (1r𝑆)))
5245, 51eqtrd 2776 . . . . . . . . . . . 12 (𝜑 → ((𝐼 × {0}) ∘f 𝐺) = (𝑥𝐼 ↦ (1r𝑆)))
5352oveq2d 7448 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))))
5426crngmgp 20239 . . . . . . . . . . . . . 14 (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
5511, 54syl 17 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ CMnd)
5655cmnmndd 19823 . . . . . . . . . . . 12 (𝜑𝑇 ∈ Mnd)
5748gsumz 18850 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝐼𝑊) → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
5856, 7, 57syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
5953, 58eqtrd 2776 . . . . . . . . . 10 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (1r𝑆))
6059adantr 480 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺)) = (1r𝑆))
6160oveq2d 7448 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))) = ((𝐹𝑥) · (1r𝑆)))
6218, 25rhmf 20486 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:(Base‘𝑅)⟶𝐶)
6332, 62syl 17 . . . . . . . . . 10 (𝜑𝐹:(Base‘𝑅)⟶𝐶)
6463ffvelcdmda 7103 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐹𝑥) ∈ 𝐶)
6525, 5, 3ringridm 20268 . . . . . . . . 9 ((𝑆 ∈ Ring ∧ (𝐹𝑥) ∈ 𝐶) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
6612, 64, 65syl2an2r 685 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
6761, 66eqtrd 2776 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘f 𝐺))) = (𝐹𝑥))
6824, 39, 673eqtrd 2780 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑅)) → (𝐸‘(𝐴𝑥)) = (𝐹𝑥))
6968ralrimiva 3145 . . . . 5 (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐸‘(𝐴𝑥)) = (𝐹𝑥))
70 eqid 2736 . . . . . . 7 (1r𝑅) = (1r𝑅)
7118, 70ringidcl 20263 . . . . . 6 (𝑅 ∈ Ring → (1r𝑅) ∈ (Base‘𝑅))
729, 71syl 17 . . . . 5 (𝜑 → (1r𝑅) ∈ (Base‘𝑅))
7315, 69, 72rspcdva 3622 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅)))
746mplassa 22043 . . . . . . . . 9 ((𝐼𝑊𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
757, 8, 74syl2anc 584 . . . . . . . 8 (𝜑𝑃 ∈ AssAlg)
76 eqid 2736 . . . . . . . . 9 (Scalar‘𝑃) = (Scalar‘𝑃)
7719, 76asclrhm 21911 . . . . . . . 8 (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
7875, 77syl 17 . . . . . . 7 (𝜑𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
796, 7, 8mplsca 22034 . . . . . . . 8 (𝜑𝑅 = (Scalar‘𝑃))
8079oveq1d 7447 . . . . . . 7 (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
8178, 80eleqtrrd 2843 . . . . . 6 (𝜑𝐴 ∈ (𝑅 RingHom 𝑃))
8270, 2rhm1 20490 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r𝑅)) = (1r𝑃))
8381, 82syl 17 . . . . 5 (𝜑 → (𝐴‘(1r𝑅)) = (1r𝑃))
8483fveq2d 6909 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐸‘(1r𝑃)))
8570, 3rhm1 20490 . . . . 5 (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r𝑅)) = (1r𝑆))
8632, 85syl 17 . . . 4 (𝜑 → (𝐹‘(1r𝑅)) = (1r𝑆))
8773, 84, 863eqtr3d 2784 . . 3 (𝜑 → (𝐸‘(1r𝑃)) = (1r𝑆))
88 eqid 2736 . . . . 5 (+g𝑃) = (+g𝑃)
89 eqid 2736 . . . . 5 (+g𝑆) = (+g𝑆)
9010ringgrpd 20240 . . . . 5 (𝜑𝑃 ∈ Grp)
9112ringgrpd 20240 . . . . 5 (𝜑𝑆 ∈ Grp)
92 eqid 2736 . . . . . . 7 (0g𝑆) = (0g𝑆)
93 ringcmn 20280 . . . . . . . . 9 (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
9412, 93syl 17 . . . . . . . 8 (𝜑𝑆 ∈ CMnd)
9594adantr 480 . . . . . . 7 ((𝜑𝑝𝐵) → 𝑆 ∈ CMnd)
96 ovex 7465 . . . . . . . . 9 (ℕ0m 𝐼) ∈ V
9716, 96rabex2 5340 . . . . . . . 8 𝐷 ∈ V
9897a1i 11 . . . . . . 7 ((𝜑𝑝𝐵) → 𝐷 ∈ V)
997adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐼𝑊)
1008adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑅 ∈ CRing)
10111adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑆 ∈ CRing)
10232adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
10334adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐺:𝐼𝐶)
104 simpr 484 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑝𝐵)
1056, 1, 25, 16, 26, 27, 5, 28, 29, 99, 100, 101, 102, 103, 104evlslem6 22106 . . . . . . . 8 ((𝜑𝑝𝐵) → ((𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
106105simpld 494 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
107105simprd 495 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
10825, 92, 95, 98, 106, 107gsumcl 19934 . . . . . 6 ((𝜑𝑝𝐵) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ 𝐶)
109108, 29fmptd 7133 . . . . 5 (𝜑𝐸:𝐵𝐶)
110 eqid 2736 . . . . . . . . . . . . . . . . 17 (+g𝑅) = (+g𝑅)
111 simplrl 776 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥𝐵)
112 simplrr 777 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦𝐵)
1136, 1, 110, 88, 111, 112mpladd 22030 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥(+g𝑃)𝑦) = (𝑥f (+g𝑅)𝑦))
114113fveq1d 6907 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥f (+g𝑅)𝑦)‘𝑏))
115 simprl 770 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
1166, 18, 1, 16, 115mplelf 22019 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥:𝐷⟶(Base‘𝑅))
117116ffnd 6736 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 Fn 𝐷)
118117adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥 Fn 𝐷)
119 simprr 772 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
1206, 18, 1, 16, 119mplelf 22019 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦:𝐷⟶(Base‘𝑅))
121120ffnd 6736 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 Fn 𝐷)
122121adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦 Fn 𝐷)
12397a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐷 ∈ V)
124 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑏𝐷)
125 fnfvof 7715 . . . . . . . . . . . . . . . 16 (((𝑥 Fn 𝐷𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏𝐷)) → ((𝑥f (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
126118, 122, 123, 124, 125syl22anc 838 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥f (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
127114, 126eqtrd 2776 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
128127fveq2d 6909 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))))
129 rhmghm 20485 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
13032, 129syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ (𝑅 GrpHom 𝑆))
131130ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
132116ffvelcdmda 7103 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥𝑏) ∈ (Base‘𝑅))
133120ffvelcdmda 7103 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑦𝑏) ∈ (Base‘𝑅))
13418, 110, 89ghmlin 19240 . . . . . . . . . . . . . 14 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥𝑏) ∈ (Base‘𝑅) ∧ (𝑦𝑏) ∈ (Base‘𝑅)) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
135131, 132, 133, 134syl3anc 1372 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
136128, 135eqtrd 2776 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
137136oveq1d 7447 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))))
13812ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑆 ∈ Ring)
13963ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹:(Base‘𝑅)⟶𝐶)
140139, 132ffvelcdmd 7104 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑥𝑏)) ∈ 𝐶)
141139, 133ffvelcdmd 7104 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑦𝑏)) ∈ 𝐶)
14255ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑇 ∈ CMnd)
14334ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐺:𝐼𝐶)
14416, 47, 27, 142, 124, 143psrbagev2 22103 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑇 Σg (𝑏f 𝐺)) ∈ 𝐶)
14525, 89, 5ringdir 20260 . . . . . . . . . . . 12 ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏f 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
146138, 140, 141, 144, 145syl13anc 1373 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
147137, 146eqtrd 2776 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
148147mpteq2dva 5241 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
14997a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐷 ∈ V)
150 ovexd 7467 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))) ∈ V)
151 ovexd 7467 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))) ∈ V)
152 eqidd 2737 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
153 eqidd 2737 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
154149, 150, 151, 152, 153offval2 7718 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
155148, 154eqtr4d 2779 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
156155oveq2d 7448 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
15794adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CMnd)
1587adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐼𝑊)
1598adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑅 ∈ CRing)
16011adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CRing)
16132adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
16234adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺:𝐼𝐶)
1636, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 115evlslem6 22106 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
164163simpld 494 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
1656, 1, 25, 16, 26, 27, 5, 28, 29, 158, 159, 160, 161, 162, 119evlslem6 22106 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆)))
166165simpld 494 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))):𝐷𝐶)
167163simprd 495 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
168165simprd 495 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) finSupp (0g𝑆))
16925, 92, 89, 157, 149, 164, 166, 167, 168gsumadd 19942 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) ∘f (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
170156, 169eqtrd 2776 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
17190adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑃 ∈ Grp)
1721, 88grpcl 18960 . . . . . . . 8 ((𝑃 ∈ Grp ∧ 𝑥𝐵𝑦𝐵) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
173171, 115, 119, 172syl3anc 1372 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
174 fveq1 6904 . . . . . . . . . . . 12 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑝𝑏) = ((𝑥(+g𝑃)𝑦)‘𝑏))
175174fveq2d 6909 . . . . . . . . . . 11 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝐹‘(𝑝𝑏)) = (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)))
176175oveq1d 7447 . . . . . . . . . 10 (𝑝 = (𝑥(+g𝑃)𝑦) → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
177176mpteq2dv 5243 . . . . . . . . 9 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
178177oveq2d 7448 . . . . . . . 8 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
179 ovex 7465 . . . . . . . 8 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
180178, 29, 179fvmpt 7015 . . . . . . 7 ((𝑥(+g𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
181173, 180syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
182 fveq1 6904 . . . . . . . . . . . . 13 (𝑝 = 𝑥 → (𝑝𝑏) = (𝑥𝑏))
183182fveq2d 6909 . . . . . . . . . . . 12 (𝑝 = 𝑥 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑥𝑏)))
184183oveq1d 7447 . . . . . . . . . . 11 (𝑝 = 𝑥 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
185184mpteq2dv 5243 . . . . . . . . . 10 (𝑝 = 𝑥 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
186185oveq2d 7448 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
187 ovex 7465 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
188186, 29, 187fvmpt 7015 . . . . . . . 8 (𝑥𝐵 → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
189115, 188syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
190 fveq1 6904 . . . . . . . . . . . . 13 (𝑝 = 𝑦 → (𝑝𝑏) = (𝑦𝑏))
191190fveq2d 6909 . . . . . . . . . . . 12 (𝑝 = 𝑦 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑦𝑏)))
192191oveq1d 7447 . . . . . . . . . . 11 (𝑝 = 𝑦 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))) = ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))
193192mpteq2dv 5243 . . . . . . . . . 10 (𝑝 = 𝑦 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))
194193oveq2d 7448 . . . . . . . . 9 (𝑝 = 𝑦 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
195 ovex 7465 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
196194, 29, 195fvmpt 7015 . . . . . . . 8 (𝑦𝐵 → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
197196ad2antll 729 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺))))))
198189, 197oveq12d 7450 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐸𝑥)(+g𝑆)(𝐸𝑦)) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏f 𝐺)))))))
199170, 181, 1983eqtr4d 2786 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = ((𝐸𝑥)(+g𝑆)(𝐸𝑦)))
2001, 25, 88, 89, 90, 91, 109, 199isghmd 19244 . . . 4 (𝜑𝐸 ∈ (𝑃 GrpHom 𝑆))
201 eqid 2736 . . . . . . . . . . 11 (mulGrp‘𝑅) = (mulGrp‘𝑅)
202201, 26rhmmhm 20480 . . . . . . . . . 10 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
20332, 202syl 17 . . . . . . . . 9 (𝜑𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
204203adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
205 simprll 778 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥𝐵)
2066, 18, 1, 16, 205mplelf 22019 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥:𝐷⟶(Base‘𝑅))
207 simprrl 780 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑧𝐷)
208206, 207ffvelcdmd 7104 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑥𝑧) ∈ (Base‘𝑅))
209 simprlr 779 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦𝐵)
2106, 18, 1, 16, 209mplelf 22019 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦:𝐷⟶(Base‘𝑅))
211 simprrr 781 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑤𝐷)
212210, 211ffvelcdmd 7104 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑦𝑤) ∈ (Base‘𝑅))
213201, 18mgpbas 20143 . . . . . . . . 9 (Base‘𝑅) = (Base‘(mulGrp‘𝑅))
214 eqid 2736 . . . . . . . . . 10 (.r𝑅) = (.r𝑅)
215201, 214mgpplusg 20142 . . . . . . . . 9 (.r𝑅) = (+g‘(mulGrp‘𝑅))
21626, 5mgpplusg 20142 . . . . . . . . 9 · = (+g𝑇)
217213, 215, 216mhmlin 18807 . . . . . . . 8 ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥𝑧) ∈ (Base‘𝑅) ∧ (𝑦𝑤) ∈ (Base‘𝑅)) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
218204, 208, 212, 217syl3anc 1372 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
21956ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → 𝑇 ∈ Mnd)
220 simprl 770 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧𝐷)
22116psrbagf 21939 . . . . . . . . . . . . . . 15 (𝑧𝐷𝑧:𝐼⟶ℕ0)
222220, 221syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧:𝐼⟶ℕ0)
223222ffvelcdmda 7103 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) ∈ ℕ0)
22416psrbagf 21939 . . . . . . . . . . . . . . 15 (𝑤𝐷𝑤:𝐼⟶ℕ0)
225224ad2antll 729 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤:𝐼⟶ℕ0)
226225ffvelcdmda 7103 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) ∈ ℕ0)
22734adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺:𝐼𝐶)
228227ffvelcdmda 7103 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ 𝐶)
22947, 27, 216mulgnn0dir 19123 . . . . . . . . . . . . 13 ((𝑇 ∈ Mnd ∧ ((𝑧𝑣) ∈ ℕ0 ∧ (𝑤𝑣) ∈ ℕ0 ∧ (𝐺𝑣) ∈ 𝐶)) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
230219, 223, 226, 228, 229syl13anc 1373 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
231230mpteq2dva 5241 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
2327adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐼𝑊)
233 ovexd 7467 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) + (𝑤𝑣)) ∈ V)
234 fvexd 6920 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ V)
235222ffnd 6736 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧 Fn 𝐼)
236225ffnd 6736 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤 Fn 𝐼)
237 inidm 4226 . . . . . . . . . . . . 13 (𝐼𝐼) = 𝐼
238 eqidd 2737 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) = (𝑧𝑣))
239 eqidd 2737 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) = (𝑤𝑣))
240235, 236, 232, 232, 237, 238, 239offval 7707 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f + 𝑤) = (𝑣𝐼 ↦ ((𝑧𝑣) + (𝑤𝑣))))
24134feqmptd 6976 . . . . . . . . . . . . 13 (𝜑𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
242241adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
243232, 233, 234, 240, 242offval2 7718 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f + 𝑤) ∘f 𝐺) = (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))))
244 ovexd 7467 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) (𝐺𝑣)) ∈ V)
245 ovexd 7467 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑤𝑣) (𝐺𝑣)) ∈ V)
24634ffnd 6736 . . . . . . . . . . . . . 14 (𝜑𝐺 Fn 𝐼)
247246adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 Fn 𝐼)
248 eqidd 2737 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) = (𝐺𝑣))
249235, 247, 232, 232, 237, 238, 248offval 7707 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺) = (𝑣𝐼 ↦ ((𝑧𝑣) (𝐺𝑣))))
250236, 247, 232, 232, 237, 239, 248offval 7707 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺) = (𝑣𝐼 ↦ ((𝑤𝑣) (𝐺𝑣))))
251232, 244, 245, 249, 250offval2 7718 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f 𝐺) ∘f · (𝑤f 𝐺)) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
252231, 243, 2513eqtr4d 2786 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f + 𝑤) ∘f 𝐺) = ((𝑧f 𝐺) ∘f · (𝑤f 𝐺)))
253252oveq2d 7448 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = (𝑇 Σg ((𝑧f 𝐺) ∘f · (𝑤f 𝐺))))
25455adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑇 ∈ CMnd)
25516, 47, 27, 48, 254, 220, 227psrbagev1 22102 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧f 𝐺):𝐼𝐶 ∧ (𝑧f 𝐺) finSupp (1r𝑆)))
256255simpld 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺):𝐼𝐶)
257 simprr 772 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤𝐷)
25816, 47, 27, 48, 254, 257, 227psrbagev1 22102 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑤f 𝐺):𝐼𝐶 ∧ (𝑤f 𝐺) finSupp (1r𝑆)))
259258simpld 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺):𝐼𝐶)
260255simprd 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧f 𝐺) finSupp (1r𝑆))
261258simprd 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤f 𝐺) finSupp (1r𝑆))
26247, 48, 216, 254, 232, 256, 259, 260, 261gsumadd 19942 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f 𝐺) ∘f · (𝑤f 𝐺))) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
263253, 262eqtrd 2776 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
264263adantrl 716 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺)) = ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺))))
265218, 264oveq12d 7450 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))))
26655adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑇 ∈ CMnd)
26763adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹:(Base‘𝑅)⟶𝐶)
268267, 208ffvelcdmd 7104 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑥𝑧)) ∈ 𝐶)
269267, 212ffvelcdmd 7104 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑦𝑤)) ∈ 𝐶)
27016, 47, 27, 254, 220, 227psrbagev2 22103 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶)
271270adantrl 716 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶)
27216, 47, 27, 254, 257, 227psrbagev2 22103 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)
273272adantrl 716 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)
27447, 216cmn4 19820 . . . . . . 7 ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧f 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤f 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
275266, 268, 269, 271, 273, 274syl122anc 1380 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧f 𝐺)) · (𝑇 Σg (𝑤f 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
276265, 275eqtrd 2776 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧f + 𝑤) ∘f 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
2777adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐼𝑊)
2788adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ CRing)
27911adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑆 ∈ CRing)
28032adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆))
28134adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐺:𝐼𝐶)
28216psrbagaddcl 21945 . . . . . . 7 ((𝑧𝐷𝑤𝐷) → (𝑧f + 𝑤) ∈ 𝐷)
283282ad2antll 729 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑧f + 𝑤) ∈ 𝐷)
2849adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ Ring)
28518, 214ringcl 20248 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝑥𝑧) ∈ (Base‘𝑅) ∧ (𝑦𝑤) ∈ (Base‘𝑅)) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ (Base‘𝑅))
286284, 208, 212, 285syl3anc 1372 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ (Base‘𝑅))
2876, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 283, 286evlslem3 22105 . . . . 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 22105 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) = ((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))))
2896, 1, 25, 18, 16, 26, 27, 5, 28, 29, 277, 278, 279, 280, 281, 17, 211, 212evlslem3 22105 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅)))) = ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺))))
290288, 289oveq12d 7450 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧f 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤f 𝐺)))))
291276, 287, 2903eqtr4d 2786 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧f + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))))
2926, 1, 5, 17, 16, 7, 8, 11, 200, 291evlslem2 22104 . . 3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(.r𝑃)𝑦)) = ((𝐸𝑥) · (𝐸𝑦)))
2931, 2, 3, 4, 5, 10, 12, 87, 292, 25, 88, 89, 109, 199isrhmd 20489 . 2 (𝜑𝐸 ∈ (𝑃 RingHom 𝑆))
294 ovex 7465 . . . . . 6 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏f 𝐺))))) ∈ V
295294, 29fnmpti 6710 . . . . 5 𝐸 Fn 𝐵
296295a1i 11 . . . 4 (𝜑𝐸 Fn 𝐵)
29718, 1rhmf 20486 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:(Base‘𝑅)⟶𝐵)
29881, 297syl 17 . . . . 5 (𝜑𝐴:(Base‘𝑅)⟶𝐵)
299298ffnd 6736 . . . 4 (𝜑𝐴 Fn (Base‘𝑅))
300298frnd 6743 . . . 4 (𝜑 → ran 𝐴𝐵)
301 fnco 6685 . . . 4 ((𝐸 Fn 𝐵𝐴 Fn (Base‘𝑅) ∧ ran 𝐴𝐵) → (𝐸𝐴) Fn (Base‘𝑅))
302296, 299, 300, 301syl3anc 1372 . . 3 (𝜑 → (𝐸𝐴) Fn (Base‘𝑅))
30363ffnd 6736 . . 3 (𝜑𝐹 Fn (Base‘𝑅))
304 fvco2 7005 . . . . 5 ((𝐴 Fn (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
305299, 304sylan 580 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
306305, 68eqtrd 2776 . . 3 ((𝜑𝑥 ∈ (Base‘𝑅)) → ((𝐸𝐴)‘𝑥) = (𝐹𝑥))
307302, 303, 306eqfnfvd 7053 . 2 (𝜑 → (𝐸𝐴) = 𝐹)
3086, 28, 1, 7, 9mvrf2 22014 . . . . 5 (𝜑𝑉:𝐼𝐵)
309308ffnd 6736 . . . 4 (𝜑𝑉 Fn 𝐼)
310308frnd 6743 . . . 4 (𝜑 → ran 𝑉𝐵)
311 fnco 6685 . . . 4 ((𝐸 Fn 𝐵𝑉 Fn 𝐼 ∧ ran 𝑉𝐵) → (𝐸𝑉) Fn 𝐼)
312296, 309, 310, 311syl3anc 1372 . . 3 (𝜑 → (𝐸𝑉) Fn 𝐼)
313 fvco2 7005 . . . . 5 ((𝑉 Fn 𝐼𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
314309, 313sylan 580 . . . 4 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
3157adantr 480 . . . . . . 7 ((𝜑𝑥𝐼) → 𝐼𝑊)
3168adantr 480 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑅 ∈ CRing)
317 simpr 484 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑥𝐼)
31828, 16, 17, 70, 315, 316, 317mvrval 22003 . . . . . 6 ((𝜑𝑥𝐼) → (𝑉𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅))))
319318fveq2d 6909 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))))
32011adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → 𝑆 ∈ CRing)
32132adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆))
32234adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → 𝐺:𝐼𝐶)
32316psrbagsn 22088 . . . . . . . 8 (𝐼𝑊 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
3247, 323syl 17 . . . . . . 7 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
325324adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
32672adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → (1r𝑅) ∈ (Base‘𝑅))
3276, 1, 25, 18, 16, 26, 27, 5, 28, 29, 315, 316, 320, 321, 322, 17, 325, 326evlslem3 22105 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))) = ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))))
32886adantr 480 . . . . . . 7 ((𝜑𝑥𝐼) → (𝐹‘(1r𝑅)) = (1r𝑆))
329 1nn0 12544 . . . . . . . . . . . . . 14 1 ∈ ℕ0
330 0nn0 12543 . . . . . . . . . . . . . 14 0 ∈ ℕ0
331329, 330ifcli 4572 . . . . . . . . . . . . 13 if(𝑧 = 𝑥, 1, 0) ∈ ℕ0
332331a1i 11 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → if(𝑧 = 𝑥, 1, 0) ∈ ℕ0)
33334ffvelcdmda 7103 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
334 eqidd 2737 . . . . . . . . . . . 12 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))
33534feqmptd 6976 . . . . . . . . . . . 12 (𝜑𝐺 = (𝑧𝐼 ↦ (𝐺𝑧)))
3367, 332, 333, 334, 335offval2 7718 . . . . . . . . . . 11 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))))
337 oveq1 7439 . . . . . . . . . . . . . 14 (1 = if(𝑧 = 𝑥, 1, 0) → (1 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
338337eqeq1d 2738 . . . . . . . . . . . . 13 (1 = if(𝑧 = 𝑥, 1, 0) → ((1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
339 oveq1 7439 . . . . . . . . . . . . . 14 (0 = if(𝑧 = 𝑥, 1, 0) → (0 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
340339eqeq1d 2738 . . . . . . . . . . . . 13 (0 = if(𝑧 = 𝑥, 1, 0) → ((0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
341333adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (𝐺𝑧) ∈ 𝐶)
34247, 27mulg1 19100 . . . . . . . . . . . . . . 15 ((𝐺𝑧) ∈ 𝐶 → (1 (𝐺𝑧)) = (𝐺𝑧))
343341, 342syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = (𝐺𝑧))
344 iftrue 4530 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
345344adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
346343, 345eqtr4d 2779 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
34747, 48, 27mulg0 19093 . . . . . . . . . . . . . . . 16 ((𝐺𝑧) ∈ 𝐶 → (0 (𝐺𝑧)) = (1r𝑆))
348333, 347syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐼) → (0 (𝐺𝑧)) = (1r𝑆))
349348adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = (1r𝑆))
350 iffalse 4533 . . . . . . . . . . . . . . 15 𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
351350adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
352349, 351eqtr4d 2779 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
353338, 340, 346, 352ifbothda 4563 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
354353mpteq2dva 5241 . . . . . . . . . . 11 (𝜑 → (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
355336, 354eqtrd 2776 . . . . . . . . . 10 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
356355adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
357356oveq2d 7448 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺)) = (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))))
35856adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐼) → 𝑇 ∈ Mnd)
359333adantlr 715 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
36025, 3ringidcl 20263 . . . . . . . . . . . . 13 (𝑆 ∈ Ring → (1r𝑆) ∈ 𝐶)
36112, 360syl 17 . . . . . . . . . . . 12 (𝜑 → (1r𝑆) ∈ 𝐶)
362361ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (1r𝑆) ∈ 𝐶)
363359, 362ifcld 4571 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ∈ 𝐶)
364363fmpttd 7134 . . . . . . . . 9 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))):𝐼𝐶)
365 eldifsnneq 4790 . . . . . . . . . . . 12 (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥)
366365, 350syl 17 . . . . . . . . . . 11 (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
367366adantl 481 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
368367, 315suppss2 8226 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) supp (1r𝑆)) ⊆ {𝑥})
36947, 48, 358, 315, 317, 364, 368gsumpt 19981 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))) = ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥))
370 fveq2 6905 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝐺𝑧) = (𝐺𝑥))
371344, 370eqtrd 2776 . . . . . . . . . 10 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑥))
372 eqid 2736 . . . . . . . . . 10 (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
373 fvex 6918 . . . . . . . . . 10 (𝐺𝑥) ∈ V
374371, 372, 373fvmpt 7015 . . . . . . . . 9 (𝑥𝐼 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
375374adantl 481 . . . . . . . 8 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
376357, 369, 3753eqtrd 2780 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺)) = (𝐺𝑥))
377328, 376oveq12d 7450 . . . . . 6 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))) = ((1r𝑆) · (𝐺𝑥)))
37825, 5, 3ringlidm 20267 . . . . . . 7 ((𝑆 ∈ Ring ∧ (𝐺𝑥) ∈ 𝐶) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
37912, 46, 378syl2an2r 685 . . . . . 6 ((𝜑𝑥𝐼) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
380377, 379eqtrd 2776 . . . . 5 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘f 𝐺))) = (𝐺𝑥))
381319, 327, 3803eqtrd 2780 . . . 4 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐺𝑥))
382314, 381eqtrd 2776 . . 3 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐺𝑥))
383312, 246, 382eqfnfvd 7053 . 2 (𝜑 → (𝐸𝑉) = 𝐺)
384293, 307, 3833jca 1128 1 (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸𝐴) = 𝐹 ∧ (𝐸𝑉) = 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1086   = wceq 1539  wcel 2107  {crab 3435  Vcvv 3479  cdif 3947  wss 3950  ifcif 4524  {csn 4625   class class class wbr 5142  cmpt 5224   × cxp 5682  ccnv 5683  ran crn 5685  cima 5687  ccom 5688   Fn wfn 6555  wf 6556  cfv 6560  (class class class)co 7432  f cof 7696  m cmap 8867  Fincfn 8986   finSupp cfsupp 9402  0cc0 11156  1c1 11157   + caddc 11159  cn 12267  0cn0 12528  cz 12615  Basecbs 17248  +gcplusg 17298  .rcmulr 17299  Scalarcsca 17301  0gc0g 17485   Σg cgsu 17486  Mndcmnd 18748   MndHom cmhm 18795  Grpcgrp 18952  .gcmg 19086   GrpHom cghm 19231  CMndccmn 19799  mulGrpcmgp 20138  1rcur 20179  Ringcrg 20231  CRingccrg 20232   RingHom crh 20470  AssAlgcasa 21871  algSccascl 21873   mVar cmvr 21926   mPoly cmpl 21927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-of 7698  df-ofr 7699  df-om 7889  df-1st 8015  df-2nd 8016  df-supp 8187  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-er 8746  df-map 8869  df-pm 8870  df-ixp 8939  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fsupp 9403  df-sup 9483  df-oi 9551  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12529  df-z 12616  df-dec 12736  df-uz 12880  df-fz 13549  df-fzo 13696  df-seq 14044  df-hash 14371  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17249  df-ress 17276  df-plusg 17311  df-mulr 17312  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-hom 17322  df-cco 17323  df-0g 17487  df-gsum 17488  df-prds 17493  df-pws 17495  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-mhm 18797  df-submnd 18798  df-grp 18955  df-minusg 18956  df-sbg 18957  df-mulg 19087  df-subg 19142  df-ghm 19232  df-cntz 19336  df-cmn 19801  df-abl 19802  df-mgp 20139  df-rng 20151  df-ur 20180  df-ring 20233  df-cring 20234  df-rhm 20473  df-subrng 20547  df-subrg 20571  df-lmod 20861  df-lss 20931  df-assa 21874  df-ascl 21876  df-psr 21930  df-mvr 21931  df-mpl 21932
This theorem is referenced by:  evlseu  22108  evlsval3  42574
  Copyright terms: Public domain W3C validator