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

Theorem evlslem1 19563
Description: Lemma for evlseu 19564, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.)
Hypotheses
Ref Expression
evlslem1.p 𝑃 = (𝐼 mPoly 𝑅)
evlslem1.b 𝐵 = (Base‘𝑃)
evlslem1.c 𝐶 = (Base‘𝑆)
evlslem1.k 𝐾 = (Base‘𝑅)
evlslem1.d 𝐷 = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
evlslem1.t 𝑇 = (mulGrp‘𝑆)
evlslem1.x = (.g𝑇)
evlslem1.m · = (.r𝑆)
evlslem1.v 𝑉 = (𝐼 mVar 𝑅)
evlslem1.e 𝐸 = (𝑝𝐵 ↦ (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
evlslem1.i (𝜑𝐼 ∈ V)
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 2651 . . 3 (1r𝑃) = (1r𝑃)
3 eqid 2651 . . 3 (1r𝑆) = (1r𝑆)
4 eqid 2651 . . 3 (.r𝑃) = (.r𝑃)
5 evlslem1.m . . 3 · = (.r𝑆)
6 evlslem1.i . . . 4 (𝜑𝐼 ∈ V)
7 evlslem1.r . . . . 5 (𝜑𝑅 ∈ CRing)
8 crngring 18604 . . . . 5 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
97, 8syl 17 . . . 4 (𝜑𝑅 ∈ Ring)
10 evlslem1.p . . . . 5 𝑃 = (𝐼 mPoly 𝑅)
1110mplring 19500 . . . 4 ((𝐼 ∈ V ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring)
126, 9, 11syl2anc 694 . . 3 (𝜑𝑃 ∈ Ring)
13 evlslem1.s . . . 4 (𝜑𝑆 ∈ CRing)
14 crngring 18604 . . . 4 (𝑆 ∈ CRing → 𝑆 ∈ Ring)
1513, 14syl 17 . . 3 (𝜑𝑆 ∈ Ring)
16 fveq2 6229 . . . . . . 7 (𝑥 = (1r𝑅) → (𝐴𝑥) = (𝐴‘(1r𝑅)))
1716fveq2d 6233 . . . . . 6 (𝑥 = (1r𝑅) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝐴‘(1r𝑅))))
18 fveq2 6229 . . . . . 6 (𝑥 = (1r𝑅) → (𝐹𝑥) = (𝐹‘(1r𝑅)))
1917, 18eqeq12d 2666 . . . . 5 (𝑥 = (1r𝑅) → ((𝐸‘(𝐴𝑥)) = (𝐹𝑥) ↔ (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅))))
20 evlslem1.d . . . . . . . . 9 𝐷 = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
21 eqid 2651 . . . . . . . . 9 (0g𝑅) = (0g𝑅)
22 evlslem1.k . . . . . . . . 9 𝐾 = (Base‘𝑅)
23 evlslem1.a . . . . . . . . 9 𝐴 = (algSc‘𝑃)
246adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐾) → 𝐼 ∈ V)
259adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐾) → 𝑅 ∈ Ring)
26 simpr 476 . . . . . . . . 9 ((𝜑𝑥𝐾) → 𝑥𝐾)
2710, 20, 21, 22, 23, 24, 25, 26mplascl 19544 . . . . . . . 8 ((𝜑𝑥𝐾) → (𝐴𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅))))
2827fveq2d 6233 . . . . . . 7 ((𝜑𝑥𝐾) → (𝐸‘(𝐴𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))))
29 evlslem1.c . . . . . . . 8 𝐶 = (Base‘𝑆)
30 evlslem1.t . . . . . . . 8 𝑇 = (mulGrp‘𝑆)
31 evlslem1.x . . . . . . . 8 = (.g𝑇)
32 evlslem1.v . . . . . . . 8 𝑉 = (𝐼 mVar 𝑅)
33 evlslem1.e . . . . . . . 8 𝐸 = (𝑝𝐵 ↦ (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
347adantr 480 . . . . . . . 8 ((𝜑𝑥𝐾) → 𝑅 ∈ CRing)
3513adantr 480 . . . . . . . 8 ((𝜑𝑥𝐾) → 𝑆 ∈ CRing)
36 evlslem1.f . . . . . . . . 9 (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))
3736adantr 480 . . . . . . . 8 ((𝜑𝑥𝐾) → 𝐹 ∈ (𝑅 RingHom 𝑆))
38 evlslem1.g . . . . . . . . 9 (𝜑𝐺:𝐼𝐶)
3938adantr 480 . . . . . . . 8 ((𝜑𝑥𝐾) → 𝐺:𝐼𝐶)
4020psrbag0 19542 . . . . . . . . . 10 (𝐼 ∈ V → (𝐼 × {0}) ∈ 𝐷)
416, 40syl 17 . . . . . . . . 9 (𝜑 → (𝐼 × {0}) ∈ 𝐷)
4241adantr 480 . . . . . . . 8 ((𝜑𝑥𝐾) → (𝐼 × {0}) ∈ 𝐷)
4310, 1, 29, 22, 20, 30, 31, 5, 32, 33, 24, 34, 35, 37, 39, 21, 42, 26evlslem3 19562 . . . . . . 7 ((𝜑𝑥𝐾) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝐼 × {0}), 𝑥, (0g𝑅)))) = ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺))))
44 0zd 11427 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → 0 ∈ ℤ)
45 fvexd 6241 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ V)
46 fconstmpt 5197 . . . . . . . . . . . . . . 15 (𝐼 × {0}) = (𝑥𝐼 ↦ 0)
4746a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 × {0}) = (𝑥𝐼 ↦ 0))
4838feqmptd 6288 . . . . . . . . . . . . . 14 (𝜑𝐺 = (𝑥𝐼 ↦ (𝐺𝑥)))
496, 44, 45, 47, 48offval2 6956 . . . . . . . . . . . . 13 (𝜑 → ((𝐼 × {0}) ∘𝑓 𝐺) = (𝑥𝐼 ↦ (0 (𝐺𝑥))))
5038ffvelrnda 6399 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝐼) → (𝐺𝑥) ∈ 𝐶)
5130, 29mgpbas 18541 . . . . . . . . . . . . . . . 16 𝐶 = (Base‘𝑇)
5230, 3ringidval 18549 . . . . . . . . . . . . . . . 16 (1r𝑆) = (0g𝑇)
5351, 52, 31mulg0 17593 . . . . . . . . . . . . . . 15 ((𝐺𝑥) ∈ 𝐶 → (0 (𝐺𝑥)) = (1r𝑆))
5450, 53syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐼) → (0 (𝐺𝑥)) = (1r𝑆))
5554mpteq2dva 4777 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝐼 ↦ (0 (𝐺𝑥))) = (𝑥𝐼 ↦ (1r𝑆)))
5649, 55eqtrd 2685 . . . . . . . . . . . 12 (𝜑 → ((𝐼 × {0}) ∘𝑓 𝐺) = (𝑥𝐼 ↦ (1r𝑆)))
5756oveq2d 6706 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺)) = (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))))
5830crngmgp 18601 . . . . . . . . . . . . . 14 (𝑆 ∈ CRing → 𝑇 ∈ CMnd)
5913, 58syl 17 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ CMnd)
60 cmnmnd 18254 . . . . . . . . . . . . 13 (𝑇 ∈ CMnd → 𝑇 ∈ Mnd)
6159, 60syl 17 . . . . . . . . . . . 12 (𝜑𝑇 ∈ Mnd)
6252gsumz 17421 . . . . . . . . . . . 12 ((𝑇 ∈ Mnd ∧ 𝐼 ∈ V) → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
6361, 6, 62syl2anc 694 . . . . . . . . . . 11 (𝜑 → (𝑇 Σg (𝑥𝐼 ↦ (1r𝑆))) = (1r𝑆))
6457, 63eqtrd 2685 . . . . . . . . . 10 (𝜑 → (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺)) = (1r𝑆))
6564adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐾) → (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺)) = (1r𝑆))
6665oveq2d 6706 . . . . . . . 8 ((𝜑𝑥𝐾) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺))) = ((𝐹𝑥) · (1r𝑆)))
6722, 29rhmf 18774 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹:𝐾𝐶)
6836, 67syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐾𝐶)
6968ffvelrnda 6399 . . . . . . . . 9 ((𝜑𝑥𝐾) → (𝐹𝑥) ∈ 𝐶)
7029, 5, 3ringridm 18618 . . . . . . . . 9 ((𝑆 ∈ Ring ∧ (𝐹𝑥) ∈ 𝐶) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
7115, 69, 70syl2an2r 893 . . . . . . . 8 ((𝜑𝑥𝐾) → ((𝐹𝑥) · (1r𝑆)) = (𝐹𝑥))
7266, 71eqtrd 2685 . . . . . . 7 ((𝜑𝑥𝐾) → ((𝐹𝑥) · (𝑇 Σg ((𝐼 × {0}) ∘𝑓 𝐺))) = (𝐹𝑥))
7328, 43, 723eqtrd 2689 . . . . . 6 ((𝜑𝑥𝐾) → (𝐸‘(𝐴𝑥)) = (𝐹𝑥))
7473ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑥𝐾 (𝐸‘(𝐴𝑥)) = (𝐹𝑥))
75 eqid 2651 . . . . . . 7 (1r𝑅) = (1r𝑅)
7622, 75ringidcl 18614 . . . . . 6 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐾)
779, 76syl 17 . . . . 5 (𝜑 → (1r𝑅) ∈ 𝐾)
7819, 74, 77rspcdva 3347 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐹‘(1r𝑅)))
7910mplassa 19502 . . . . . . . . 9 ((𝐼 ∈ V ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
806, 7, 79syl2anc 694 . . . . . . . 8 (𝜑𝑃 ∈ AssAlg)
81 eqid 2651 . . . . . . . . 9 (Scalar‘𝑃) = (Scalar‘𝑃)
8223, 81asclrhm 19390 . . . . . . . 8 (𝑃 ∈ AssAlg → 𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
8380, 82syl 17 . . . . . . 7 (𝜑𝐴 ∈ ((Scalar‘𝑃) RingHom 𝑃))
8410, 6, 7mplsca 19493 . . . . . . . 8 (𝜑𝑅 = (Scalar‘𝑃))
8584oveq1d 6705 . . . . . . 7 (𝜑 → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
8683, 85eleqtrrd 2733 . . . . . 6 (𝜑𝐴 ∈ (𝑅 RingHom 𝑃))
8775, 2rhm1 18778 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → (𝐴‘(1r𝑅)) = (1r𝑃))
8886, 87syl 17 . . . . 5 (𝜑 → (𝐴‘(1r𝑅)) = (1r𝑃))
8988fveq2d 6233 . . . 4 (𝜑 → (𝐸‘(𝐴‘(1r𝑅))) = (𝐸‘(1r𝑃)))
9075, 3rhm1 18778 . . . . 5 (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹‘(1r𝑅)) = (1r𝑆))
9136, 90syl 17 . . . 4 (𝜑 → (𝐹‘(1r𝑅)) = (1r𝑆))
9278, 89, 913eqtr3d 2693 . . 3 (𝜑 → (𝐸‘(1r𝑃)) = (1r𝑆))
93 eqid 2651 . . . . 5 (+g𝑃) = (+g𝑃)
94 eqid 2651 . . . . 5 (+g𝑆) = (+g𝑆)
95 ringgrp 18598 . . . . . 6 (𝑃 ∈ Ring → 𝑃 ∈ Grp)
9612, 95syl 17 . . . . 5 (𝜑𝑃 ∈ Grp)
97 ringgrp 18598 . . . . . 6 (𝑆 ∈ Ring → 𝑆 ∈ Grp)
9815, 97syl 17 . . . . 5 (𝜑𝑆 ∈ Grp)
99 eqid 2651 . . . . . . 7 (0g𝑆) = (0g𝑆)
100 ringcmn 18627 . . . . . . . . 9 (𝑆 ∈ Ring → 𝑆 ∈ CMnd)
10115, 100syl 17 . . . . . . . 8 (𝜑𝑆 ∈ CMnd)
102101adantr 480 . . . . . . 7 ((𝜑𝑝𝐵) → 𝑆 ∈ CMnd)
103 ovex 6718 . . . . . . . . 9 (ℕ0𝑚 𝐼) ∈ V
10420, 103rabex2 4847 . . . . . . . 8 𝐷 ∈ V
105104a1i 11 . . . . . . 7 ((𝜑𝑝𝐵) → 𝐷 ∈ V)
1066adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐼 ∈ V)
1077adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑅 ∈ CRing)
10813adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑆 ∈ CRing)
10936adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
11038adantr 480 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝐺:𝐼𝐶)
111 simpr 476 . . . . . . . . 9 ((𝜑𝑝𝐵) → 𝑝𝐵)
11210, 1, 29, 22, 20, 30, 31, 5, 32, 33, 106, 107, 108, 109, 110, 111evlslem6 19561 . . . . . . . 8 ((𝜑𝑝𝐵) → ((𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆)))
113112simpld 474 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶)
114112simprd 478 . . . . . . 7 ((𝜑𝑝𝐵) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆))
11529, 99, 102, 105, 113, 114gsumcl 18362 . . . . . 6 ((𝜑𝑝𝐵) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ 𝐶)
116115, 33fmptd 6425 . . . . 5 (𝜑𝐸:𝐵𝐶)
117 eqid 2651 . . . . . . . . . . . . . . . . 17 (+g𝑅) = (+g𝑅)
118 simplrl 817 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥𝐵)
119 simplrr 818 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦𝐵)
12010, 1, 117, 93, 118, 119mpladd 19490 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥(+g𝑃)𝑦) = (𝑥𝑓 (+g𝑅)𝑦))
121120fveq1d 6231 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥𝑓 (+g𝑅)𝑦)‘𝑏))
122 simprl 809 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
12310, 22, 1, 20, 122mplelf 19481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥:𝐷𝐾)
124123ffnd 6084 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 Fn 𝐷)
125124adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑥 Fn 𝐷)
126 simprr 811 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
12710, 22, 1, 20, 126mplelf 19481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦:𝐷𝐾)
128127ffnd 6084 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 Fn 𝐷)
129128adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑦 Fn 𝐷)
130104a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐷 ∈ V)
131 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑏𝐷)
132 fnfvof 6953 . . . . . . . . . . . . . . . 16 (((𝑥 Fn 𝐷𝑦 Fn 𝐷) ∧ (𝐷 ∈ V ∧ 𝑏𝐷)) → ((𝑥𝑓 (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
133125, 129, 130, 131, 132syl22anc 1367 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥𝑓 (+g𝑅)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
134121, 133eqtrd 2685 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝑥(+g𝑃)𝑦)‘𝑏) = ((𝑥𝑏)(+g𝑅)(𝑦𝑏)))
135134fveq2d 6233 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))))
136 rhmghm 18773 . . . . . . . . . . . . . . . 16 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
13736, 136syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ (𝑅 GrpHom 𝑆))
138137ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
139123ffvelrnda 6399 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑥𝑏) ∈ 𝐾)
140127ffvelrnda 6399 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑦𝑏) ∈ 𝐾)
14122, 117, 94ghmlin 17712 . . . . . . . . . . . . . 14 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝑥𝑏) ∈ 𝐾 ∧ (𝑦𝑏) ∈ 𝐾) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
142138, 139, 140, 141syl3anc 1366 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥𝑏)(+g𝑅)(𝑦𝑏))) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
143135, 142eqtrd 2685 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) = ((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))))
144143oveq1d 6705 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏𝑓 𝐺))))
14515ad2antrr 762 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑆 ∈ Ring)
14668ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐹:𝐾𝐶)
147146, 139ffvelrnd 6400 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑥𝑏)) ∈ 𝐶)
148146, 140ffvelrnd 6400 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝐹‘(𝑦𝑏)) ∈ 𝐶)
14959ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝑇 ∈ CMnd)
15038ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐺:𝐼𝐶)
1516ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → 𝐼 ∈ V)
15220, 51, 31, 52, 149, 131, 150, 151psrbagev2 19559 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (𝑇 Σg (𝑏𝑓 𝐺)) ∈ 𝐶)
15329, 94, 5ringdir 18613 . . . . . . . . . . . 12 ((𝑆 ∈ Ring ∧ ((𝐹‘(𝑥𝑏)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑏)) ∈ 𝐶 ∧ (𝑇 Σg (𝑏𝑓 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏𝑓 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
154145, 147, 148, 152, 153syl13anc 1368 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → (((𝐹‘(𝑥𝑏))(+g𝑆)(𝐹‘(𝑦𝑏))) · (𝑇 Σg (𝑏𝑓 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
155144, 154eqtrd 2685 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
156155mpteq2dva 4777 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
157104a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐷 ∈ V)
158 ovexd 6720 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) ∈ V)
159 ovexd 6720 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑏𝐷) → ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) ∈ V)
160 eqidd 2652 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
161 eqidd 2652 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
162157, 158, 159, 160, 161offval2 6956 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) ∘𝑓 (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑏𝐷 ↦ (((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))(+g𝑆)((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
163156, 162eqtr4d 2688 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) ∘𝑓 (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
164163oveq2d 6706 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) ∘𝑓 (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))))
165101adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CMnd)
1666adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐼 ∈ V)
1677adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑅 ∈ CRing)
16813adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑆 ∈ CRing)
16936adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐹 ∈ (𝑅 RingHom 𝑆))
17038adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝐺:𝐼𝐶)
17110, 1, 29, 22, 20, 30, 31, 5, 32, 33, 166, 167, 168, 169, 170, 122evlslem6 19561 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆)))
172171simpld 474 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶)
17310, 1, 29, 22, 20, 30, 31, 5, 32, 33, 166, 167, 168, 169, 170, 126evlslem6 19561 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶 ∧ (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆)))
174173simpld 474 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))):𝐷𝐶)
175171simprd 478 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆))
176173simprd 478 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) finSupp (0g𝑆))
17729, 99, 94, 165, 157, 172, 174, 175, 176gsumadd 18369 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg ((𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) ∘𝑓 (+g𝑆)(𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))))
178164, 177eqtrd 2685 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))))
17996adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑃 ∈ Grp)
1801, 93grpcl 17477 . . . . . . . 8 ((𝑃 ∈ Grp ∧ 𝑥𝐵𝑦𝐵) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
181179, 122, 126, 180syl3anc 1366 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝑃)𝑦) ∈ 𝐵)
182 fveq1 6228 . . . . . . . . . . . 12 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑝𝑏) = ((𝑥(+g𝑃)𝑦)‘𝑏))
183182fveq2d 6233 . . . . . . . . . . 11 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝐹‘(𝑝𝑏)) = (𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)))
184183oveq1d 6705 . . . . . . . . . 10 (𝑝 = (𝑥(+g𝑃)𝑦) → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))
185184mpteq2dv 4778 . . . . . . . . 9 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
186185oveq2d 6706 . . . . . . . 8 (𝑝 = (𝑥(+g𝑃)𝑦) → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
187 ovex 6718 . . . . . . . 8 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ V
188186, 33, 187fvmpt 6321 . . . . . . 7 ((𝑥(+g𝑃)𝑦) ∈ 𝐵 → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
189181, 188syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘((𝑥(+g𝑃)𝑦)‘𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
190 fveq1 6228 . . . . . . . . . . . . 13 (𝑝 = 𝑥 → (𝑝𝑏) = (𝑥𝑏))
191190fveq2d 6233 . . . . . . . . . . . 12 (𝑝 = 𝑥 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑥𝑏)))
192191oveq1d 6705 . . . . . . . . . . 11 (𝑝 = 𝑥 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))
193192mpteq2dv 4778 . . . . . . . . . 10 (𝑝 = 𝑥 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
194193oveq2d 6706 . . . . . . . . 9 (𝑝 = 𝑥 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
195 ovex 6718 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ V
196194, 33, 195fvmpt 6321 . . . . . . . 8 (𝑥𝐵 → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
197122, 196syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑥) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
198 fveq1 6228 . . . . . . . . . . . . 13 (𝑝 = 𝑦 → (𝑝𝑏) = (𝑦𝑏))
199198fveq2d 6233 . . . . . . . . . . . 12 (𝑝 = 𝑦 → (𝐹‘(𝑝𝑏)) = (𝐹‘(𝑦𝑏)))
200199oveq1d 6705 . . . . . . . . . . 11 (𝑝 = 𝑦 → ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))) = ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))
201200mpteq2dv 4778 . . . . . . . . . 10 (𝑝 = 𝑦 → (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))) = (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))
202201oveq2d 6706 . . . . . . . . 9 (𝑝 = 𝑦 → (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
203 ovex 6718 . . . . . . . . 9 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ V
204202, 33, 203fvmpt 6321 . . . . . . . 8 (𝑦𝐵 → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
205204ad2antll 765 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸𝑦) = (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))))
206197, 205oveq12d 6708 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((𝐸𝑥)(+g𝑆)(𝐸𝑦)) = ((𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑥𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))(+g𝑆)(𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑦𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺)))))))
207178, 189, 2063eqtr4d 2695 . . . . 5 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(+g𝑃)𝑦)) = ((𝐸𝑥)(+g𝑆)(𝐸𝑦)))
2081, 29, 93, 94, 96, 98, 116, 207isghmd 17716 . . . 4 (𝜑𝐸 ∈ (𝑃 GrpHom 𝑆))
209 eqid 2651 . . . . . . . . . . 11 (mulGrp‘𝑅) = (mulGrp‘𝑅)
210209, 30rhmmhm 18770 . . . . . . . . . 10 (𝐹 ∈ (𝑅 RingHom 𝑆) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
21136, 210syl 17 . . . . . . . . 9 (𝜑𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
212211adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇))
213 simprll 819 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥𝐵)
21410, 22, 1, 20, 213mplelf 19481 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑥:𝐷𝐾)
215 simprrl 821 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑧𝐷)
216214, 215ffvelrnd 6400 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑥𝑧) ∈ 𝐾)
217 simprlr 820 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦𝐵)
21810, 22, 1, 20, 217mplelf 19481 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑦:𝐷𝐾)
219 simprrr 822 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑤𝐷)
220218, 219ffvelrnd 6400 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑦𝑤) ∈ 𝐾)
221209, 22mgpbas 18541 . . . . . . . . 9 𝐾 = (Base‘(mulGrp‘𝑅))
222 eqid 2651 . . . . . . . . . 10 (.r𝑅) = (.r𝑅)
223209, 222mgpplusg 18539 . . . . . . . . 9 (.r𝑅) = (+g‘(mulGrp‘𝑅))
22430, 5mgpplusg 18539 . . . . . . . . 9 · = (+g𝑇)
225221, 223, 224mhmlin 17389 . . . . . . . 8 ((𝐹 ∈ ((mulGrp‘𝑅) MndHom 𝑇) ∧ (𝑥𝑧) ∈ 𝐾 ∧ (𝑦𝑤) ∈ 𝐾) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
226212, 216, 220, 225syl3anc 1366 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) = ((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))))
22761ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → 𝑇 ∈ Mnd)
228 simprl 809 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧𝐷)
22920psrbagf 19413 . . . . . . . . . . . . . . 15 ((𝐼 ∈ V ∧ 𝑧𝐷) → 𝑧:𝐼⟶ℕ0)
2306, 228, 229syl2an2r 893 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧:𝐼⟶ℕ0)
231230ffvelrnda 6399 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) ∈ ℕ0)
232 simprr 811 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤𝐷)
23320psrbagf 19413 . . . . . . . . . . . . . . 15 ((𝐼 ∈ V ∧ 𝑤𝐷) → 𝑤:𝐼⟶ℕ0)
2346, 232, 233syl2an2r 893 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤:𝐼⟶ℕ0)
235234ffvelrnda 6399 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) ∈ ℕ0)
23638adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺:𝐼𝐶)
237236ffvelrnda 6399 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ 𝐶)
23851, 31, 224mulgnn0dir 17618 . . . . . . . . . . . . 13 ((𝑇 ∈ Mnd ∧ ((𝑧𝑣) ∈ ℕ0 ∧ (𝑤𝑣) ∈ ℕ0 ∧ (𝐺𝑣) ∈ 𝐶)) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
239227, 231, 235, 237, 238syl13anc 1368 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣)) = (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣))))
240239mpteq2dva 4777 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
2416adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐼 ∈ V)
242 ovexd 6720 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) + (𝑤𝑣)) ∈ V)
243 fvexd 6241 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) ∈ V)
244230ffnd 6084 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑧 Fn 𝐼)
245234ffnd 6084 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑤 Fn 𝐼)
246 inidm 3855 . . . . . . . . . . . . 13 (𝐼𝐼) = 𝐼
247 eqidd 2652 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑧𝑣) = (𝑧𝑣))
248 eqidd 2652 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝑤𝑣) = (𝑤𝑣))
249244, 245, 241, 241, 246, 247, 248offval 6946 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧𝑓 + 𝑤) = (𝑣𝐼 ↦ ((𝑧𝑣) + (𝑤𝑣))))
25038feqmptd 6288 . . . . . . . . . . . . 13 (𝜑𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
251250adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 = (𝑣𝐼 ↦ (𝐺𝑣)))
252241, 242, 243, 249, 251offval2 6956 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺) = (𝑣𝐼 ↦ (((𝑧𝑣) + (𝑤𝑣)) (𝐺𝑣))))
253 ovexd 6720 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑧𝑣) (𝐺𝑣)) ∈ V)
254 ovexd 6720 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → ((𝑤𝑣) (𝐺𝑣)) ∈ V)
25538ffnd 6084 . . . . . . . . . . . . . 14 (𝜑𝐺 Fn 𝐼)
256255adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝐺 Fn 𝐼)
257 eqidd 2652 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐷𝑤𝐷)) ∧ 𝑣𝐼) → (𝐺𝑣) = (𝐺𝑣))
258244, 256, 241, 241, 246, 247, 257offval 6946 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧𝑓 𝐺) = (𝑣𝐼 ↦ ((𝑧𝑣) (𝐺𝑣))))
259245, 256, 241, 241, 246, 248, 257offval 6946 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤𝑓 𝐺) = (𝑣𝐼 ↦ ((𝑤𝑣) (𝐺𝑣))))
260241, 253, 254, 258, 259offval2 6956 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧𝑓 𝐺) ∘𝑓 · (𝑤𝑓 𝐺)) = (𝑣𝐼 ↦ (((𝑧𝑣) (𝐺𝑣)) · ((𝑤𝑣) (𝐺𝑣)))))
261240, 252, 2603eqtr4d 2695 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺) = ((𝑧𝑓 𝐺) ∘𝑓 · (𝑤𝑓 𝐺)))
262261oveq2d 6706 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺)) = (𝑇 Σg ((𝑧𝑓 𝐺) ∘𝑓 · (𝑤𝑓 𝐺))))
26359adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → 𝑇 ∈ CMnd)
26420, 51, 31, 52, 263, 228, 236, 241psrbagev1 19558 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑧𝑓 𝐺):𝐼𝐶 ∧ (𝑧𝑓 𝐺) finSupp (1r𝑆)))
265264simpld 474 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧𝑓 𝐺):𝐼𝐶)
26620, 51, 31, 52, 263, 232, 236, 241psrbagev1 19558 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → ((𝑤𝑓 𝐺):𝐼𝐶 ∧ (𝑤𝑓 𝐺) finSupp (1r𝑆)))
267266simpld 474 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤𝑓 𝐺):𝐼𝐶)
268264simprd 478 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑧𝑓 𝐺) finSupp (1r𝑆))
269266simprd 478 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑤𝑓 𝐺) finSupp (1r𝑆))
27051, 52, 224, 263, 241, 265, 267, 268, 269gsumadd 18369 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧𝑓 𝐺) ∘𝑓 · (𝑤𝑓 𝐺))) = ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺))))
271262, 270eqtrd 2685 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺)) = ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺))))
272271adantrl 752 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺)) = ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺))))
273226, 272oveq12d 6708 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
27459adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑇 ∈ CMnd)
27568adantr 480 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹:𝐾𝐶)
276275, 216ffvelrnd 6400 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑥𝑧)) ∈ 𝐶)
277275, 220ffvelrnd 6400 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐹‘(𝑦𝑤)) ∈ 𝐶)
27820, 51, 31, 52, 263, 228, 236, 241psrbagev2 19559 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑧𝑓 𝐺)) ∈ 𝐶)
279278adantrl 752 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑧𝑓 𝐺)) ∈ 𝐶)
28020, 51, 31, 52, 263, 232, 236, 241psrbagev2 19559 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐷𝑤𝐷)) → (𝑇 Σg (𝑤𝑓 𝐺)) ∈ 𝐶)
281280adantrl 752 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑇 Σg (𝑤𝑓 𝐺)) ∈ 𝐶)
28251, 224cmn4 18258 . . . . . . 7 ((𝑇 ∈ CMnd ∧ ((𝐹‘(𝑥𝑧)) ∈ 𝐶 ∧ (𝐹‘(𝑦𝑤)) ∈ 𝐶) ∧ ((𝑇 Σg (𝑧𝑓 𝐺)) ∈ 𝐶 ∧ (𝑇 Σg (𝑤𝑓 𝐺)) ∈ 𝐶)) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
283274, 276, 277, 279, 281, 282syl122anc 1375 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (((𝐹‘(𝑥𝑧)) · (𝐹‘(𝑦𝑤))) · ((𝑇 Σg (𝑧𝑓 𝐺)) · (𝑇 Σg (𝑤𝑓 𝐺)))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
284273, 283eqtrd 2685 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
2856adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐼 ∈ V)
2867adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ CRing)
28713adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑆 ∈ CRing)
28836adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐹 ∈ (𝑅 RingHom 𝑆))
28938adantr 480 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝐺:𝐼𝐶)
29020psrbagaddcl 19418 . . . . . . 7 ((𝐼 ∈ V ∧ 𝑧𝐷𝑤𝐷) → (𝑧𝑓 + 𝑤) ∈ 𝐷)
291285, 215, 219, 290syl3anc 1366 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝑧𝑓 + 𝑤) ∈ 𝐷)
2929adantr 480 . . . . . . 7 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → 𝑅 ∈ Ring)
29322, 222ringcl 18607 . . . . . . 7 ((𝑅 ∈ Ring ∧ (𝑥𝑧) ∈ 𝐾 ∧ (𝑦𝑤) ∈ 𝐾) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ 𝐾)
294292, 216, 220, 293syl3anc 1366 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝑥𝑧)(.r𝑅)(𝑦𝑤)) ∈ 𝐾)
29510, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 291, 294evlslem3 19562 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧𝑓 + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐹‘((𝑥𝑧)(.r𝑅)(𝑦𝑤))) · (𝑇 Σg ((𝑧𝑓 + 𝑤) ∘𝑓 𝐺))))
29610, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 215, 216evlslem3 19562 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) = ((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))))
29710, 1, 29, 22, 20, 30, 31, 5, 32, 33, 285, 286, 287, 288, 289, 21, 219, 220evlslem3 19562 . . . . . 6 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅)))) = ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺))))
298296, 297oveq12d 6708 . . . . 5 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))) = (((𝐹‘(𝑥𝑧)) · (𝑇 Σg (𝑧𝑓 𝐺))) · ((𝐹‘(𝑦𝑤)) · (𝑇 Σg (𝑤𝑓 𝐺)))))
299284, 295, 2983eqtr4d 2695 . . . 4 ((𝜑 ∧ ((𝑥𝐵𝑦𝐵) ∧ (𝑧𝐷𝑤𝐷))) → (𝐸‘(𝑣𝐷 ↦ if(𝑣 = (𝑧𝑓 + 𝑤), ((𝑥𝑧)(.r𝑅)(𝑦𝑤)), (0g𝑅)))) = ((𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑧, (𝑥𝑧), (0g𝑅)))) · (𝐸‘(𝑣𝐷 ↦ if(𝑣 = 𝑤, (𝑦𝑤), (0g𝑅))))))
30010, 1, 5, 21, 20, 6, 7, 13, 208, 299evlslem2 19560 . . 3 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝐸‘(𝑥(.r𝑃)𝑦)) = ((𝐸𝑥) · (𝐸𝑦)))
3011, 2, 3, 4, 5, 12, 15, 92, 300, 29, 93, 94, 116, 207isrhmd 18777 . 2 (𝜑𝐸 ∈ (𝑃 RingHom 𝑆))
302 ovex 6718 . . . . . 6 (𝑆 Σg (𝑏𝐷 ↦ ((𝐹‘(𝑝𝑏)) · (𝑇 Σg (𝑏𝑓 𝐺))))) ∈ V
303302, 33fnmpti 6060 . . . . 5 𝐸 Fn 𝐵
304303a1i 11 . . . 4 (𝜑𝐸 Fn 𝐵)
30522, 1rhmf 18774 . . . . . 6 (𝐴 ∈ (𝑅 RingHom 𝑃) → 𝐴:𝐾𝐵)
30686, 305syl 17 . . . . 5 (𝜑𝐴:𝐾𝐵)
307306ffnd 6084 . . . 4 (𝜑𝐴 Fn 𝐾)
308 frn 6091 . . . . 5 (𝐴:𝐾𝐵 → ran 𝐴𝐵)
309306, 308syl 17 . . . 4 (𝜑 → ran 𝐴𝐵)
310 fnco 6037 . . . 4 ((𝐸 Fn 𝐵𝐴 Fn 𝐾 ∧ ran 𝐴𝐵) → (𝐸𝐴) Fn 𝐾)
311304, 307, 309, 310syl3anc 1366 . . 3 (𝜑 → (𝐸𝐴) Fn 𝐾)
31268ffnd 6084 . . 3 (𝜑𝐹 Fn 𝐾)
313 fvco2 6312 . . . . 5 ((𝐴 Fn 𝐾𝑥𝐾) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
314307, 313sylan 487 . . . 4 ((𝜑𝑥𝐾) → ((𝐸𝐴)‘𝑥) = (𝐸‘(𝐴𝑥)))
315314, 73eqtrd 2685 . . 3 ((𝜑𝑥𝐾) → ((𝐸𝐴)‘𝑥) = (𝐹𝑥))
316311, 312, 315eqfnfvd 6354 . 2 (𝜑 → (𝐸𝐴) = 𝐹)
31710, 32, 1, 6, 9mvrf2 19540 . . . . 5 (𝜑𝑉:𝐼𝐵)
318317ffnd 6084 . . . 4 (𝜑𝑉 Fn 𝐼)
319 frn 6091 . . . . 5 (𝑉:𝐼𝐵 → ran 𝑉𝐵)
320317, 319syl 17 . . . 4 (𝜑 → ran 𝑉𝐵)
321 fnco 6037 . . . 4 ((𝐸 Fn 𝐵𝑉 Fn 𝐼 ∧ ran 𝑉𝐵) → (𝐸𝑉) Fn 𝐼)
322304, 318, 320, 321syl3anc 1366 . . 3 (𝜑 → (𝐸𝑉) Fn 𝐼)
323 fvco2 6312 . . . . 5 ((𝑉 Fn 𝐼𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
324318, 323sylan 487 . . . 4 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐸‘(𝑉𝑥)))
3256adantr 480 . . . . . . 7 ((𝜑𝑥𝐼) → 𝐼 ∈ V)
3267adantr 480 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑅 ∈ CRing)
327 simpr 476 . . . . . . 7 ((𝜑𝑥𝐼) → 𝑥𝐼)
32832, 20, 21, 75, 325, 326, 327mvrval 19469 . . . . . 6 ((𝜑𝑥𝐼) → (𝑉𝑥) = (𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅))))
329328fveq2d 6233 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))))
33013adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → 𝑆 ∈ CRing)
33136adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → 𝐹 ∈ (𝑅 RingHom 𝑆))
33238adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → 𝐺:𝐼𝐶)
33320psrbagsn 19543 . . . . . . . 8 (𝐼 ∈ V → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
3346, 333syl 17 . . . . . . 7 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
335334adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∈ 𝐷)
33677adantr 480 . . . . . 6 ((𝜑𝑥𝐼) → (1r𝑅) ∈ 𝐾)
33710, 1, 29, 22, 20, 30, 31, 5, 32, 33, 325, 326, 330, 331, 332, 21, 335, 336evlslem3 19562 . . . . 5 ((𝜑𝑥𝐼) → (𝐸‘(𝑦𝐷 ↦ if(𝑦 = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)), (1r𝑅), (0g𝑅)))) = ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺))))
33891adantr 480 . . . . . . 7 ((𝜑𝑥𝐼) → (𝐹‘(1r𝑅)) = (1r𝑆))
339 1nn0 11346 . . . . . . . . . . . . . 14 1 ∈ ℕ0
340 0nn0 11345 . . . . . . . . . . . . . 14 0 ∈ ℕ0
341339, 340keepel 4188 . . . . . . . . . . . . 13 if(𝑧 = 𝑥, 1, 0) ∈ ℕ0
342341a1i 11 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → if(𝑧 = 𝑥, 1, 0) ∈ ℕ0)
34338ffvelrnda 6399 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
344 eqidd 2652 . . . . . . . . . . . 12 (𝜑 → (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)))
34538feqmptd 6288 . . . . . . . . . . . 12 (𝜑𝐺 = (𝑧𝐼 ↦ (𝐺𝑧)))
3466, 342, 343, 344, 345offval2 6956 . . . . . . . . . . 11 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺) = (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))))
347 oveq1 6697 . . . . . . . . . . . . . 14 (1 = if(𝑧 = 𝑥, 1, 0) → (1 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
348347eqeq1d 2653 . . . . . . . . . . . . 13 (1 = if(𝑧 = 𝑥, 1, 0) → ((1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
349 oveq1 6697 . . . . . . . . . . . . . 14 (0 = if(𝑧 = 𝑥, 1, 0) → (0 (𝐺𝑧)) = (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)))
350349eqeq1d 2653 . . . . . . . . . . . . 13 (0 = if(𝑧 = 𝑥, 1, 0) → ((0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ↔ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
351343adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (𝐺𝑧) ∈ 𝐶)
35251, 31mulg1 17595 . . . . . . . . . . . . . . 15 ((𝐺𝑧) ∈ 𝐶 → (1 (𝐺𝑧)) = (𝐺𝑧))
353351, 352syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = (𝐺𝑧))
354 iftrue 4125 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
355354adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑧))
356353, 355eqtr4d 2688 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ 𝑧 = 𝑥) → (1 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
35751, 52, 31mulg0 17593 . . . . . . . . . . . . . . . 16 ((𝐺𝑧) ∈ 𝐶 → (0 (𝐺𝑧)) = (1r𝑆))
358343, 357syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝐼) → (0 (𝐺𝑧)) = (1r𝑆))
359358adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = (1r𝑆))
360 iffalse 4128 . . . . . . . . . . . . . . 15 𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
361360adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
362359, 361eqtr4d 2688 . . . . . . . . . . . . 13 (((𝜑𝑧𝐼) ∧ ¬ 𝑧 = 𝑥) → (0 (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
363348, 350, 356, 362ifbothda 4156 . . . . . . . . . . . 12 ((𝜑𝑧𝐼) → (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧)) = if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
364363mpteq2dva 4777 . . . . . . . . . . 11 (𝜑 → (𝑧𝐼 ↦ (if(𝑧 = 𝑥, 1, 0) (𝐺𝑧))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
365346, 364eqtrd 2685 . . . . . . . . . 10 (𝜑 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
366365adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))))
367366oveq2d 6706 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺)) = (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))))
36861adantr 480 . . . . . . . . 9 ((𝜑𝑥𝐼) → 𝑇 ∈ Mnd)
369343adantlr 751 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (𝐺𝑧) ∈ 𝐶)
37029, 3ringidcl 18614 . . . . . . . . . . . . 13 (𝑆 ∈ Ring → (1r𝑆) ∈ 𝐶)
37115, 370syl 17 . . . . . . . . . . . 12 (𝜑 → (1r𝑆) ∈ 𝐶)
372371ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → (1r𝑆) ∈ 𝐶)
373369, 372ifcld 4164 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧𝐼) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) ∈ 𝐶)
374 eqid 2651 . . . . . . . . . 10 (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) = (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))
375373, 374fmptd 6425 . . . . . . . . 9 ((𝜑𝑥𝐼) → (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))):𝐼𝐶)
376 eldifn 3766 . . . . . . . . . . . . 13 (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 ∈ {𝑥})
377 velsn 4226 . . . . . . . . . . . . 13 (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥)
378376, 377sylnib 317 . . . . . . . . . . . 12 (𝑧 ∈ (𝐼 ∖ {𝑥}) → ¬ 𝑧 = 𝑥)
379378, 360syl 17 . . . . . . . . . . 11 (𝑧 ∈ (𝐼 ∖ {𝑥}) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
380379adantl 481 . . . . . . . . . 10 (((𝜑𝑥𝐼) ∧ 𝑧 ∈ (𝐼 ∖ {𝑥})) → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (1r𝑆))
381380, 325suppss2 7374 . . . . . . . . 9 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆))) supp (1r𝑆)) ⊆ {𝑥})
38251, 52, 368, 325, 327, 375, 381gsumpt 18407 . . . . . . . 8 ((𝜑𝑥𝐼) → (𝑇 Σg (𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))) = ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥))
383 fveq2 6229 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝐺𝑧) = (𝐺𝑥))
384354, 383eqtrd 2685 . . . . . . . . . 10 (𝑧 = 𝑥 → if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)) = (𝐺𝑥))
385 fvex 6239 . . . . . . . . . 10 (𝐺𝑥) ∈ V
386384, 374, 385fvmpt 6321 . . . . . . . . 9 (𝑥𝐼 → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
387386adantl 481 . . . . . . . 8 ((𝜑𝑥𝐼) → ((𝑧𝐼 ↦ if(𝑧 = 𝑥, (𝐺𝑧), (1r𝑆)))‘𝑥) = (𝐺𝑥))
388367, 382, 3873eqtrd 2689 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺)) = (𝐺𝑥))
389338, 388oveq12d 6708 . . . . . 6 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺))) = ((1r𝑆) · (𝐺𝑥)))
39029, 5, 3ringlidm 18617 . . . . . . 7 ((𝑆 ∈ Ring ∧ (𝐺𝑥) ∈ 𝐶) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
39115, 50, 390syl2an2r 893 . . . . . 6 ((𝜑𝑥𝐼) → ((1r𝑆) · (𝐺𝑥)) = (𝐺𝑥))
392389, 391eqtrd 2685 . . . . 5 ((𝜑𝑥𝐼) → ((𝐹‘(1r𝑅)) · (𝑇 Σg ((𝑧𝐼 ↦ if(𝑧 = 𝑥, 1, 0)) ∘𝑓 𝐺))) = (𝐺𝑥))
393329, 337, 3923eqtrd 2689 . . . 4 ((𝜑𝑥𝐼) → (𝐸‘(𝑉𝑥)) = (𝐺𝑥))
394324, 393eqtrd 2685 . . 3 ((𝜑𝑥𝐼) → ((𝐸𝑉)‘𝑥) = (𝐺𝑥))
395322, 255, 394eqfnfvd 6354 . 2 (𝜑 → (𝐸𝑉) = 𝐺)
396301, 316, 3953jca 1261 1 (𝜑 → (𝐸 ∈ (𝑃 RingHom 𝑆) ∧ (𝐸𝐴) = 𝐹 ∧ (𝐸𝑉) = 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  {crab 2945  Vcvv 3231  cdif 3604  wss 3607  ifcif 4119  {csn 4210   class class class wbr 4685  cmpt 4762   × cxp 5141  ccnv 5142  ran crn 5144  cima 5146  ccom 5147   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  𝑓 cof 6937  𝑚 cmap 7899  Fincfn 7997   finSupp cfsupp 8316  0cc0 9974  1c1 9975   + caddc 9977  cn 11058  0cn0 11330  cz 11415  Basecbs 15904  +gcplusg 15988  .rcmulr 15989  Scalarcsca 15991  0gc0g 16147   Σg cgsu 16148  Mndcmnd 17341   MndHom cmhm 17380  Grpcgrp 17469  .gcmg 17587   GrpHom cghm 17704  CMndccmn 18239  mulGrpcmgp 18535  1rcur 18547  Ringcrg 18593  CRingccrg 18594   RingHom crh 18760  AssAlgcasa 19357  algSccascl 19359   mVar cmvr 19400   mPoly cmpl 19401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-ofr 6940  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-sca 16004  df-vsca 16005  df-tset 16007  df-0g 16149  df-gsum 16150  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-mhm 17382  df-submnd 17383  df-grp 17472  df-minusg 17473  df-sbg 17474  df-mulg 17588  df-subg 17638  df-ghm 17705  df-cntz 17796  df-cmn 18241  df-abl 18242  df-mgp 18536  df-ur 18548  df-ring 18595  df-cring 18596  df-rnghom 18763  df-subrg 18826  df-lmod 18913  df-lss 18981  df-assa 19360  df-ascl 19362  df-psr 19404  df-mvr 19405  df-mpl 19406
This theorem is referenced by:  evlseu  19564
  Copyright terms: Public domain W3C validator