Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mhphf Structured version   Visualization version   GIF version

Theorem mhphf 40757
Description: A homogeneous polynomial defines a homogeneous function. Equivalently, an algebraic form is a homogeneous function. (An algebraic form is the function corresponding to a homogeneous polynomial, which in this case is the (𝑄𝑋) which corresponds to 𝑋). (Contributed by SN, 28-Jul-2024.)
Hypotheses
Ref Expression
mhphf.q 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
mhphf.h 𝐻 = (𝐼 mHomP 𝑈)
mhphf.u 𝑈 = (𝑆s 𝑅)
mhphf.k 𝐾 = (Base‘𝑆)
mhphf.m · = (.r𝑆)
mhphf.e = (.g‘(mulGrp‘𝑆))
mhphf.i (𝜑𝐼𝑉)
mhphf.s (𝜑𝑆 ∈ CRing)
mhphf.r (𝜑𝑅 ∈ (SubRing‘𝑆))
mhphf.l (𝜑𝐿𝑅)
mhphf.n (𝜑𝑁 ∈ ℕ0)
mhphf.x (𝜑𝑋 ∈ (𝐻𝑁))
mhphf.a (𝜑𝐴 ∈ (𝐾m 𝐼))
Assertion
Ref Expression
mhphf (𝜑 → ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴)))

Proof of Theorem mhphf
Dummy variables 𝑎 𝑏 𝑓 𝑠 𝑗 𝑘 𝑣 𝑥 𝑦 𝑤 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mhphf.h . . 3 𝐻 = (𝐼 mHomP 𝑈)
2 eqid 2736 . . 3 (Base‘𝑈) = (Base‘𝑈)
3 eqid 2736 . . 3 (0g𝑈) = (0g𝑈)
4 eqid 2736 . . 3 (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈)
5 eqid 2736 . . 3 (+g‘(𝐼 mPoly 𝑈)) = (+g‘(𝐼 mPoly 𝑈))
6 eqid 2736 . . 3 { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
7 eqid 2736 . . 3 {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} = {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}
8 mhphf.i . . 3 (𝜑𝐼𝑉)
9 mhphf.r . . . . 5 (𝜑𝑅 ∈ (SubRing‘𝑆))
10 mhphf.u . . . . . 6 𝑈 = (𝑆s 𝑅)
1110subrgring 20225 . . . . 5 (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
129, 11syl 17 . . . 4 (𝜑𝑈 ∈ Ring)
1312ringgrpd 19973 . . 3 (𝜑𝑈 ∈ Grp)
14 mhphf.n . . 3 (𝜑𝑁 ∈ ℕ0)
15 mhphf.x . . 3 (𝜑𝑋 ∈ (𝐻𝑁))
16 eqid 2736 . . . . . 6 (algSc‘(𝐼 mPoly 𝑈)) = (algSc‘(𝐼 mPoly 𝑈))
17 eqid 2736 . . . . . 6 (0g‘(𝐼 mPoly 𝑈)) = (0g‘(𝐼 mPoly 𝑈))
18 mhphf.s . . . . . . 7 (𝜑𝑆 ∈ CRing)
1910subrgcrng 20226 . . . . . . 7 ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing)
2018, 9, 19syl2anc 584 . . . . . 6 (𝜑𝑈 ∈ CRing)
214, 16, 3, 17, 8, 20mplascl0 40730 . . . . 5 (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) = (0g‘(𝐼 mPoly 𝑈)))
224, 6, 3, 17, 8, 13mpl0 21412 . . . . 5 (𝜑 → (0g‘(𝐼 mPoly 𝑈)) = ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {(0g𝑈)}))
2321, 22eqtr2d 2777 . . . 4 (𝜑 → ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {(0g𝑈)}) = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))
24 mhphf.m . . . . . . . . . 10 · = (.r𝑆)
2510, 24ressmulr 17188 . . . . . . . . 9 (𝑅 ∈ (SubRing‘𝑆) → · = (.r𝑈))
269, 25syl 17 . . . . . . . 8 (𝜑· = (.r𝑈))
2726oveqd 7374 . . . . . . 7 (𝜑 → ((𝑁 𝐿) · (0g𝑈)) = ((𝑁 𝐿)(.r𝑈)(0g𝑈)))
28 eqid 2736 . . . . . . . . . . . 12 (mulGrp‘𝑆) = (mulGrp‘𝑆)
2928subrgsubm 20235 . . . . . . . . . . 11 (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)))
309, 29syl 17 . . . . . . . . . 10 (𝜑𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)))
31 mhphf.l . . . . . . . . . 10 (𝜑𝐿𝑅)
32 mhphf.e . . . . . . . . . . 11 = (.g‘(mulGrp‘𝑆))
3332submmulgcl 18919 . . . . . . . . . 10 ((𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)) ∧ 𝑁 ∈ ℕ0𝐿𝑅) → (𝑁 𝐿) ∈ 𝑅)
3430, 14, 31, 33syl3anc 1371 . . . . . . . . 9 (𝜑 → (𝑁 𝐿) ∈ 𝑅)
3510subrgbas 20231 . . . . . . . . . 10 (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
369, 35syl 17 . . . . . . . . 9 (𝜑𝑅 = (Base‘𝑈))
3734, 36eleqtrd 2840 . . . . . . . 8 (𝜑 → (𝑁 𝐿) ∈ (Base‘𝑈))
38 eqid 2736 . . . . . . . . 9 (.r𝑈) = (.r𝑈)
392, 38, 3ringrz 20012 . . . . . . . 8 ((𝑈 ∈ Ring ∧ (𝑁 𝐿) ∈ (Base‘𝑈)) → ((𝑁 𝐿)(.r𝑈)(0g𝑈)) = (0g𝑈))
4012, 37, 39syl2anc 584 . . . . . . 7 (𝜑 → ((𝑁 𝐿)(.r𝑈)(0g𝑈)) = (0g𝑈))
4127, 40eqtrd 2776 . . . . . 6 (𝜑 → ((𝑁 𝐿) · (0g𝑈)) = (0g𝑈))
42 mhphf.q . . . . . . . . 9 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
43 mhphf.k . . . . . . . . 9 𝐾 = (Base‘𝑆)
44 eqid 2736 . . . . . . . . 9 (Base‘(𝐼 mPoly 𝑈)) = (Base‘(𝐼 mPoly 𝑈))
452, 3ring0cl 19990 . . . . . . . . . . 11 (𝑈 ∈ Ring → (0g𝑈) ∈ (Base‘𝑈))
4612, 45syl 17 . . . . . . . . . 10 (𝜑 → (0g𝑈) ∈ (Base‘𝑈))
4746, 36eleqtrrd 2841 . . . . . . . . 9 (𝜑 → (0g𝑈) ∈ 𝑅)
48 mhphf.a . . . . . . . . 9 (𝜑𝐴 ∈ (𝐾m 𝐼))
4942, 4, 10, 43, 44, 16, 8, 18, 9, 47, 48evlsscaval 40734 . . . . . . . 8 (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴) = (0g𝑈)))
5049simprd 496 . . . . . . 7 (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴) = (0g𝑈))
5150oveq2d 7373 . . . . . 6 (𝜑 → ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴)) = ((𝑁 𝐿) · (0g𝑈)))
5243fvexi 6856 . . . . . . . . . 10 𝐾 ∈ V
5352a1i 11 . . . . . . . . 9 (𝜑𝐾 ∈ V)
5418crngringd 19977 . . . . . . . . . . . 12 (𝜑𝑆 ∈ Ring)
5543, 24ringcl 19981 . . . . . . . . . . . 12 ((𝑆 ∈ Ring ∧ 𝑗𝐾𝑘𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
5654, 55syl3an1 1163 . . . . . . . . . . 11 ((𝜑𝑗𝐾𝑘𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
57563expb 1120 . . . . . . . . . 10 ((𝜑 ∧ (𝑗𝐾𝑘𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
5843subrgss 20223 . . . . . . . . . . . . 13 (𝑅 ∈ (SubRing‘𝑆) → 𝑅𝐾)
599, 58syl 17 . . . . . . . . . . . 12 (𝜑𝑅𝐾)
6059, 31sseldd 3945 . . . . . . . . . . 11 (𝜑𝐿𝐾)
61 fconst6g 6731 . . . . . . . . . . 11 (𝐿𝐾 → (𝐼 × {𝐿}):𝐼𝐾)
6260, 61syl 17 . . . . . . . . . 10 (𝜑 → (𝐼 × {𝐿}):𝐼𝐾)
63 elmapi 8787 . . . . . . . . . . 11 (𝐴 ∈ (𝐾m 𝐼) → 𝐴:𝐼𝐾)
6448, 63syl 17 . . . . . . . . . 10 (𝜑𝐴:𝐼𝐾)
65 inidm 4178 . . . . . . . . . 10 (𝐼𝐼) = 𝐼
6657, 62, 64, 8, 8, 65off 7635 . . . . . . . . 9 (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼𝐾)
6753, 8, 66elmapdd 40664 . . . . . . . 8 (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾m 𝐼))
6842, 4, 10, 43, 44, 16, 8, 18, 9, 47, 67evlsscaval 40734 . . . . . . 7 (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (0g𝑈)))
6968simprd 496 . . . . . 6 (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (0g𝑈))
7041, 51, 693eqtr4rd 2787 . . . . 5 (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴)))
71 fvex 6855 . . . . . 6 ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ V
72 fveq2 6842 . . . . . . . 8 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → (𝑄𝑓) = (𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈))))
7372fveq1d 6844 . . . . . . 7 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
7472fveq1d 6844 . . . . . . . 8 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → ((𝑄𝑓)‘𝐴) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴))
7574oveq2d 7373 . . . . . . 7 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴)))
7673, 75eqeq12d 2752 . . . . . 6 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴))))
7771, 76elab 3630 . . . . 5 (((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴)))
7870, 77sylibr 233 . . . 4 (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
7923, 78eqeltrd 2838 . . 3 (𝜑 → ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {(0g𝑈)}) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
804mplassa 21427 . . . . . . . . 9 ((𝐼𝑉𝑈 ∈ CRing) → (𝐼 mPoly 𝑈) ∈ AssAlg)
818, 20, 80syl2anc 584 . . . . . . . 8 (𝜑 → (𝐼 mPoly 𝑈) ∈ AssAlg)
8281adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 mPoly 𝑈) ∈ AssAlg)
834, 8, 12mplsca 21417 . . . . . . . . . . 11 (𝜑𝑈 = (Scalar‘(𝐼 mPoly 𝑈)))
8483fveq2d 6846 . . . . . . . . . 10 (𝜑 → (Base‘𝑈) = (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
8584eleq2d 2823 . . . . . . . . 9 (𝜑 → (𝑏 ∈ (Base‘𝑈) ↔ 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈)))))
8685biimpa 477 . . . . . . . 8 ((𝜑𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
8786adantrl 714 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
88 fvexd 6857 . . . . . . . . . . 11 (𝜑 → (Base‘𝑈) ∈ V)
89 ovex 7390 . . . . . . . . . . . . 13 (ℕ0m 𝐼) ∈ V
9089rabex 5289 . . . . . . . . . . . 12 { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∈ V
9190a1i 11 . . . . . . . . . . 11 (𝜑 → { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∈ V)
92 eqid 2736 . . . . . . . . . . . . . . . 16 (1r𝑈) = (1r𝑈)
932, 92ringidcl 19989 . . . . . . . . . . . . . . 15 (𝑈 ∈ Ring → (1r𝑈) ∈ (Base‘𝑈))
9412, 93syl 17 . . . . . . . . . . . . . 14 (𝜑 → (1r𝑈) ∈ (Base‘𝑈))
9594, 46ifcld 4532 . . . . . . . . . . . . 13 (𝜑 → if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) ∈ (Base‘𝑈))
9695adantr 481 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) ∈ (Base‘𝑈))
9796fmpttd 7063 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))):{ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}⟶(Base‘𝑈))
9888, 91, 97elmapdd 40664 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ ((Base‘𝑈) ↑m { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}))
99 eqid 2736 . . . . . . . . . . 11 (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈)
100 eqid 2736 . . . . . . . . . . 11 (Base‘(𝐼 mPwSer 𝑈)) = (Base‘(𝐼 mPwSer 𝑈))
10199, 2, 6, 100, 8psrbas 21346 . . . . . . . . . 10 (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑m { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}))
10298, 101eleqtrrd 2841 . . . . . . . . 9 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈)))
10390mptex 7173 . . . . . . . . . . 11 (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ V
104103a1i 11 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ V)
105 fvexd 6857 . . . . . . . . . 10 (𝜑 → (0g𝑈) ∈ V)
106 funmpt 6539 . . . . . . . . . . 11 Fun (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))
107106a1i 11 . . . . . . . . . 10 (𝜑 → Fun (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))))
108 snfi 8988 . . . . . . . . . . . 12 {𝑎} ∈ Fin
109108a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑎} ∈ Fin)
110 eldifsnneq 4751 . . . . . . . . . . . . . 14 (𝑤 ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑎}) → ¬ 𝑤 = 𝑎)
111110adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑎})) → ¬ 𝑤 = 𝑎)
112111iffalsed 4497 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑎})) → if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) = (0g𝑈))
113112, 91suppss2 8131 . . . . . . . . . . 11 (𝜑 → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) supp (0g𝑈)) ⊆ {𝑎})
114109, 113ssfid 9211 . . . . . . . . . 10 (𝜑 → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) supp (0g𝑈)) ∈ Fin)
115104, 105, 107, 114isfsuppd 40665 . . . . . . . . 9 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) finSupp (0g𝑈))
1164, 99, 100, 3, 44mplelbas 21399 . . . . . . . . 9 ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ↔ ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈)) ∧ (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) finSupp (0g𝑈)))
117102, 115, 116sylanbrc 583 . . . . . . . 8 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)))
118117adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)))
119 eqid 2736 . . . . . . . 8 (Scalar‘(𝐼 mPoly 𝑈)) = (Scalar‘(𝐼 mPoly 𝑈))
120 eqid 2736 . . . . . . . 8 (Base‘(Scalar‘(𝐼 mPoly 𝑈))) = (Base‘(Scalar‘(𝐼 mPoly 𝑈)))
121 eqid 2736 . . . . . . . 8 (.r‘(𝐼 mPoly 𝑈)) = (.r‘(𝐼 mPoly 𝑈))
122 eqid 2736 . . . . . . . 8 ( ·𝑠 ‘(𝐼 mPoly 𝑈)) = ( ·𝑠 ‘(𝐼 mPoly 𝑈))
12316, 119, 120, 44, 121, 122asclmul1 21289 . . . . . . 7 (((𝐼 mPoly 𝑈) ∈ AssAlg ∧ 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))) ∧ (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑏( ·𝑠 ‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))
12482, 87, 118, 123syl3anc 1371 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑏( ·𝑠 ‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))
125 simprr 771 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘𝑈))
1264, 122, 2, 44, 38, 6, 125, 118mplvsca 21419 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑏( ·𝑠 ‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r𝑈)(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))
127124, 126eqtrd 2776 . . . . 5 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r𝑈)(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))
128 vex 3449 . . . . . . 7 𝑏 ∈ V
129 fnconstg 6730 . . . . . . 7 (𝑏 ∈ V → ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) Fn { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
130128, 129mp1i 13 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) Fn { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
131 fvex 6855 . . . . . . . . 9 (1r𝑈) ∈ V
132 fvex 6855 . . . . . . . . 9 (0g𝑈) ∈ V
133131, 132ifex 4536 . . . . . . . 8 if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) ∈ V
134 eqid 2736 . . . . . . . 8 (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) = (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))
135133, 134fnmpti 6644 . . . . . . 7 (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) Fn { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
136135a1i 11 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) Fn { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
13790a1i 11 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∈ V)
138 inidm 4178 . . . . . 6 ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∩ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
139128fvconst2 7153 . . . . . . 7 (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏})‘𝑠) = 𝑏)
140139adantl 482 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏})‘𝑠) = 𝑏)
141 equequ1 2028 . . . . . . . . 9 (𝑤 = 𝑠 → (𝑤 = 𝑎𝑠 = 𝑎))
142141ifbid 4509 . . . . . . . 8 (𝑤 = 𝑠 → if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) = if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))
143131, 132ifex 4536 . . . . . . . 8 if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)) ∈ V
144142, 134, 143fvmpt 6948 . . . . . . 7 (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))‘𝑠) = if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))
145144adantl 482 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))‘𝑠) = if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))
146130, 136, 137, 137, 138, 140, 145offval 7626 . . . . 5 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r𝑈)(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ (𝑏(.r𝑈)if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))))
147 ovif2 7455 . . . . . . 7 (𝑏(.r𝑈)if(𝑠 = 𝑎, (1r𝑈), (0g𝑈))) = if(𝑠 = 𝑎, (𝑏(.r𝑈)(1r𝑈)), (𝑏(.r𝑈)(0g𝑈)))
14812ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → 𝑈 ∈ Ring)
149 simplrr 776 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → 𝑏 ∈ (Base‘𝑈))
1502, 38, 92, 148, 149ringridmd 40692 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑏(.r𝑈)(1r𝑈)) = 𝑏)
1512, 38, 3ringrz 20012 . . . . . . . . 9 ((𝑈 ∈ Ring ∧ 𝑏 ∈ (Base‘𝑈)) → (𝑏(.r𝑈)(0g𝑈)) = (0g𝑈))
152148, 149, 151syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑏(.r𝑈)(0g𝑈)) = (0g𝑈))
153150, 152ifeq12d 4507 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → if(𝑠 = 𝑎, (𝑏(.r𝑈)(1r𝑈)), (𝑏(.r𝑈)(0g𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g𝑈)))
154147, 153eqtrid 2788 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑏(.r𝑈)if(𝑠 = 𝑎, (1r𝑈), (0g𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g𝑈)))
155154mpteq2dva 5205 . . . . 5 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ (𝑏(.r𝑈)if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g𝑈))))
156127, 146, 1553eqtrd 2780 . . . 4 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g𝑈))))
1578adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐼𝑉)
15818adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ CRing)
1599adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑅 ∈ (SubRing‘𝑆))
16067adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾m 𝐼))
16112adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑈 ∈ Ring)
1624, 44, 2, 16, 157, 161mplasclf 21473 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (algSc‘(𝐼 mPoly 𝑈)):(Base‘𝑈)⟶(Base‘(𝐼 mPoly 𝑈)))
163162, 125ffvelcdmd 7036 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)))
164 eqidd 2737 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
165163, 164jca 512 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴))))
166 elrabi 3639 . . . . . . . . . 10 (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} → 𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
167166ad2antrl 726 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
16842, 4, 10, 44, 43, 28, 32, 3, 92, 6, 134, 157, 158, 159, 160, 167evlsbagval 40736 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))))
16942, 4, 10, 43, 44, 157, 158, 159, 160, 165, 168, 121, 24evlsmulval 40739 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))))))
170169simprd 496 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))))
17128, 43mgpbas 19902 . . . . . . . . . . . 12 𝐾 = (Base‘(mulGrp‘𝑆))
17228ringmgp 19970 . . . . . . . . . . . . 13 (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
17354, 172syl 17 . . . . . . . . . . . 12 (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
174171, 32, 173, 14, 60mulgnn0cld 18897 . . . . . . . . . . 11 (𝜑 → (𝑁 𝐿) ∈ 𝐾)
175174adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑁 𝐿) ∈ 𝐾)
17636, 59eqsstrrd 3983 . . . . . . . . . . . 12 (𝜑 → (Base‘𝑈) ⊆ 𝐾)
177176sselda 3944 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (Base‘𝑈)) → 𝑏𝐾)
178177adantrl 714 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏𝐾)
17943, 24crngcom 19982 . . . . . . . . . 10 ((𝑆 ∈ CRing ∧ (𝑁 𝐿) ∈ 𝐾𝑏𝐾) → ((𝑁 𝐿) · 𝑏) = (𝑏 · (𝑁 𝐿)))
180158, 175, 178, 179syl3anc 1371 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 𝐿) · 𝑏) = (𝑏 · (𝑁 𝐿)))
181180oveq1d 7372 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = ((𝑏 · (𝑁 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
182158crngringd 19977 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ Ring)
183 eqid 2736 . . . . . . . . . . 11 (1r𝑆) = (1r𝑆)
18428, 183ringidval 19915 . . . . . . . . . 10 (1r𝑆) = (0g‘(mulGrp‘𝑆))
18528crngmgp 19972 . . . . . . . . . . . 12 (𝑆 ∈ CRing → (mulGrp‘𝑆) ∈ CMnd)
18618, 185syl 17 . . . . . . . . . . 11 (𝜑 → (mulGrp‘𝑆) ∈ CMnd)
187186adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (mulGrp‘𝑆) ∈ CMnd)
188173ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (mulGrp‘𝑆) ∈ Mnd)
189 elrabi 3639 . . . . . . . . . . . . . . . 16 (𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → 𝑎 ∈ (ℕ0m 𝐼))
190 elmapi 8787 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (ℕ0m 𝐼) → 𝑎:𝐼⟶ℕ0)
191166, 189, 1903syl 18 . . . . . . . . . . . . . . 15 (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} → 𝑎:𝐼⟶ℕ0)
192191adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → 𝑎:𝐼⟶ℕ0)
193192adantrr 715 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎:𝐼⟶ℕ0)
194193ffvelcdmda 7035 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (𝑎𝑣) ∈ ℕ0)
19564ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → 𝐴:𝐼𝐾)
196 simpr 485 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → 𝑣𝐼)
197195, 196ffvelcdmd 7036 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (𝐴𝑣) ∈ 𝐾)
198171, 32, 188, 194, 197mulgnn0cld 18897 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝑎𝑣) (𝐴𝑣)) ∈ 𝐾)
199198fmpttd 7063 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))):𝐼𝐾)
2006psrbagfsupp 21322 . . . . . . . . . . . . . . 15 (𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → 𝑎 finSupp 0)
201200adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → 𝑎 finSupp 0)
202201fsuppimpd 9312 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑎 supp 0) ∈ Fin)
203166, 202sylan2 593 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ∈ Fin)
204203adantrr 715 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ∈ Fin)
205193feqmptd 6910 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 = (𝑣𝐼 ↦ (𝑎𝑣)))
206205oveq1d 7372 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) = ((𝑣𝐼 ↦ (𝑎𝑣)) supp 0))
207 ssidd 3967 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ⊆ (𝑎 supp 0))
208206, 207eqsstrrd 3983 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣𝐼 ↦ (𝑎𝑣)) supp 0) ⊆ (𝑎 supp 0))
209171, 184, 32mulg0 18879 . . . . . . . . . . . . 13 (𝑘𝐾 → (0 𝑘) = (1r𝑆))
210209adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑘𝐾) → (0 𝑘) = (1r𝑆))
211 c0ex 11149 . . . . . . . . . . . . 13 0 ∈ V
212211a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 0 ∈ V)
213208, 210, 194, 197, 212suppssov1 8129 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) supp (1r𝑆)) ⊆ (𝑎 supp 0))
214204, 213ssfid 9211 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) supp (1r𝑆)) ∈ Fin)
215171, 184, 187, 157, 199, 214gsumcl2 19691 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))) ∈ 𝐾)
21643, 24, 182, 175, 178, 215ringassd 40690 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
21743, 24, 182, 178, 175, 215ringassd 40690 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑏 · (𝑁 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = (𝑏 · ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
218181, 216, 2173eqtr3d 2784 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))) = (𝑏 · ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
21948adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 ∈ (𝐾m 𝐼))
22036eleq2d 2823 . . . . . . . . . . . . 13 (𝜑 → (𝑏𝑅𝑏 ∈ (Base‘𝑈)))
221220biimpar 478 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (Base‘𝑈)) → 𝑏𝑅)
222221adantrl 714 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏𝑅)
22342, 4, 10, 43, 44, 16, 157, 158, 159, 222, 219evlsscaval 40734 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘𝐴) = 𝑏))
22442, 4, 10, 44, 43, 28, 32, 3, 92, 6, 134, 157, 158, 159, 219, 167evlsbagval 40736 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))))‘𝐴) = ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
22542, 4, 10, 43, 44, 157, 158, 159, 219, 223, 224, 121, 24evlsmulval 40739 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴) = (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
226225simprd 496 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴) = (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
227226oveq2d 7373 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴)) = ((𝑁 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
22842, 4, 10, 43, 44, 16, 157, 158, 159, 222, 160evlsscaval 40734 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏))
229228simprd 496 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏)
230 fconst6g 6731 . . . . . . . . . . . . . . . . 17 (𝐿𝑅 → (𝐼 × {𝐿}):𝐼𝑅)
23131, 230syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐼 × {𝐿}):𝐼𝑅)
232231ffnd 6669 . . . . . . . . . . . . . . 15 (𝜑 → (𝐼 × {𝐿}) Fn 𝐼)
233232adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 × {𝐿}) Fn 𝐼)
23464ffnd 6669 . . . . . . . . . . . . . . 15 (𝜑𝐴 Fn 𝐼)
235234adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 Fn 𝐼)
23631ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → 𝐿𝑅)
237 fvconst2g 7151 . . . . . . . . . . . . . . 15 ((𝐿𝑅𝑣𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿)
238236, 196, 237syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿)
239 eqidd 2737 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (𝐴𝑣) = (𝐴𝑣))
240233, 235, 157, 157, 65, 238, 239ofval 7628 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣) = (𝐿 · (𝐴𝑣)))
241240oveq2d 7373 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = ((𝑎𝑣) (𝐿 · (𝐴𝑣))))
242186ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (mulGrp‘𝑆) ∈ CMnd)
24360ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → 𝐿𝐾)
24428, 24mgpplusg 19900 . . . . . . . . . . . . . 14 · = (+g‘(mulGrp‘𝑆))
245171, 32, 244mulgnn0di 19604 . . . . . . . . . . . . 13 (((mulGrp‘𝑆) ∈ CMnd ∧ ((𝑎𝑣) ∈ ℕ0𝐿𝐾 ∧ (𝐴𝑣) ∈ 𝐾)) → ((𝑎𝑣) (𝐿 · (𝐴𝑣))) = (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))
246242, 194, 243, 197, 245syl13anc 1372 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝑎𝑣) (𝐿 · (𝐴𝑣))) = (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))
247241, 246eqtrd 2776 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))
248247mpteq2dva 5205 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))) = (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣)))))
249248oveq2d 7373 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))))
250186adantr 481 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (mulGrp‘𝑆) ∈ CMnd)
2518adantr 481 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → 𝐼𝑉)
252173ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → (mulGrp‘𝑆) ∈ Mnd)
253192ffvelcdmda 7035 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → (𝑎𝑣) ∈ ℕ0)
25460ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → 𝐿𝐾)
255171, 32, 252, 253, 254mulgnn0cld 18897 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → ((𝑎𝑣) 𝐿) ∈ 𝐾)
25664ffvelcdmda 7035 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐼) → (𝐴𝑣) ∈ 𝐾)
257256adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → (𝐴𝑣) ∈ 𝐾)
258171, 32, 252, 253, 257mulgnn0cld 18897 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → ((𝑎𝑣) (𝐴𝑣)) ∈ 𝐾)
259 eqidd 2737 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) = (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)))
260 eqidd 2737 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) = (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))
261251mptexd 7174 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) ∈ V)
262 fvexd 6857 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (1r𝑆) ∈ V)
263 funmpt 6539 . . . . . . . . . . . . . 14 Fun (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿))
264263a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → Fun (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)))
265192feqmptd 6910 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → 𝑎 = (𝑣𝐼 ↦ (𝑎𝑣)))
266265oveq1d 7372 . . . . . . . . . . . . . . . 16 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) = ((𝑣𝐼 ↦ (𝑎𝑣)) supp 0))
267 ssidd 3967 . . . . . . . . . . . . . . . 16 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ⊆ (𝑎 supp 0))
268266, 267eqsstrrd 3983 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ (𝑎𝑣)) supp 0) ⊆ (𝑎 supp 0))
269209adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑘𝐾) → (0 𝑘) = (1r𝑆))
270211a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → 0 ∈ V)
271268, 269, 253, 254, 270suppssov1 8129 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) supp (1r𝑆)) ⊆ (𝑎 supp 0))
272203, 271ssfid 9211 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) supp (1r𝑆)) ∈ Fin)
273261, 262, 264, 272isfsuppd 40665 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) finSupp (1r𝑆))
274251mptexd 7174 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) ∈ V)
275 funmpt 6539 . . . . . . . . . . . . . 14 Fun (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))
276275a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → Fun (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))
277268, 269, 253, 257, 270suppssov1 8129 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) supp (1r𝑆)) ⊆ (𝑎 supp 0))
278203, 277ssfid 9211 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) supp (1r𝑆)) ∈ Fin)
279274, 262, 276, 278isfsuppd 40665 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) finSupp (1r𝑆))
280171, 184, 244, 250, 251, 255, 258, 259, 260, 273, 279gsummptfsadd 19701 . . . . . . . . . . 11 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))) = (((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿))) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
2816, 7, 171, 32, 8, 173, 60, 14mhphflem 40756 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿))) = (𝑁 𝐿))
282281oveq1d 7372 . . . . . . . . . . 11 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿))) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
283280, 282eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
284283adantrr 715 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
285249, 284eqtrd 2776 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
286229, 285oveq12d 7375 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = (𝑏 · ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
287218, 227, 2863eqtr4rd 2787 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴)))
288170, 287eqtrd 2776 . . . . 5 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴)))
289 ovex 7390 . . . . . 6 (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) ∈ V
290 fveq2 6842 . . . . . . . 8 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → (𝑄𝑓) = (𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))))))
291290fveq1d 6844 . . . . . . 7 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
292290fveq1d 6844 . . . . . . . 8 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → ((𝑄𝑓)‘𝐴) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴))
293292oveq2d 7373 . . . . . . 7 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴)))
294291, 293eqeq12d 2752 . . . . . 6 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴))))
295289, 294elab 3630 . . . . 5 ((((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴)))
296288, 295sylibr 233 . . . 4 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
297156, 296eqeltrrd 2839 . . 3 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g𝑈))) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
298 elin 3926 . . . . . 6 (𝑥 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}))
299 vex 3449 . . . . . . . 8 𝑥 ∈ V
300 fveq2 6842 . . . . . . . . . 10 (𝑓 = 𝑥 → (𝑄𝑓) = (𝑄𝑥))
301300fveq1d 6844 . . . . . . . . 9 (𝑓 = 𝑥 → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
302300fveq1d 6844 . . . . . . . . . 10 (𝑓 = 𝑥 → ((𝑄𝑓)‘𝐴) = ((𝑄𝑥)‘𝐴))
303302oveq2d 7373 . . . . . . . . 9 (𝑓 = 𝑥 → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))
304301, 303eqeq12d 2752 . . . . . . . 8 (𝑓 = 𝑥 → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
305299, 304elab 3630 . . . . . . 7 (𝑥 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))
306305anbi2i 623 . . . . . 6 ((𝑥 ∈ (𝐻𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
307298, 306bitri 274 . . . . 5 (𝑥 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
308 elin 3926 . . . . . 6 (𝑦 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}))
309 vex 3449 . . . . . . . 8 𝑦 ∈ V
310 fveq2 6842 . . . . . . . . . 10 (𝑓 = 𝑦 → (𝑄𝑓) = (𝑄𝑦))
311310fveq1d 6844 . . . . . . . . 9 (𝑓 = 𝑦 → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
312310fveq1d 6844 . . . . . . . . . 10 (𝑓 = 𝑦 → ((𝑄𝑓)‘𝐴) = ((𝑄𝑦)‘𝐴))
313312oveq2d 7373 . . . . . . . . 9 (𝑓 = 𝑦 → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))
314311, 313eqeq12d 2752 . . . . . . . 8 (𝑓 = 𝑦 → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
315309, 314elab 3630 . . . . . . 7 (𝑦 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))
316315anbi2i 623 . . . . . 6 ((𝑦 ∈ (𝐻𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
317308, 316bitri 274 . . . . 5 (𝑦 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
318307, 317anbi12i 627 . . . 4 ((𝑥 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})) ↔ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))))
31954adantr 481 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑆 ∈ Ring)
320174adantr 481 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑁 𝐿) ∈ 𝐾)
321 eqid 2736 . . . . . . . . 9 (𝑆s (Base‘(𝑆s 𝐼))) = (𝑆s (Base‘(𝑆s 𝐼)))
322 eqid 2736 . . . . . . . . 9 (Base‘(𝑆s (Base‘(𝑆s 𝐼)))) = (Base‘(𝑆s (Base‘(𝑆s 𝐼))))
32318adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑆 ∈ CRing)
324 fvexd 6857 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (Base‘(𝑆s 𝐼)) ∈ V)
325 eqid 2736 . . . . . . . . . . . . . . 15 (𝑆s (𝐾m 𝐼)) = (𝑆s (𝐾m 𝐼))
32642, 4, 10, 325, 43evlsrhm 21498 . . . . . . . . . . . . . 14 ((𝐼𝑉𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆s (𝐾m 𝐼))))
3278, 18, 9, 326syl3anc 1371 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆s (𝐾m 𝐼))))
328 eqid 2736 . . . . . . . . . . . . . 14 (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(𝑆s (𝐾m 𝐼)))
32944, 328rhmf 20158 . . . . . . . . . . . . 13 (𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆s (𝐾m 𝐼))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆s (𝐾m 𝐼))))
330327, 329syl 17 . . . . . . . . . . . 12 (𝜑𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆s (𝐾m 𝐼))))
331330adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆s (𝐾m 𝐼))))
3328adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝐼𝑉)
33312adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝑈 ∈ Ring)
33414adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝑁 ∈ ℕ0)
335 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝑥 ∈ (𝐻𝑁))
3361, 4, 44, 332, 333, 334, 335mhpmpl 21534 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
337336adantrr 715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
338337adantrr 715 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
339331, 338ffvelcdmd 7036 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑥) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
340 eqid 2736 . . . . . . . . . . . . . . 15 (𝑆s 𝐼) = (𝑆s 𝐼)
341340, 43pwsbas 17369 . . . . . . . . . . . . . 14 ((𝑆 ∈ CRing ∧ 𝐼𝑉) → (𝐾m 𝐼) = (Base‘(𝑆s 𝐼)))
34218, 8, 341syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (𝐾m 𝐼) = (Base‘(𝑆s 𝐼)))
343342oveq2d 7373 . . . . . . . . . . . 12 (𝜑 → (𝑆s (𝐾m 𝐼)) = (𝑆s (Base‘(𝑆s 𝐼))))
344343fveq2d 6846 . . . . . . . . . . 11 (𝜑 → (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(𝑆s (Base‘(𝑆s 𝐼)))))
345344adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(𝑆s (Base‘(𝑆s 𝐼)))))
346339, 345eleqtrd 2840 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑥) ∈ (Base‘(𝑆s (Base‘(𝑆s 𝐼)))))
347321, 43, 322, 323, 324, 346pwselbas 17371 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑥):(Base‘(𝑆s 𝐼))⟶𝐾)
34848, 342eleqtrd 2840 . . . . . . . . 9 (𝜑𝐴 ∈ (Base‘(𝑆s 𝐼)))
349348adantr 481 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐴 ∈ (Base‘(𝑆s 𝐼)))
350347, 349ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄𝑥)‘𝐴) ∈ 𝐾)
3518adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝐼𝑉)
35212adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝑈 ∈ Ring)
35314adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝑁 ∈ ℕ0)
354 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝑦 ∈ (𝐻𝑁))
3551, 4, 44, 351, 352, 353, 354mhpmpl 21534 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
356355adantrr 715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
357356adantrl 714 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
358331, 357ffvelcdmd 7036 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑦) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
359358, 345eleqtrd 2840 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑦) ∈ (Base‘(𝑆s (Base‘(𝑆s 𝐼)))))
360321, 43, 322, 323, 324, 359pwselbas 17371 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑦):(Base‘(𝑆s 𝐼))⟶𝐾)
361360, 349ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄𝑦)‘𝐴) ∈ 𝐾)
362 eqid 2736 . . . . . . . 8 (+g𝑆) = (+g𝑆)
36343, 362, 24ringdi 19987 . . . . . . 7 ((𝑆 ∈ Ring ∧ ((𝑁 𝐿) ∈ 𝐾 ∧ ((𝑄𝑥)‘𝐴) ∈ 𝐾 ∧ ((𝑄𝑦)‘𝐴) ∈ 𝐾)) → ((𝑁 𝐿) · (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴))) = (((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))(+g𝑆)((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
364319, 320, 350, 361, 363syl13anc 1372 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑁 𝐿) · (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴))) = (((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))(+g𝑆)((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
3658adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐼𝑉)
3669adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑅 ∈ (SubRing‘𝑆))
36748adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐴 ∈ (𝐾m 𝐼))
368 eqidd 2737 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) → ((𝑄𝑥)‘𝐴) = ((𝑄𝑥)‘𝐴))
369336, 368anim12dan 619 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑥)‘𝐴) = ((𝑄𝑥)‘𝐴)))
370369adantrr 715 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑥)‘𝐴) = ((𝑄𝑥)‘𝐴)))
371 eqidd 2737 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))) → ((𝑄𝑦)‘𝐴) = ((𝑄𝑦)‘𝐴))
372355, 371anim12dan 619 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑦)‘𝐴) = ((𝑄𝑦)‘𝐴)))
373372adantrl 714 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑦)‘𝐴) = ((𝑄𝑦)‘𝐴)))
37442, 4, 10, 43, 44, 365, 323, 366, 367, 370, 373, 5, 362evlsaddval 40738 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴))))
375374simprd 496 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴)))
376375oveq2d 7373 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)) = ((𝑁 𝐿) · (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴))))
37752a1i 11 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐾 ∈ V)
37857adantlr 713 . . . . . . . . . 10 (((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) ∧ (𝑗𝐾𝑘𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
37962adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝐼 × {𝐿}):𝐼𝐾)
38064adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐴:𝐼𝐾)
381378, 379, 380, 365, 365, 65off 7635 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼𝐾)
382377, 365, 381elmapdd 40664 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾m 𝐼))
383 simpr 485 . . . . . . . . . 10 ((𝜑 ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) → ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))
384336, 383anim12dan 619 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
385384adantrr 715 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
386 simpr 485 . . . . . . . . . 10 ((𝜑 ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))) → ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))
387355, 386anim12dan 619 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
388387adantrl 714 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
38942, 4, 10, 43, 44, 365, 323, 366, 382, 385, 388, 5, 362evlsaddval 40738 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))(+g𝑆)((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))))
390389simprd 496 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))(+g𝑆)((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
391364, 376, 3903eqtr4rd 2787 . . . . 5 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
392 ovex 7390 . . . . . 6 (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ V
393 fveq2 6842 . . . . . . . 8 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (𝑄𝑓) = (𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦)))
394393fveq1d 6844 . . . . . . 7 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
395393fveq1d 6844 . . . . . . . 8 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄𝑓)‘𝐴) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))
396395oveq2d 7373 . . . . . . 7 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
397394, 396eqeq12d 2752 . . . . . 6 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))))
398392, 397elab 3630 . . . . 5 ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
399391, 398sylibr 233 . . . 4 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
400318, 399sylan2b 594 . . 3 ((𝜑 ∧ (𝑥 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
4011, 2, 3, 4, 5, 6, 7, 8, 13, 14, 15, 79, 297, 400mhpind 40755 . 2 (𝜑𝑋 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
402 fveq2 6842 . . . . . 6 (𝑓 = 𝑋 → (𝑄𝑓) = (𝑄𝑋))
403402fveq1d 6844 . . . . 5 (𝑓 = 𝑋 → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
404402fveq1d 6844 . . . . . 6 (𝑓 = 𝑋 → ((𝑄𝑓)‘𝐴) = ((𝑄𝑋)‘𝐴))
405404oveq2d 7373 . . . . 5 (𝑓 = 𝑋 → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴)))
406403, 405eqeq12d 2752 . . . 4 (𝑓 = 𝑋 → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴))))
407406elabg 3628 . . 3 (𝑋 ∈ (𝐻𝑁) → (𝑋 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴))))
40815, 407syl 17 . 2 (𝜑 → (𝑋 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴))))
409401, 408mpbid 231 1 (𝜑 → ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  {cab 2713  {crab 3407  Vcvv 3445  cdif 3907  cin 3909  wss 3910  ifcif 4486  {csn 4586   class class class wbr 5105  cmpt 5188   × cxp 5631  ccnv 5632  cima 5636  Fun wfun 6490   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  f cof 7615   supp csupp 8092  m cmap 8765  Fincfn 8883   finSupp cfsupp 9305  0cc0 11051  cn 12153  0cn0 12413  Basecbs 17083  s cress 17112  +gcplusg 17133  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  0gc0g 17321   Σg cgsu 17322  s cpws 17328  Mndcmnd 18556  SubMndcsubmnd 18600  .gcmg 18872  CMndccmn 19562  mulGrpcmgp 19896  1rcur 19913  Ringcrg 19964  CRingccrg 19965   RingHom crh 20143  SubRingcsubrg 20218  fldccnfld 20796  AssAlgcasa 21256  algSccascl 21258   mPwSer cmps 21306   mPoly cmpl 21308   evalSub ces 21480   mHomP cmhp 21519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-oi 9446  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-pws 17331  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-mhm 18601  df-submnd 18602  df-grp 18751  df-minusg 18752  df-sbg 18753  df-mulg 18873  df-subg 18925  df-ghm 19006  df-cntz 19097  df-cmn 19564  df-abl 19565  df-mgp 19897  df-ur 19914  df-srg 19918  df-ring 19966  df-cring 19967  df-rnghom 20146  df-subrg 20220  df-lmod 20324  df-lss 20393  df-lsp 20433  df-cnfld 20797  df-assa 21259  df-asp 21260  df-ascl 21261  df-psr 21311  df-mvr 21312  df-mpl 21313  df-evls 21482  df-mhp 21523
This theorem is referenced by:  mhphf2  40758  mhphf3  40759
  Copyright terms: Public domain W3C validator