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

Theorem mhphf 39775
 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 2759 . . 3 (Base‘𝑈) = (Base‘𝑈)
3 eqid 2759 . . 3 (0g𝑈) = (0g𝑈)
4 eqid 2759 . . 3 (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈)
5 eqid 2759 . . 3 (+g‘(𝐼 mPoly 𝑈)) = (+g‘(𝐼 mPoly 𝑈))
6 eqid 2759 . . 3 { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
7 eqid 2759 . . 3 {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} = {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}
8 mhphf.i . . 3 (𝜑𝐼𝑉)
9 mhphf.r . . . . 5 (𝜑𝑅 ∈ (SubRing‘𝑆))
10 mhphf.u . . . . . 6 𝑈 = (𝑆s 𝑅)
1110subrgring 19591 . . . . 5 (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring)
129, 11syl 17 . . . 4 (𝜑𝑈 ∈ Ring)
1312ringgrpd 19359 . . 3 (𝜑𝑈 ∈ Grp)
14 mhphf.n . . 3 (𝜑𝑁 ∈ ℕ0)
15 mhphf.x . . 3 (𝜑𝑋 ∈ (𝐻𝑁))
164, 8, 12mplsca 20761 . . . . . . 7 (𝜑𝑈 = (Scalar‘(𝐼 mPoly 𝑈)))
1716fveq2d 6655 . . . . . 6 (𝜑 → (0g𝑈) = (0g‘(Scalar‘(𝐼 mPoly 𝑈))))
1817fveq2d 6655 . . . . 5 (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘(Scalar‘(𝐼 mPoly 𝑈)))))
19 eqid 2759 . . . . . 6 (algSc‘(𝐼 mPoly 𝑈)) = (algSc‘(𝐼 mPoly 𝑈))
20 eqid 2759 . . . . . 6 (Scalar‘(𝐼 mPoly 𝑈)) = (Scalar‘(𝐼 mPoly 𝑈))
214mpllmod 20767 . . . . . . 7 ((𝐼𝑉𝑈 ∈ Ring) → (𝐼 mPoly 𝑈) ∈ LMod)
228, 12, 21syl2anc 588 . . . . . 6 (𝜑 → (𝐼 mPoly 𝑈) ∈ LMod)
234mplring 20768 . . . . . . 7 ((𝐼𝑉𝑈 ∈ Ring) → (𝐼 mPoly 𝑈) ∈ Ring)
248, 12, 23syl2anc 588 . . . . . 6 (𝜑 → (𝐼 mPoly 𝑈) ∈ Ring)
2519, 20, 22, 24ascl0 20631 . . . . 5 (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘(Scalar‘(𝐼 mPoly 𝑈)))) = (0g‘(𝐼 mPoly 𝑈)))
26 eqid 2759 . . . . . 6 (0g‘(𝐼 mPoly 𝑈)) = (0g‘(𝐼 mPoly 𝑈))
274, 6, 3, 26, 8, 13mpl0 20756 . . . . 5 (𝜑 → (0g‘(𝐼 mPoly 𝑈)) = ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {(0g𝑈)}))
2818, 25, 273eqtrrd 2799 . . . 4 (𝜑 → ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {(0g𝑈)}) = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))
29 mhphf.m . . . . . . . . . 10 · = (.r𝑆)
3010, 29ressmulr 16668 . . . . . . . . 9 (𝑅 ∈ (SubRing‘𝑆) → · = (.r𝑈))
319, 30syl 17 . . . . . . . 8 (𝜑· = (.r𝑈))
3231oveqd 7160 . . . . . . 7 (𝜑 → ((𝑁 𝐿) · (0g𝑈)) = ((𝑁 𝐿)(.r𝑈)(0g𝑈)))
33 eqid 2759 . . . . . . . . . . . 12 (mulGrp‘𝑆) = (mulGrp‘𝑆)
3433subrgsubm 19601 . . . . . . . . . . 11 (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)))
359, 34syl 17 . . . . . . . . . 10 (𝜑𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)))
36 mhphf.l . . . . . . . . . 10 (𝜑𝐿𝑅)
37 mhphf.e . . . . . . . . . . 11 = (.g‘(mulGrp‘𝑆))
3837submmulgcl 18322 . . . . . . . . . 10 ((𝑅 ∈ (SubMnd‘(mulGrp‘𝑆)) ∧ 𝑁 ∈ ℕ0𝐿𝑅) → (𝑁 𝐿) ∈ 𝑅)
3935, 14, 36, 38syl3anc 1369 . . . . . . . . 9 (𝜑 → (𝑁 𝐿) ∈ 𝑅)
4010subrgbas 19597 . . . . . . . . . 10 (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈))
419, 40syl 17 . . . . . . . . 9 (𝜑𝑅 = (Base‘𝑈))
4239, 41eleqtrd 2853 . . . . . . . 8 (𝜑 → (𝑁 𝐿) ∈ (Base‘𝑈))
43 eqid 2759 . . . . . . . . 9 (.r𝑈) = (.r𝑈)
442, 43, 3ringrz 19394 . . . . . . . 8 ((𝑈 ∈ Ring ∧ (𝑁 𝐿) ∈ (Base‘𝑈)) → ((𝑁 𝐿)(.r𝑈)(0g𝑈)) = (0g𝑈))
4512, 42, 44syl2anc 588 . . . . . . 7 (𝜑 → ((𝑁 𝐿)(.r𝑈)(0g𝑈)) = (0g𝑈))
4632, 45eqtrd 2794 . . . . . 6 (𝜑 → ((𝑁 𝐿) · (0g𝑈)) = (0g𝑈))
47 mhphf.q . . . . . . . . 9 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
48 mhphf.k . . . . . . . . 9 𝐾 = (Base‘𝑆)
49 eqid 2759 . . . . . . . . 9 (Base‘(𝐼 mPoly 𝑈)) = (Base‘(𝐼 mPoly 𝑈))
50 mhphf.s . . . . . . . . 9 (𝜑𝑆 ∈ CRing)
512, 3ring0cl 19375 . . . . . . . . . . 11 (𝑈 ∈ Ring → (0g𝑈) ∈ (Base‘𝑈))
5212, 51syl 17 . . . . . . . . . 10 (𝜑 → (0g𝑈) ∈ (Base‘𝑈))
5352, 41eleqtrrd 2854 . . . . . . . . 9 (𝜑 → (0g𝑈) ∈ 𝑅)
54 mhphf.a . . . . . . . . 9 (𝜑𝐴 ∈ (𝐾m 𝐼))
5547, 4, 10, 48, 49, 19, 8, 50, 9, 53, 54evlsscaval 39763 . . . . . . . 8 (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴) = (0g𝑈)))
5655simprd 500 . . . . . . 7 (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴) = (0g𝑈))
5756oveq2d 7159 . . . . . 6 (𝜑 → ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴)) = ((𝑁 𝐿) · (0g𝑈)))
5848fvexi 6665 . . . . . . . . . 10 𝐾 ∈ V
5958a1i 11 . . . . . . . . 9 (𝜑𝐾 ∈ V)
6050crngringd 19363 . . . . . . . . . . . 12 (𝜑𝑆 ∈ Ring)
6148, 29ringcl 19367 . . . . . . . . . . . 12 ((𝑆 ∈ Ring ∧ 𝑗𝐾𝑘𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
6260, 61syl3an1 1161 . . . . . . . . . . 11 ((𝜑𝑗𝐾𝑘𝐾) → (𝑗 · 𝑘) ∈ 𝐾)
63623expb 1118 . . . . . . . . . 10 ((𝜑 ∧ (𝑗𝐾𝑘𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
6448subrgss 19589 . . . . . . . . . . . . 13 (𝑅 ∈ (SubRing‘𝑆) → 𝑅𝐾)
659, 64syl 17 . . . . . . . . . . . 12 (𝜑𝑅𝐾)
6665, 36sseldd 3889 . . . . . . . . . . 11 (𝜑𝐿𝐾)
67 fconst6g 6546 . . . . . . . . . . 11 (𝐿𝐾 → (𝐼 × {𝐿}):𝐼𝐾)
6866, 67syl 17 . . . . . . . . . 10 (𝜑 → (𝐼 × {𝐿}):𝐼𝐾)
69 elmapi 8431 . . . . . . . . . . 11 (𝐴 ∈ (𝐾m 𝐼) → 𝐴:𝐼𝐾)
7054, 69syl 17 . . . . . . . . . 10 (𝜑𝐴:𝐼𝐾)
71 inidm 4119 . . . . . . . . . 10 (𝐼𝐼) = 𝐼
7263, 68, 70, 8, 8, 71off 7415 . . . . . . . . 9 (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼𝐾)
7359, 8, 72elmapdd 39707 . . . . . . . 8 (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾m 𝐼))
7447, 4, 10, 48, 49, 19, 8, 50, 9, 53, 73evlsscaval 39763 . . . . . . 7 (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (0g𝑈)))
7574simprd 500 . . . . . 6 (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (0g𝑈))
7646, 57, 753eqtr4rd 2805 . . . . 5 (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴)))
77 fvex 6664 . . . . . 6 ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ V
78 fveq2 6651 . . . . . . . 8 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → (𝑄𝑓) = (𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈))))
7978fveq1d 6653 . . . . . . 7 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
8078fveq1d 6653 . . . . . . . 8 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → ((𝑄𝑓)‘𝐴) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴))
8180oveq2d 7159 . . . . . . 7 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴)))
8279, 81eqeq12d 2775 . . . . . 6 (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴))))
8377, 82elab 3586 . . . . 5 (((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)))‘𝐴)))
8476, 83sylibr 237 . . . 4 (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g𝑈)) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
8528, 84eqeltrd 2851 . . 3 (𝜑 → ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {(0g𝑈)}) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
8610subrgcrng 19592 . . . . . . . . . 10 ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing)
8750, 9, 86syl2anc 588 . . . . . . . . 9 (𝜑𝑈 ∈ CRing)
884mplassa 20771 . . . . . . . . 9 ((𝐼𝑉𝑈 ∈ CRing) → (𝐼 mPoly 𝑈) ∈ AssAlg)
898, 87, 88syl2anc 588 . . . . . . . 8 (𝜑 → (𝐼 mPoly 𝑈) ∈ AssAlg)
9089adantr 485 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 mPoly 𝑈) ∈ AssAlg)
9116fveq2d 6655 . . . . . . . . . 10 (𝜑 → (Base‘𝑈) = (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
9291eleq2d 2836 . . . . . . . . 9 (𝜑 → (𝑏 ∈ (Base‘𝑈) ↔ 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈)))))
9392biimpa 481 . . . . . . . 8 ((𝜑𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
9493adantrl 716 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))
95 fvexd 6666 . . . . . . . . . . 11 (𝜑 → (Base‘𝑈) ∈ V)
96 ovex 7176 . . . . . . . . . . . . 13 (ℕ0m 𝐼) ∈ V
9796rabex 5195 . . . . . . . . . . . 12 { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∈ V
9897a1i 11 . . . . . . . . . . 11 (𝜑 → { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∈ V)
99 eqid 2759 . . . . . . . . . . . . . . . 16 (1r𝑈) = (1r𝑈)
1002, 99ringidcl 19374 . . . . . . . . . . . . . . 15 (𝑈 ∈ Ring → (1r𝑈) ∈ (Base‘𝑈))
10112, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (1r𝑈) ∈ (Base‘𝑈))
102101, 52ifcld 4459 . . . . . . . . . . . . 13 (𝜑 → if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) ∈ (Base‘𝑈))
103102adantr 485 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) ∈ (Base‘𝑈))
104103fmpttd 6863 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))):{ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}⟶(Base‘𝑈))
10595, 98, 104elmapdd 39707 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ ((Base‘𝑈) ↑m { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}))
106 eqid 2759 . . . . . . . . . . 11 (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈)
107 eqid 2759 . . . . . . . . . . 11 (Base‘(𝐼 mPwSer 𝑈)) = (Base‘(𝐼 mPwSer 𝑈))
108106, 2, 6, 107, 8psrbas 20691 . . . . . . . . . 10 (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑m { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}))
109105, 108eleqtrrd 2854 . . . . . . . . 9 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈)))
11097mptex 6970 . . . . . . . . . . 11 (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ V
111110a1i 11 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ V)
112 fvexd 6666 . . . . . . . . . 10 (𝜑 → (0g𝑈) ∈ V)
113 funmpt 6366 . . . . . . . . . . 11 Fun (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))
114113a1i 11 . . . . . . . . . 10 (𝜑 → Fun (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))))
115 snfi 8607 . . . . . . . . . . . 12 {𝑎} ∈ Fin
116115a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑎} ∈ Fin)
117 eldifsnneq 4674 . . . . . . . . . . . . . 14 (𝑤 ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑎}) → ¬ 𝑤 = 𝑎)
118117adantl 486 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑎})) → ¬ 𝑤 = 𝑎)
119118iffalsed 4424 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∖ {𝑎})) → if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) = (0g𝑈))
120119, 98suppss2 7867 . . . . . . . . . . 11 (𝜑 → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) supp (0g𝑈)) ⊆ {𝑎})
121116, 120ssfid 8755 . . . . . . . . . 10 (𝜑 → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) supp (0g𝑈)) ∈ Fin)
122111, 112, 114, 121isfsuppd 39708 . . . . . . . . 9 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) finSupp (0g𝑈))
1234, 106, 107, 3, 49mplelbas 20743 . . . . . . . . 9 ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ↔ ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈)) ∧ (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) finSupp (0g𝑈)))
124109, 122, 123sylanbrc 587 . . . . . . . 8 (𝜑 → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)))
125124adantr 485 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)))
126 eqid 2759 . . . . . . . 8 (Base‘(Scalar‘(𝐼 mPoly 𝑈))) = (Base‘(Scalar‘(𝐼 mPoly 𝑈)))
127 eqid 2759 . . . . . . . 8 (.r‘(𝐼 mPoly 𝑈)) = (.r‘(𝐼 mPoly 𝑈))
128 eqid 2759 . . . . . . . 8 ( ·𝑠 ‘(𝐼 mPoly 𝑈)) = ( ·𝑠 ‘(𝐼 mPoly 𝑈))
12919, 20, 126, 49, 127, 128asclmul1 20633 . . . . . . 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𝑈)))))
13090, 94, 125, 129syl3anc 1369 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑏( ·𝑠 ‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))
131 simprr 773 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘𝑈))
1324, 128, 2, 49, 43, 6, 131, 125mplvsca 20763 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑏( ·𝑠 ‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r𝑈)(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))
133130, 132eqtrd 2794 . . . . 5 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r𝑈)(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))
134 vex 3411 . . . . . . 7 𝑏 ∈ V
135 fnconstg 6545 . . . . . . 7 (𝑏 ∈ V → ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) Fn { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
136134, 135mp1i 13 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) Fn { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
137 fvex 6664 . . . . . . . . 9 (1r𝑈) ∈ V
138 fvex 6664 . . . . . . . . 9 (0g𝑈) ∈ V
139137, 138ifex 4463 . . . . . . . 8 if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) ∈ V
140 eqid 2759 . . . . . . . 8 (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) = (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))
141139, 140fnmpti 6467 . . . . . . 7 (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) Fn { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
142141a1i 11 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) Fn { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
14397a1i 11 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∈ V)
144 inidm 4119 . . . . . 6 ({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∩ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
145134fvconst2 6950 . . . . . . 7 (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏})‘𝑠) = 𝑏)
146145adantl 486 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏})‘𝑠) = 𝑏)
147 equequ1 2033 . . . . . . . . 9 (𝑤 = 𝑠 → (𝑤 = 𝑎𝑠 = 𝑎))
148147ifbid 4436 . . . . . . . 8 (𝑤 = 𝑠 → if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)) = if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))
149137, 138ifex 4463 . . . . . . . 8 if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)) ∈ V
150148, 140, 149fvmpt 6752 . . . . . . 7 (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))‘𝑠) = if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))
151150adantl 486 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))‘𝑠) = if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))
152136, 142, 143, 143, 144, 146, 151offval 7406 . . . . 5 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (({ ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} × {𝑏}) ∘f (.r𝑈)(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ (𝑏(.r𝑈)if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))))
153 ovif2 7239 . . . . . . 7 (𝑏(.r𝑈)if(𝑠 = 𝑎, (1r𝑈), (0g𝑈))) = if(𝑠 = 𝑎, (𝑏(.r𝑈)(1r𝑈)), (𝑏(.r𝑈)(0g𝑈)))
15412ad2antrr 726 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → 𝑈 ∈ Ring)
155 simplrr 778 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → 𝑏 ∈ (Base‘𝑈))
1562, 43, 99ringridm 19378 . . . . . . . . 9 ((𝑈 ∈ Ring ∧ 𝑏 ∈ (Base‘𝑈)) → (𝑏(.r𝑈)(1r𝑈)) = 𝑏)
157154, 155, 156syl2anc 588 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑏(.r𝑈)(1r𝑈)) = 𝑏)
1582, 43, 3ringrz 19394 . . . . . . . . 9 ((𝑈 ∈ Ring ∧ 𝑏 ∈ (Base‘𝑈)) → (𝑏(.r𝑈)(0g𝑈)) = (0g𝑈))
159154, 155, 158syl2anc 588 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑏(.r𝑈)(0g𝑈)) = (0g𝑈))
160157, 159ifeq12d 4434 . . . . . . 7 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → if(𝑠 = 𝑎, (𝑏(.r𝑈)(1r𝑈)), (𝑏(.r𝑈)(0g𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g𝑈)))
161153, 160syl5eq 2806 . . . . . 6 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑏(.r𝑈)if(𝑠 = 𝑎, (1r𝑈), (0g𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g𝑈)))
162161mpteq2dva 5120 . . . . 5 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ (𝑏(.r𝑈)if(𝑠 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g𝑈))))
163133, 152, 1623eqtrd 2798 . . . 4 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) = (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g𝑈))))
1648adantr 485 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐼𝑉)
16550adantr 485 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ CRing)
1669adantr 485 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑅 ∈ (SubRing‘𝑆))
16773adantr 485 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾m 𝐼))
16812adantr 485 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑈 ∈ Ring)
1694, 49, 2, 19, 164, 168mplasclf 20811 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (algSc‘(𝐼 mPoly 𝑈)):(Base‘𝑈)⟶(Base‘(𝐼 mPoly 𝑈)))
170169, 131ffvelrnd 6836 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)))
171 eqidd 2760 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
172170, 171jca 516 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴))))
173 elrabi 3594 . . . . . . . . . 10 (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} → 𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
174173ad2antrl 728 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
17547, 4, 10, 49, 48, 33, 37, 3, 99, 6, 140, 164, 165, 166, 167, 174evlsbagval 39765 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))))
17647, 4, 10, 48, 49, 164, 165, 166, 167, 172, 175, 127, 29evlsmulval 39768 . . . . . . 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 · 𝐴)‘𝑣)))))))
177176simprd 500 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))))
17833ringmgp 19356 . . . . . . . . . . . . 13 (𝑆 ∈ Ring → (mulGrp‘𝑆) ∈ Mnd)
17960, 178syl 17 . . . . . . . . . . . 12 (𝜑 → (mulGrp‘𝑆) ∈ Mnd)
18033, 48mgpbas 19298 . . . . . . . . . . . . 13 𝐾 = (Base‘(mulGrp‘𝑆))
181180, 37mulgnn0cl 18296 . . . . . . . . . . . 12 (((mulGrp‘𝑆) ∈ Mnd ∧ 𝑁 ∈ ℕ0𝐿𝐾) → (𝑁 𝐿) ∈ 𝐾)
182179, 14, 66, 181syl3anc 1369 . . . . . . . . . . 11 (𝜑 → (𝑁 𝐿) ∈ 𝐾)
183182adantr 485 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑁 𝐿) ∈ 𝐾)
18441, 65eqsstrrd 3927 . . . . . . . . . . . 12 (𝜑 → (Base‘𝑈) ⊆ 𝐾)
185184sselda 3888 . . . . . . . . . . 11 ((𝜑𝑏 ∈ (Base‘𝑈)) → 𝑏𝐾)
186185adantrl 716 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏𝐾)
18748, 29crngcom 19368 . . . . . . . . . 10 ((𝑆 ∈ CRing ∧ (𝑁 𝐿) ∈ 𝐾𝑏𝐾) → ((𝑁 𝐿) · 𝑏) = (𝑏 · (𝑁 𝐿)))
188165, 183, 186, 187syl3anc 1369 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 𝐿) · 𝑏) = (𝑏 · (𝑁 𝐿)))
189188oveq1d 7158 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = ((𝑏 · (𝑁 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
190165crngringd 19363 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ Ring)
191 eqid 2759 . . . . . . . . . . 11 (1r𝑆) = (1r𝑆)
19233, 191ringidval 19306 . . . . . . . . . 10 (1r𝑆) = (0g‘(mulGrp‘𝑆))
19333crngmgp 19358 . . . . . . . . . . . 12 (𝑆 ∈ CRing → (mulGrp‘𝑆) ∈ CMnd)
19450, 193syl 17 . . . . . . . . . . 11 (𝜑 → (mulGrp‘𝑆) ∈ CMnd)
195194adantr 485 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (mulGrp‘𝑆) ∈ CMnd)
196179ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (mulGrp‘𝑆) ∈ Mnd)
197 elrabi 3594 . . . . . . . . . . . . . . . 16 (𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → 𝑎 ∈ (ℕ0m 𝐼))
198 elmapi 8431 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (ℕ0m 𝐼) → 𝑎:𝐼⟶ℕ0)
199173, 197, 1983syl 18 . . . . . . . . . . . . . . 15 (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} → 𝑎:𝐼⟶ℕ0)
200199adantl 486 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → 𝑎:𝐼⟶ℕ0)
201200adantrr 717 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎:𝐼⟶ℕ0)
202201ffvelrnda 6835 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (𝑎𝑣) ∈ ℕ0)
20370ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → 𝐴:𝐼𝐾)
204 simpr 489 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → 𝑣𝐼)
205203, 204ffvelrnd 6836 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (𝐴𝑣) ∈ 𝐾)
206180, 37mulgnn0cl 18296 . . . . . . . . . . . 12 (((mulGrp‘𝑆) ∈ Mnd ∧ (𝑎𝑣) ∈ ℕ0 ∧ (𝐴𝑣) ∈ 𝐾) → ((𝑎𝑣) (𝐴𝑣)) ∈ 𝐾)
207196, 202, 205, 206syl3anc 1369 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝑎𝑣) (𝐴𝑣)) ∈ 𝐾)
208207fmpttd 6863 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))):𝐼𝐾)
2096psrbagfsupp 20667 . . . . . . . . . . . . . . 15 (𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} → 𝑎 finSupp 0)
210209adantl 486 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → 𝑎 finSupp 0)
211210fsuppimpd 8858 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}) → (𝑎 supp 0) ∈ Fin)
212173, 211sylan2 596 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ∈ Fin)
213212adantrr 717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ∈ Fin)
214201feqmptd 6714 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 = (𝑣𝐼 ↦ (𝑎𝑣)))
215214oveq1d 7158 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) = ((𝑣𝐼 ↦ (𝑎𝑣)) supp 0))
216 ssidd 3911 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ⊆ (𝑎 supp 0))
217215, 216eqsstrrd 3927 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣𝐼 ↦ (𝑎𝑣)) supp 0) ⊆ (𝑎 supp 0))
218180, 192, 37mulg0 18283 . . . . . . . . . . . . 13 (𝑘𝐾 → (0 𝑘) = (1r𝑆))
219218adantl 486 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑘𝐾) → (0 𝑘) = (1r𝑆))
220 c0ex 10658 . . . . . . . . . . . . 13 0 ∈ V
221220a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 0 ∈ V)
222217, 219, 202, 205, 221suppssov1 7865 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) supp (1r𝑆)) ⊆ (𝑎 supp 0))
223213, 222ssfid 8755 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) supp (1r𝑆)) ∈ Fin)
224180, 192, 195, 164, 208, 223gsumcl2 19087 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))) ∈ 𝐾)
22548, 29ringass 19370 . . . . . . . . 9 ((𝑆 ∈ Ring ∧ ((𝑁 𝐿) ∈ 𝐾𝑏𝐾 ∧ ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))) ∈ 𝐾)) → (((𝑁 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
226190, 183, 186, 224, 225syl13anc 1370 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 𝐿) · 𝑏) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
22748, 29ringass 19370 . . . . . . . . 9 ((𝑆 ∈ Ring ∧ (𝑏𝐾 ∧ (𝑁 𝐿) ∈ 𝐾 ∧ ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))) ∈ 𝐾)) → ((𝑏 · (𝑁 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = (𝑏 · ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
228190, 186, 183, 224, 227syl13anc 1370 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑏 · (𝑁 𝐿)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = (𝑏 · ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
229189, 226, 2283eqtr3d 2802 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))) = (𝑏 · ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
23054adantr 485 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 ∈ (𝐾m 𝐼))
23141eleq2d 2836 . . . . . . . . . . . . 13 (𝜑 → (𝑏𝑅𝑏 ∈ (Base‘𝑈)))
232231biimpar 482 . . . . . . . . . . . 12 ((𝜑𝑏 ∈ (Base‘𝑈)) → 𝑏𝑅)
233232adantrl 716 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏𝑅)
23447, 4, 10, 48, 49, 19, 164, 165, 166, 233, 230evlsscaval 39763 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘𝐴) = 𝑏))
23547, 4, 10, 49, 48, 33, 37, 3, 99, 6, 140, 164, 165, 166, 230, 174evlsbagval 39765 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))))‘𝐴) = ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
23647, 4, 10, 48, 49, 164, 165, 166, 230, 234, 235, 127, 29evlsmulval 39768 . . . . . . . . 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 (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
237236simprd 500 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴) = (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
238237oveq2d 7159 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴)) = ((𝑁 𝐿) · (𝑏 · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
23947, 4, 10, 48, 49, 19, 164, 165, 166, 233, 167evlsscaval 39763 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏))
240239simprd 500 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏)
241 fconst6g 6546 . . . . . . . . . . . . . . . . 17 (𝐿𝑅 → (𝐼 × {𝐿}):𝐼𝑅)
24236, 241syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐼 × {𝐿}):𝐼𝑅)
243242ffnd 6492 . . . . . . . . . . . . . . 15 (𝜑 → (𝐼 × {𝐿}) Fn 𝐼)
244243adantr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 × {𝐿}) Fn 𝐼)
24570ffnd 6492 . . . . . . . . . . . . . . 15 (𝜑𝐴 Fn 𝐼)
246245adantr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 Fn 𝐼)
24736ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → 𝐿𝑅)
248 fvconst2g 6948 . . . . . . . . . . . . . . 15 ((𝐿𝑅𝑣𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿)
249247, 204, 248syl2anc 588 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿)
250 eqidd 2760 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (𝐴𝑣) = (𝐴𝑣))
251244, 246, 164, 164, 71, 249, 250ofval 7408 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣) = (𝐿 · (𝐴𝑣)))
252251oveq2d 7159 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = ((𝑎𝑣) (𝐿 · (𝐴𝑣))))
253194ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → (mulGrp‘𝑆) ∈ CMnd)
25466ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → 𝐿𝐾)
25533, 29mgpplusg 19296 . . . . . . . . . . . . . 14 · = (+g‘(mulGrp‘𝑆))
256180, 37, 255mulgnn0di 18999 . . . . . . . . . . . . 13 (((mulGrp‘𝑆) ∈ CMnd ∧ ((𝑎𝑣) ∈ ℕ0𝐿𝐾 ∧ (𝐴𝑣) ∈ 𝐾)) → ((𝑎𝑣) (𝐿 · (𝐴𝑣))) = (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))
257253, 202, 254, 205, 256syl13anc 1370 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝑎𝑣) (𝐿 · (𝐴𝑣))) = (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))
258252, 257eqtrd 2794 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣𝐼) → ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))
259258mpteq2dva 5120 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))) = (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣)))))
260259oveq2d 7159 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))))
261194adantr 485 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (mulGrp‘𝑆) ∈ CMnd)
2628adantr 485 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → 𝐼𝑉)
263179ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → (mulGrp‘𝑆) ∈ Mnd)
264200ffvelrnda 6835 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → (𝑎𝑣) ∈ ℕ0)
26566ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → 𝐿𝐾)
266180, 37mulgnn0cl 18296 . . . . . . . . . . . . 13 (((mulGrp‘𝑆) ∈ Mnd ∧ (𝑎𝑣) ∈ ℕ0𝐿𝐾) → ((𝑎𝑣) 𝐿) ∈ 𝐾)
267263, 264, 265, 266syl3anc 1369 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → ((𝑎𝑣) 𝐿) ∈ 𝐾)
26870ffvelrnda 6835 . . . . . . . . . . . . . 14 ((𝜑𝑣𝐼) → (𝐴𝑣) ∈ 𝐾)
269268adantlr 715 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → (𝐴𝑣) ∈ 𝐾)
270263, 264, 269, 206syl3anc 1369 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑣𝐼) → ((𝑎𝑣) (𝐴𝑣)) ∈ 𝐾)
271 eqidd 2760 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) = (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)))
272 eqidd 2760 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) = (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))
273262mptexd 6971 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) ∈ V)
274 fvexd 6666 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (1r𝑆) ∈ V)
275 funmpt 6366 . . . . . . . . . . . . . 14 Fun (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿))
276275a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → Fun (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)))
277200feqmptd 6714 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → 𝑎 = (𝑣𝐼 ↦ (𝑎𝑣)))
278277oveq1d 7158 . . . . . . . . . . . . . . . 16 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) = ((𝑣𝐼 ↦ (𝑎𝑣)) supp 0))
279 ssidd 3911 . . . . . . . . . . . . . . . 16 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ⊆ (𝑎 supp 0))
280278, 279eqsstrrd 3927 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ (𝑎𝑣)) supp 0) ⊆ (𝑎 supp 0))
281218adantl 486 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) ∧ 𝑘𝐾) → (0 𝑘) = (1r𝑆))
282220a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → 0 ∈ V)
283280, 281, 264, 265, 282suppssov1 7865 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) supp (1r𝑆)) ⊆ (𝑎 supp 0))
284212, 283ssfid 8755 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) supp (1r𝑆)) ∈ Fin)
285273, 274, 276, 284isfsuppd 39708 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿)) finSupp (1r𝑆))
286262mptexd 6971 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) ∈ V)
287 funmpt 6366 . . . . . . . . . . . . . 14 Fun (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))
288287a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → Fun (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))
289280, 281, 264, 269, 282suppssov1 7865 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) supp (1r𝑆)) ⊆ (𝑎 supp 0))
290212, 289ssfid 8755 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) supp (1r𝑆)) ∈ Fin)
291286, 274, 288, 290isfsuppd 39708 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))) finSupp (1r𝑆))
292180, 192, 255, 261, 262, 267, 270, 271, 272, 285, 291gsummptfsadd 19097 . . . . . . . . . . 11 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))) = (((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿))) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
2936, 7, 180, 37, 8, 179, 66, 14mhphflem 39774 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿))) = (𝑁 𝐿))
294293oveq1d 7158 . . . . . . . . . . 11 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → (((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) 𝐿))) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
295292, 294eqtrd 2794 . . . . . . . . . 10 ((𝜑𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
296295adantrr 717 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ (((𝑎𝑣) 𝐿) · ((𝑎𝑣) (𝐴𝑣))))) = ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
297260, 296eqtrd 2794 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣))))))
298240, 297oveq12d 7161 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = (𝑏 · ((𝑁 𝐿) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (𝐴𝑣)))))))
299229, 238, 2983eqtr4rd 2805 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) · ((mulGrp‘𝑆) Σg (𝑣𝐼 ↦ ((𝑎𝑣) (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴)))
300177, 299eqtrd 2794 . . . . 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𝑈)))))‘𝐴)))
301 ovex 7176 . . . . . 6 (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) ∈ V
302 fveq2 6651 . . . . . . . 8 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → (𝑄𝑓) = (𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈))))))
303302fveq1d 6653 . . . . . . 7 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
304302fveq1d 6653 . . . . . . . 8 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → ((𝑄𝑓)‘𝐴) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴))
305304oveq2d 7159 . . . . . . 7 (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))))‘𝐴)))
306303, 305eqeq12d 2775 . . . . . 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𝑈)))))‘𝐴))))
307301, 306elab 3586 . . . . 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𝑈)))))‘𝐴)))
308300, 307sylibr 237 . . . 4 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r𝑈), (0g𝑈)))) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
309163, 308eqeltrrd 2852 . . 3 ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ∣ ((ℂflds0) Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g𝑈))) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
310 elin 3870 . . . . . 6 (𝑥 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}))
311 vex 3411 . . . . . . . 8 𝑥 ∈ V
312 fveq2 6651 . . . . . . . . . 10 (𝑓 = 𝑥 → (𝑄𝑓) = (𝑄𝑥))
313312fveq1d 6653 . . . . . . . . 9 (𝑓 = 𝑥 → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
314312fveq1d 6653 . . . . . . . . . 10 (𝑓 = 𝑥 → ((𝑄𝑓)‘𝐴) = ((𝑄𝑥)‘𝐴))
315314oveq2d 7159 . . . . . . . . 9 (𝑓 = 𝑥 → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))
316313, 315eqeq12d 2775 . . . . . . . 8 (𝑓 = 𝑥 → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
317311, 316elab 3586 . . . . . . 7 (𝑥 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))
318317anbi2i 626 . . . . . 6 ((𝑥 ∈ (𝐻𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
319310, 318bitri 278 . . . . 5 (𝑥 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
320 elin 3870 . . . . . 6 (𝑦 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}))
321 vex 3411 . . . . . . . 8 𝑦 ∈ V
322 fveq2 6651 . . . . . . . . . 10 (𝑓 = 𝑦 → (𝑄𝑓) = (𝑄𝑦))
323322fveq1d 6653 . . . . . . . . 9 (𝑓 = 𝑦 → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
324322fveq1d 6653 . . . . . . . . . 10 (𝑓 = 𝑦 → ((𝑄𝑓)‘𝐴) = ((𝑄𝑦)‘𝐴))
325324oveq2d 7159 . . . . . . . . 9 (𝑓 = 𝑦 → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))
326323, 325eqeq12d 2775 . . . . . . . 8 (𝑓 = 𝑦 → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
327321, 326elab 3586 . . . . . . 7 (𝑦 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))
328327anbi2i 626 . . . . . 6 ((𝑦 ∈ (𝐻𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
329320, 328bitri 278 . . . . 5 (𝑦 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
330319, 329anbi12i 630 . . . 4 ((𝑥 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})) ↔ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))))
33160adantr 485 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑆 ∈ Ring)
332182adantr 485 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑁 𝐿) ∈ 𝐾)
333 eqid 2759 . . . . . . . . 9 (𝑆s (Base‘(𝑆s 𝐼))) = (𝑆s (Base‘(𝑆s 𝐼)))
334 eqid 2759 . . . . . . . . 9 (Base‘(𝑆s (Base‘(𝑆s 𝐼)))) = (Base‘(𝑆s (Base‘(𝑆s 𝐼))))
33550adantr 485 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑆 ∈ CRing)
336 fvexd 6666 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (Base‘(𝑆s 𝐼)) ∈ V)
337 eqid 2759 . . . . . . . . . . . . . . 15 (𝑆s (𝐾m 𝐼)) = (𝑆s (𝐾m 𝐼))
33847, 4, 10, 337, 48evlsrhm 20836 . . . . . . . . . . . . . 14 ((𝐼𝑉𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆s (𝐾m 𝐼))))
3398, 50, 9, 338syl3anc 1369 . . . . . . . . . . . . 13 (𝜑𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆s (𝐾m 𝐼))))
340 eqid 2759 . . . . . . . . . . . . . 14 (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(𝑆s (𝐾m 𝐼)))
34149, 340rhmf 19534 . . . . . . . . . . . . 13 (𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆s (𝐾m 𝐼))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆s (𝐾m 𝐼))))
342339, 341syl 17 . . . . . . . . . . . 12 (𝜑𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆s (𝐾m 𝐼))))
343342adantr 485 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆s (𝐾m 𝐼))))
3448adantr 485 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝐼𝑉)
34512adantr 485 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝑈 ∈ Ring)
34614adantr 485 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝑁 ∈ ℕ0)
347 simpr 489 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝑥 ∈ (𝐻𝑁))
3481, 4, 49, 344, 345, 346, 347mhpmpl 20872 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐻𝑁)) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
349348adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
350349adantrr 717 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)))
351343, 350ffvelrnd 6836 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑥) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
352 eqid 2759 . . . . . . . . . . . . . . 15 (𝑆s 𝐼) = (𝑆s 𝐼)
353352, 48pwsbas 16803 . . . . . . . . . . . . . 14 ((𝑆 ∈ CRing ∧ 𝐼𝑉) → (𝐾m 𝐼) = (Base‘(𝑆s 𝐼)))
35450, 8, 353syl2anc 588 . . . . . . . . . . . . 13 (𝜑 → (𝐾m 𝐼) = (Base‘(𝑆s 𝐼)))
355354oveq2d 7159 . . . . . . . . . . . 12 (𝜑 → (𝑆s (𝐾m 𝐼)) = (𝑆s (Base‘(𝑆s 𝐼))))
356355fveq2d 6655 . . . . . . . . . . 11 (𝜑 → (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(𝑆s (Base‘(𝑆s 𝐼)))))
357356adantr 485 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (Base‘(𝑆s (𝐾m 𝐼))) = (Base‘(𝑆s (Base‘(𝑆s 𝐼)))))
358351, 357eleqtrd 2853 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑥) ∈ (Base‘(𝑆s (Base‘(𝑆s 𝐼)))))
359333, 48, 334, 335, 336, 358pwselbas 16805 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑥):(Base‘(𝑆s 𝐼))⟶𝐾)
36054, 354eleqtrd 2853 . . . . . . . . 9 (𝜑𝐴 ∈ (Base‘(𝑆s 𝐼)))
361360adantr 485 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐴 ∈ (Base‘(𝑆s 𝐼)))
362359, 361ffvelrnd 6836 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄𝑥)‘𝐴) ∈ 𝐾)
3638adantr 485 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝐼𝑉)
36412adantr 485 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝑈 ∈ Ring)
36514adantr 485 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝑁 ∈ ℕ0)
366 simpr 489 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝑦 ∈ (𝐻𝑁))
3671, 4, 49, 363, 364, 365, 366mhpmpl 20872 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝐻𝑁)) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
368367adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
369368adantrl 716 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)))
370343, 369ffvelrnd 6836 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑦) ∈ (Base‘(𝑆s (𝐾m 𝐼))))
371370, 357eleqtrd 2853 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑦) ∈ (Base‘(𝑆s (Base‘(𝑆s 𝐼)))))
372333, 48, 334, 335, 336, 371pwselbas 16805 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑄𝑦):(Base‘(𝑆s 𝐼))⟶𝐾)
373372, 361ffvelrnd 6836 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄𝑦)‘𝐴) ∈ 𝐾)
374 eqid 2759 . . . . . . . 8 (+g𝑆) = (+g𝑆)
37548, 374, 29ringdi 19372 . . . . . . 7 ((𝑆 ∈ Ring ∧ ((𝑁 𝐿) ∈ 𝐾 ∧ ((𝑄𝑥)‘𝐴) ∈ 𝐾 ∧ ((𝑄𝑦)‘𝐴) ∈ 𝐾)) → ((𝑁 𝐿) · (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴))) = (((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))(+g𝑆)((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
376331, 332, 362, 373, 375syl13anc 1370 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑁 𝐿) · (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴))) = (((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))(+g𝑆)((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
3778adantr 485 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐼𝑉)
3789adantr 485 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝑅 ∈ (SubRing‘𝑆))
37954adantr 485 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐴 ∈ (𝐾m 𝐼))
380 eqidd 2760 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) → ((𝑄𝑥)‘𝐴) = ((𝑄𝑥)‘𝐴))
381348, 380anim12dan 622 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑥)‘𝐴) = ((𝑄𝑥)‘𝐴)))
382381adantrr 717 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑥)‘𝐴) = ((𝑄𝑥)‘𝐴)))
383 eqidd 2760 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))) → ((𝑄𝑦)‘𝐴) = ((𝑄𝑦)‘𝐴))
384367, 383anim12dan 622 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑦)‘𝐴) = ((𝑄𝑦)‘𝐴)))
385384adantrl 716 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑦)‘𝐴) = ((𝑄𝑦)‘𝐴)))
38647, 4, 10, 48, 49, 377, 335, 378, 379, 382, 385, 5, 374evlsaddval 39767 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴))))
387386simprd 500 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴)))
388387oveq2d 7159 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)) = ((𝑁 𝐿) · (((𝑄𝑥)‘𝐴)(+g𝑆)((𝑄𝑦)‘𝐴))))
38958a1i 11 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐾 ∈ V)
39063adantlr 715 . . . . . . . . . 10 (((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) ∧ (𝑗𝐾𝑘𝐾)) → (𝑗 · 𝑘) ∈ 𝐾)
39168adantr 485 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝐼 × {𝐿}):𝐼𝐾)
39270adantr 485 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → 𝐴:𝐼𝐾)
393390, 391, 392, 377, 377, 71off 7415 . . . . . . . . 9 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼𝐾)
394389, 377, 393elmapdd 39707 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾m 𝐼))
395 simpr 489 . . . . . . . . . 10 ((𝜑 ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) → ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))
396348, 395anim12dan 622 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
397396adantrr 717 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))))
398 simpr 489 . . . . . . . . . 10 ((𝜑 ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))) → ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))
399367, 398anim12dan 622 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
400399adantrl 716 . . . . . . . 8 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
40147, 4, 10, 48, 49, 377, 335, 378, 394, 397, 400, 5, 374evlsaddval 39767 . . . . . . 7 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))(+g𝑆)((𝑁 𝐿) · ((𝑄𝑦)‘𝐴)))))
402401simprd 500 . . . . . 6 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))(+g𝑆)((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))
403376, 388, 4023eqtr4rd 2805 . . . . 5 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
404 ovex 7176 . . . . . 6 (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ V
405 fveq2 6651 . . . . . . . 8 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (𝑄𝑓) = (𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦)))
406405fveq1d 6653 . . . . . . 7 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)))
407405fveq1d 6653 . . . . . . . 8 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄𝑓)‘𝐴) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))
408407oveq2d 7159 . . . . . . 7 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
409406, 408eqeq12d 2775 . . . . . 6 (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))))
410404, 409elab 3586 . . . . 5 ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))
411403, 410sylibr 237 . . . 4 ((𝜑 ∧ ((𝑥 ∈ (𝐻𝑁) ∧ ((𝑄𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻𝑁) ∧ ((𝑄𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑦)‘𝐴))))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
412330, 411sylan2b 597 . . 3 ((𝜑 ∧ (𝑥 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻𝑁) ∩ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))}))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
4131, 2, 3, 4, 5, 6, 7, 8, 13, 14, 15, 85, 309, 412mhpind 39773 . 2 (𝜑𝑋 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))})
414 fveq2 6651 . . . . . 6 (𝑓 = 𝑋 → (𝑄𝑓) = (𝑄𝑋))
415414fveq1d 6653 . . . . 5 (𝑓 = 𝑋 → ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)))
416414fveq1d 6653 . . . . . 6 (𝑓 = 𝑋 → ((𝑄𝑓)‘𝐴) = ((𝑄𝑋)‘𝐴))
417416oveq2d 7159 . . . . 5 (𝑓 = 𝑋 → ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴)))
418415, 417eqeq12d 2775 . . . 4 (𝑓 = 𝑋 → (((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴)) ↔ ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴))))
419418elabg 3585 . . 3 (𝑋 ∈ (𝐻𝑁) → (𝑋 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴))))
42015, 419syl 17 . 2 (𝜑 → (𝑋 ∈ {𝑓 ∣ ((𝑄𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑓)‘𝐴))} ↔ ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴))))
421413, 420mpbid 235 1 (𝜑 → ((𝑄𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 𝐿) · ((𝑄𝑋)‘𝐴)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  {cab 2736  {crab 3072  Vcvv 3407   ∖ cdif 3851   ∩ cin 3853   ⊆ wss 3854  ifcif 4413  {csn 4515   class class class wbr 5025   ↦ cmpt 5105   × cxp 5515  ◡ccnv 5516   “ cima 5520  Fun wfun 6322   Fn wfn 6323  ⟶wf 6324  ‘cfv 6328  (class class class)co 7143   ∘f cof 7396   supp csupp 7828   ↑m cmap 8409  Fincfn 8520   finSupp cfsupp 8851  0cc0 10560  ℕcn 11659  ℕ0cn0 11919  Basecbs 16526   ↾s cress 16527  +gcplusg 16608  .rcmulr 16609  Scalarcsca 16611   ·𝑠 cvsca 16612  0gc0g 16756   Σg cgsu 16757   ↑s cpws 16763  Mndcmnd 17962  SubMndcsubmnd 18006  .gcmg 18276  CMndccmn 18958  mulGrpcmgp 19292  1rcur 19304  Ringcrg 19350  CRingccrg 19351   RingHom crh 19520  SubRingcsubrg 19584  LModclmod 19687  ℂfldccnfld 20151  AssAlgcasa 20600  algSccascl 20602   mPwSer cmps 20651   mPoly cmpl 20653   evalSub ces 20818   mHomP cmhp 20857 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-cnex 10616  ax-resscn 10617  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-mulcom 10624  ax-addass 10625  ax-mulass 10626  ax-distr 10627  ax-i2m1 10628  ax-1ne0 10629  ax-1rid 10630  ax-rnegex 10631  ax-rrecex 10632  ax-cnre 10633  ax-pre-lttri 10634  ax-pre-lttrn 10635  ax-pre-ltadd 10636  ax-pre-mulgt0 10637  ax-addf 10639  ax-mulf 10640 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-nel 3054  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-int 4832  df-iun 4878  df-iin 4879  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-se 5477  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-of 7398  df-ofr 7399  df-om 7573  df-1st 7686  df-2nd 7687  df-supp 7829  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-1o 8105  df-2o 8106  df-oadd 8109  df-er 8292  df-map 8411  df-pm 8412  df-ixp 8473  df-en 8521  df-dom 8522  df-sdom 8523  df-fin 8524  df-fsupp 8852  df-sup 8924  df-oi 8992  df-dju 9348  df-card 9386  df-pnf 10700  df-mnf 10701  df-xr 10702  df-ltxr 10703  df-le 10704  df-sub 10895  df-neg 10896  df-nn 11660  df-2 11722  df-3 11723  df-4 11724  df-5 11725  df-6 11726  df-7 11727  df-8 11728  df-9 11729  df-n0 11920  df-z 12006  df-dec 12123  df-uz 12268  df-fz 12925  df-fzo 13068  df-seq 13404  df-hash 13726  df-struct 16528  df-ndx 16529  df-slot 16530  df-base 16532  df-sets 16533  df-ress 16534  df-plusg 16621  df-mulr 16622  df-starv 16623  df-sca 16624  df-vsca 16625  df-ip 16626  df-tset 16627  df-ple 16628  df-ds 16630  df-unif 16631  df-hom 16632  df-cco 16633  df-0g 16758  df-gsum 16759  df-prds 16764  df-pws 16766  df-mre 16900  df-mrc 16901  df-acs 16903  df-mgm 17903  df-sgrp 17952  df-mnd 17963  df-mhm 18007  df-submnd 18008  df-grp 18157  df-minusg 18158  df-sbg 18159  df-mulg 18277  df-subg 18328  df-ghm 18408  df-cntz 18499  df-cmn 18960  df-abl 18961  df-mgp 19293  df-ur 19305  df-srg 19309  df-ring 19352  df-cring 19353  df-rnghom 19523  df-subrg 19586  df-lmod 19689  df-lss 19757  df-lsp 19797  df-cnfld 20152  df-assa 20603  df-asp 20604  df-ascl 20605  df-psr 20656  df-mvr 20657  df-mpl 20658  df-evls 20820  df-mhp 20861 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator