Metamath Proof Explorer

Theorem mhphf

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 ( QX ) which corresponds to X ). (Contributed by SN, 28-Jul-2024)

Ref Expression
Hypotheses 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 mhphf ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 mhphf.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 mhphf.h ⊢ 𝐻 = ( 𝐼 mHomP 𝑈 )
3 mhphf.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4 mhphf.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
5 mhphf.m ⊢ · = ( .r ‘ 𝑆 )
6 mhphf.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
7 mhphf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8 mhphf.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
9 mhphf.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
10 mhphf.l ⊢ ( 𝜑 → 𝐿 ∈ 𝑅 )
11 mhphf.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 mhphf.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) )
13 mhphf.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
14 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
15 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
16 eqid ⊢ ( 𝐼 mPoly 𝑈 ) = ( 𝐼 mPoly 𝑈 )
17 eqid ⊢ ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) = ( +g ‘ ( 𝐼 mPoly 𝑈 ) )
18 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
19 eqid ⊢ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } = { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
20 3 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
21 9 20 syl ⊢ ( 𝜑 → 𝑈 ∈ Ring )
22 21 ringgrpd ⊢ ( 𝜑 → 𝑈 ∈ Grp )
23 eqid ⊢ ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) = ( algSc ‘ ( 𝐼 mPoly 𝑈 ) )
24 eqid ⊢ ( 0g ‘ ( 𝐼 mPoly 𝑈 ) ) = ( 0g ‘ ( 𝐼 mPoly 𝑈 ) )
25 3 subrgcrng ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
26 8 9 25 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
27 16 23 15 24 7 26 mplascl0 ⊢ ( 𝜑 → ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ ( 𝐼 mPoly 𝑈 ) ) )
28 16 18 15 24 7 22 mpl0 ⊢ ( 𝜑 → ( 0g ‘ ( 𝐼 mPoly 𝑈 ) ) = ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑈 ) } ) )
29 27 28 eqtr2d ⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑈 ) } ) = ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) )
30 3 5 ressmulr ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → · = ( .r ‘ 𝑈 ) )
31 9 30 syl ⊢ ( 𝜑 → · = ( .r ‘ 𝑈 ) )
32 31 oveqd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐿 ) · ( 0g ‘ 𝑈 ) ) = ( ( 𝑁 ↑ 𝐿 ) ( .r ‘ 𝑈 ) ( 0g ‘ 𝑈 ) ) )
33 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
34 33 subrgsubm ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑆 ) ) )
35 9 34 syl ⊢ ( 𝜑 → 𝑅 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑆 ) ) )
36 6 submmulgcl ⊢ ( ( 𝑅 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑆 ) ) ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ 𝑅 ) → ( 𝑁 ↑ 𝐿 ) ∈ 𝑅 )
37 35 11 10 36 syl3anc ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐿 ) ∈ 𝑅 )
38 3 subrgbas ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 = ( Base ‘ 𝑈 ) )
39 9 38 syl ⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
40 37 39 eleqtrd ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐿 ) ∈ ( Base ‘ 𝑈 ) )
41 eqid ⊢ ( .r ‘ 𝑈 ) = ( .r ‘ 𝑈 )
42 14 41 15 ringrz ⊢ ( ( 𝑈 ∈ Ring ∧ ( 𝑁 ↑ 𝐿 ) ∈ ( Base ‘ 𝑈 ) ) → ( ( 𝑁 ↑ 𝐿 ) ( .r ‘ 𝑈 ) ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑈 ) )
43 21 40 42 syl2anc ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐿 ) ( .r ‘ 𝑈 ) ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑈 ) )
44 32 43 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐿 ) · ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑈 ) )
45 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑈 ) )
46 14 15 ring0cl ⊢ ( 𝑈 ∈ Ring → ( 0g ‘ 𝑈 ) ∈ ( Base ‘ 𝑈 ) )
47 21 46 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ ( Base ‘ 𝑈 ) )
48 47 39 eleqtrrd ⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ 𝑅 )
49 1 16 3 4 45 23 7 8 9 48 13 evlsscaval ⊢ ( 𝜑 → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ 𝐴 ) = ( 0g ‘ 𝑈 ) ) )
50 49 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ 𝐴 ) = ( 0g ‘ 𝑈 ) )
51 50 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( 0g ‘ 𝑈 ) ) )
52 4 fvexi ⊢ 𝐾 ∈ V
53 52 a1i ⊢ ( 𝜑 → 𝐾 ∈ V )
54 8 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
55 4 5 ringcl ⊢ ( ( 𝑆 ∈ Ring ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑗 · 𝑘 ) ∈ 𝐾 )
56 54 55 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) → ( 𝑗 · 𝑘 ) ∈ 𝐾 )
57 56 3expb ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑗 · 𝑘 ) ∈ 𝐾 )
58 4 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
59 9 58 syl ⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 )
60 59 10 sseldd ⊢ ( 𝜑 → 𝐿 ∈ 𝐾 )
61 fconst6g ⊢ ( 𝐿 ∈ 𝐾 → ( 𝐼 × { 𝐿 } ) : 𝐼 ⟶ 𝐾 )
62 60 61 syl ⊢ ( 𝜑 → ( 𝐼 × { 𝐿 } ) : 𝐼 ⟶ 𝐾 )
63 elmapi ⊢ ( 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐾 )
64 13 63 syl ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐾 )
65 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
66 57 62 64 7 7 65 off ⊢ ( 𝜑 → ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) : 𝐼 ⟶ 𝐾 )
67 53 7 66 elmapdd ⊢ ( 𝜑 → ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ∈ ( 𝐾 ↑m 𝐼 ) )
68 1 16 3 4 45 23 7 8 9 48 67 evlsscaval ⊢ ( 𝜑 → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( 0g ‘ 𝑈 ) ) )
69 68 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( 0g ‘ 𝑈 ) )
70 44 51 69 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ 𝐴 ) ) )
71 fvex ⊢ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ∈ V
72 fveq2 ⊢ ( 𝑓 = ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) → ( 𝑄 ‘ 𝑓 ) = ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) )
73 72 fveq1d ⊢ ( 𝑓 = ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) → ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
74 72 fveq1d ⊢ ( 𝑓 = ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) → ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ 𝐴 ) )
75 74 oveq2d ⊢ ( 𝑓 = ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ 𝐴 ) ) )
76 73 75 eqeq12d ⊢ ( 𝑓 = ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) → ( ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) ↔ ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ 𝐴 ) ) ) )
77 71 76 elab ⊢ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ↔ ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ) ‘ 𝐴 ) ) )
78 70 77 sylibr ⊢ ( 𝜑 → ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ ( 0g ‘ 𝑈 ) ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } )
79 29 78 eqeltrd ⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑈 ) } ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } )
80 16 mplassa ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑈 ∈ CRing ) → ( 𝐼 mPoly 𝑈 ) ∈ AssAlg )
81 7 26 80 syl2anc ⊢ ( 𝜑 → ( 𝐼 mPoly 𝑈 ) ∈ AssAlg )
82 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝐼 mPoly 𝑈 ) ∈ AssAlg )
83 16 7 21 mplsca ⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) )
84 83 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) ) )
85 84 eleq2d ⊢ ( 𝜑 → ( 𝑏 ∈ ( Base ‘ 𝑈 ) ↔ 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) ) ) )
86 85 biimpa ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) → 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) ) )
87 86 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) ) )
88 fvexd ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ∈ V )
89 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
90 89 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
91 90 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V )
92 eqid ⊢ ( 1r ‘ 𝑈 ) = ( 1r ‘ 𝑈 )
93 14 92 ringidcl ⊢ ( 𝑈 ∈ Ring → ( 1r ‘ 𝑈 ) ∈ ( Base ‘ 𝑈 ) )
94 21 93 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑈 ) ∈ ( Base ‘ 𝑈 ) )
95 94 47 ifcld ⊢ ( 𝜑 → if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ∈ ( Base ‘ 𝑈 ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ∈ ( Base ‘ 𝑈 ) )
97 96 fmpttd ⊢ ( 𝜑 → ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑈 ) )
98 88 91 97 elmapdd ⊢ ( 𝜑 → ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( ( Base ‘ 𝑈 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) )
99 eqid ⊢ ( 𝐼 mPwSer 𝑈 ) = ( 𝐼 mPwSer 𝑈 )
100 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑈 ) )
101 99 14 18 100 7 psrbas ⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) = ( ( Base ‘ 𝑈 ) ↑m { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) )
102 98 101 eleqtrrd ⊢ ( 𝜑 → ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) )
103 90 mptex ⊢ ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ V
104 103 a1i ⊢ ( 𝜑 → ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ V )
105 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ V )
106 funmpt ⊢ Fun ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) )
107 106 a1i ⊢ ( 𝜑 → Fun ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) )
108 snfi ⊢ { 𝑎 } ∈ Fin
109 108 a1i ⊢ ( 𝜑 → { 𝑎 } ∈ Fin )
110 eldifsnneq ⊢ ( 𝑤 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑎 } ) → ¬ 𝑤 = 𝑎 )
111 110 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑎 } ) ) → ¬ 𝑤 = 𝑎 )
112 111 iffalsed ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ { 𝑎 } ) ) → if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑈 ) )
113 112 91 suppss2 ⊢ ( 𝜑 → ( ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) supp ( 0g ‘ 𝑈 ) ) ⊆ { 𝑎 } )
114 109 113 ssfid ⊢ ( 𝜑 → ( ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) supp ( 0g ‘ 𝑈 ) ) ∈ Fin )
115 104 105 107 114 isfsuppd ⊢ ( 𝜑 → ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) finSupp ( 0g ‘ 𝑈 ) )
116 16 99 100 15 45 mplelbas ⊢ ( ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ↔ ( ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑈 ) ) ∧ ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) finSupp ( 0g ‘ 𝑈 ) ) )
117 102 115 116 sylanbrc ⊢ ( 𝜑 → ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
118 117 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
119 eqid ⊢ ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) = ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) )
120 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) )
121 eqid ⊢ ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) = ( .r ‘ ( 𝐼 mPoly 𝑈 ) )
122 eqid ⊢ ( ·𝑠 ‘ ( 𝐼 mPoly 𝑈 ) ) = ( ·𝑠 ‘ ( 𝐼 mPoly 𝑈 ) )
123 23 119 120 45 121 122 asclmul1 ⊢ ( ( ( 𝐼 mPoly 𝑈 ) ∈ AssAlg ∧ 𝑏 ∈ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly 𝑈 ) ) ) ∧ ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) = ( 𝑏 ( ·𝑠 ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) )
124 82 87 118 123 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) = ( 𝑏 ( ·𝑠 ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) )
125 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑏 ∈ ( Base ‘ 𝑈 ) )
126 16 122 14 45 41 18 125 118 mplvsca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑏 ( ·𝑠 ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑏 } ) ∘f ( .r ‘ 𝑈 ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) )
127 124 126 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑏 } ) ∘f ( .r ‘ 𝑈 ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) )
128 vex ⊢ 𝑏 ∈ V
129 fnconstg ⊢ ( 𝑏 ∈ V → ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑏 } ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
130 128 129 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑏 } ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
131 fvex ⊢ ( 1r ‘ 𝑈 ) ∈ V
132 fvex ⊢ ( 0g ‘ 𝑈 ) ∈ V
133 131 132 ifex ⊢ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ∈ V
134 eqid ⊢ ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) = ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) )
135 133 134 fnmpti ⊢ ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
136 135 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) Fn { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
137 90 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V )
138 inidm ⊢ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∩ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
139 128 fvconst2 ⊢ ( 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑏 } ) ‘ 𝑠 ) = 𝑏 )
140 139 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑏 } ) ‘ 𝑠 ) = 𝑏 )
141 equequ1 ⊢ ( 𝑤 = 𝑠 → ( 𝑤 = 𝑎 ↔ 𝑠 = 𝑎 ) )
142 141 ifbid ⊢ ( 𝑤 = 𝑠 → if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) = if ( 𝑠 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) )
143 131 132 ifex ⊢ if ( 𝑠 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ∈ V
144 142 134 143 fvmpt ⊢ ( 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → ( ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ‘ 𝑠 ) = if ( 𝑠 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) )
145 144 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ‘ 𝑠 ) = if ( 𝑠 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) )
146 130 136 137 137 138 140 145 offval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝑏 } ) ∘f ( .r ‘ 𝑈 ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) = ( 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑏 ( .r ‘ 𝑈 ) if ( 𝑠 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) )
147 ovif2 ⊢ ( 𝑏 ( .r ‘ 𝑈 ) if ( 𝑠 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) = if ( 𝑠 = 𝑎 , ( 𝑏 ( .r ‘ 𝑈 ) ( 1r ‘ 𝑈 ) ) , ( 𝑏 ( .r ‘ 𝑈 ) ( 0g ‘ 𝑈 ) ) )
148 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑈 ∈ Ring )
149 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑏 ∈ ( Base ‘ 𝑈 ) )
150 14 41 92 148 149 ringridmd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑏 ( .r ‘ 𝑈 ) ( 1r ‘ 𝑈 ) ) = 𝑏 )
151 14 41 15 ringrz ⊢ ( ( 𝑈 ∈ Ring ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑏 ( .r ‘ 𝑈 ) ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑈 ) )
152 148 149 151 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑏 ( .r ‘ 𝑈 ) ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑈 ) )
153 150 152 ifeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → if ( 𝑠 = 𝑎 , ( 𝑏 ( .r ‘ 𝑈 ) ( 1r ‘ 𝑈 ) ) , ( 𝑏 ( .r ‘ 𝑈 ) ( 0g ‘ 𝑈 ) ) ) = if ( 𝑠 = 𝑎 , 𝑏 , ( 0g ‘ 𝑈 ) ) )
154 147 153 eqtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑏 ( .r ‘ 𝑈 ) if ( 𝑠 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) = if ( 𝑠 = 𝑎 , 𝑏 , ( 0g ‘ 𝑈 ) ) )
155 154 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝑏 ( .r ‘ 𝑈 ) if ( 𝑠 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) = ( 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑠 = 𝑎 , 𝑏 , ( 0g ‘ 𝑈 ) ) ) )
156 127 146 155 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) = ( 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑠 = 𝑎 , 𝑏 , ( 0g ‘ 𝑈 ) ) ) )
157 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝐼 ∈ 𝑉 )
158 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑆 ∈ CRing )
159 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
160 67 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ∈ ( 𝐾 ↑m 𝐼 ) )
161 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑈 ∈ Ring )
162 16 45 14 23 157 161 mplasclf ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
163 162 125 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
164 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
165 163 164 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) ) )
166 elrabi ⊢ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } → 𝑎 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
167 166 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑎 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
168 1 16 3 45 4 33 6 15 92 18 134 157 158 159 160 167 evlsbagval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) ) ) ) )
169 1 16 3 4 45 157 158 159 160 165 168 121 5 evlsmulval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) ) ) ) ) )
170 169 simprd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) ) ) ) )
171 33 ringmgp ⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
172 54 171 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
173 33 4 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
174 173 6 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑆 ) ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ) → ( 𝑁 ↑ 𝐿 ) ∈ 𝐾 )
175 172 11 60 174 syl3anc ⊢ ( 𝜑 → ( 𝑁 ↑ 𝐿 ) ∈ 𝐾 )
176 175 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑁 ↑ 𝐿 ) ∈ 𝐾 )
177 39 59 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) ⊆ 𝐾 )
178 177 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) → 𝑏 ∈ 𝐾 )
179 178 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑏 ∈ 𝐾 )
180 4 5 crngcom ⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝑁 ↑ 𝐿 ) ∈ 𝐾 ∧ 𝑏 ∈ 𝐾 ) → ( ( 𝑁 ↑ 𝐿 ) · 𝑏 ) = ( 𝑏 · ( 𝑁 ↑ 𝐿 ) ) )
181 158 176 179 180 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑁 ↑ 𝐿 ) · 𝑏 ) = ( 𝑏 · ( 𝑁 ↑ 𝐿 ) ) )
182 181 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( 𝑁 ↑ 𝐿 ) · 𝑏 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 𝑏 · ( 𝑁 ↑ 𝐿 ) ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
183 158 crngringd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑆 ∈ Ring )
184 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
185 33 184 ringidval ⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ ( mulGrp ‘ 𝑆 ) )
186 33 crngmgp ⊢ ( 𝑆 ∈ CRing → ( mulGrp ‘ 𝑆 ) ∈ CMnd )
187 8 186 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ CMnd )
188 187 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( mulGrp ‘ 𝑆 ) ∈ CMnd )
189 172 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
190 elrabi ⊢ ( 𝑎 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) )
191 elmapi ⊢ ( 𝑎 ∈ ( ℕ0 ↑m 𝐼 ) → 𝑎 : 𝐼 ⟶ ℕ0 )
192 166 190 191 3syl ⊢ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } → 𝑎 : 𝐼 ⟶ ℕ0 )
193 192 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → 𝑎 : 𝐼 ⟶ ℕ0 )
194 193 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑎 : 𝐼 ⟶ ℕ0 )
195 194 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑣 ) ∈ ℕ0 )
196 64 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐾 )
197 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → 𝑣 ∈ 𝐼 )
198 196 197 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 )
199 173 6 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑆 ) ∈ Mnd ∧ ( 𝑎 ‘ 𝑣 ) ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 ) → ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ∈ 𝐾 )
200 189 195 198 199 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ∈ 𝐾 )
201 200 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) : 𝐼 ⟶ 𝐾 )
202 18 psrbagfsupp ⊢ ( 𝑎 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → 𝑎 finSupp 0 )
203 202 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → 𝑎 finSupp 0 )
204 203 fsuppimpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) → ( 𝑎 supp 0 ) ∈ Fin )
205 166 204 sylan2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑎 supp 0 ) ∈ Fin )
206 205 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑎 supp 0 ) ∈ Fin )
207 194 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑎 = ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) )
208 207 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑎 supp 0 ) = ( ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) supp 0 ) )
209 ssidd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑎 supp 0 ) ⊆ ( 𝑎 supp 0 ) )
210 208 209 eqsstrrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) supp 0 ) ⊆ ( 𝑎 supp 0 ) )
211 173 185 6 mulg0 ⊢ ( 𝑘 ∈ 𝐾 → ( 0 ↑ 𝑘 ) = ( 1r ‘ 𝑆 ) )
212 211 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑘 ∈ 𝐾 ) → ( 0 ↑ 𝑘 ) = ( 1r ‘ 𝑆 ) )
213 c0ex ⊢ 0 ∈ V
214 213 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 0 ∈ V )
215 210 212 195 198 214 suppssov1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) supp ( 1r ‘ 𝑆 ) ) ⊆ ( 𝑎 supp 0 ) )
216 206 215 ssfid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) supp ( 1r ‘ 𝑆 ) ) ∈ Fin )
217 173 185 188 157 201 216 gsumcl2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ∈ 𝐾 )
218 4 5 183 176 179 217 ringassd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( 𝑁 ↑ 𝐿 ) · 𝑏 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( 𝑏 · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
219 4 5 183 179 176 217 ringassd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑏 · ( 𝑁 ↑ 𝐿 ) ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( 𝑏 · ( ( 𝑁 ↑ 𝐿 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
220 182 218 219 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑁 ↑ 𝐿 ) · ( 𝑏 · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) = ( 𝑏 · ( ( 𝑁 ↑ 𝐿 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
221 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
222 39 eleq2d ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑅 ↔ 𝑏 ∈ ( Base ‘ 𝑈 ) ) )
223 222 biimpar ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) → 𝑏 ∈ 𝑅 )
224 223 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝑏 ∈ 𝑅 )
225 1 16 3 4 45 23 157 158 159 224 221 evlsscaval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ 𝐴 ) = 𝑏 ) )
226 1 16 3 45 4 33 6 15 92 18 134 157 158 159 221 167 evlsbagval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ‘ 𝐴 ) = ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
227 1 16 3 4 45 157 158 159 221 225 226 121 5 evlsmulval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) = ( 𝑏 · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
228 227 simprd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) = ( 𝑏 · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
229 228 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( 𝑏 · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
230 1 16 3 4 45 23 157 158 159 224 160 evlsscaval ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = 𝑏 ) )
231 230 simprd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = 𝑏 )
232 fconst6g ⊢ ( 𝐿 ∈ 𝑅 → ( 𝐼 × { 𝐿 } ) : 𝐼 ⟶ 𝑅 )
233 10 232 syl ⊢ ( 𝜑 → ( 𝐼 × { 𝐿 } ) : 𝐼 ⟶ 𝑅 )
234 233 ffnd ⊢ ( 𝜑 → ( 𝐼 × { 𝐿 } ) Fn 𝐼 )
235 234 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝐼 × { 𝐿 } ) Fn 𝐼 )
236 64 ffnd ⊢ ( 𝜑 → 𝐴 Fn 𝐼 )
237 236 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → 𝐴 Fn 𝐼 )
238 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → 𝐿 ∈ 𝑅 )
239 fvconst2g ⊢ ( ( 𝐿 ∈ 𝑅 ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝐼 × { 𝐿 } ) ‘ 𝑣 ) = 𝐿 )
240 238 197 239 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝐼 × { 𝐿 } ) ‘ 𝑣 ) = 𝐿 )
241 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑣 ) = ( 𝐴 ‘ 𝑣 ) )
242 235 237 157 157 65 240 241 ofval ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) = ( 𝐿 · ( 𝐴 ‘ 𝑣 ) ) )
243 242 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) = ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐿 · ( 𝐴 ‘ 𝑣 ) ) ) )
244 187 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( mulGrp ‘ 𝑆 ) ∈ CMnd )
245 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → 𝐿 ∈ 𝐾 )
246 33 5 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ 𝑆 ) )
247 173 6 246 mulgnn0di ⊢ ( ( ( mulGrp ‘ 𝑆 ) ∈ CMnd ∧ ( ( 𝑎 ‘ 𝑣 ) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ∧ ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 ) ) → ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐿 · ( 𝐴 ‘ 𝑣 ) ) ) = ( ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) · ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
248 244 195 245 198 247 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐿 · ( 𝐴 ‘ 𝑣 ) ) ) = ( ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) · ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
249 243 248 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) = ( ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) · ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
250 249 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) ) = ( 𝑣 ∈ 𝐼 ↦ ( ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) · ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) )
251 250 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) ) ) = ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) · ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
252 187 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( mulGrp ‘ 𝑆 ) ∈ CMnd )
253 7 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → 𝐼 ∈ 𝑉 )
254 172 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ∧ 𝑣 ∈ 𝐼 ) → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
255 193 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑣 ) ∈ ℕ0 )
256 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ∧ 𝑣 ∈ 𝐼 ) → 𝐿 ∈ 𝐾 )
257 173 6 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑆 ) ∈ Mnd ∧ ( 𝑎 ‘ 𝑣 ) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ) → ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ∈ 𝐾 )
258 254 255 256 257 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ∈ 𝐾 )
259 64 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 )
260 259 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑣 ) ∈ 𝐾 )
261 254 255 260 199 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ∧ 𝑣 ∈ 𝐼 ) → ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ∈ 𝐾 )
262 eqidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) = ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) )
263 eqidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) = ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
264 253 mptexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) ∈ V )
265 fvexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 1r ‘ 𝑆 ) ∈ V )
266 funmpt ⊢ Fun ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) )
267 266 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → Fun ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) )
268 193 feqmptd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → 𝑎 = ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) )
269 268 oveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑎 supp 0 ) = ( ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) supp 0 ) )
270 ssidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑎 supp 0 ) ⊆ ( 𝑎 supp 0 ) )
271 269 270 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) supp 0 ) ⊆ ( 𝑎 supp 0 ) )
272 211 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ∧ 𝑘 ∈ 𝐾 ) → ( 0 ↑ 𝑘 ) = ( 1r ‘ 𝑆 ) )
273 213 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → 0 ∈ V )
274 271 272 255 256 273 suppssov1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) supp ( 1r ‘ 𝑆 ) ) ⊆ ( 𝑎 supp 0 ) )
275 205 274 ssfid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) supp ( 1r ‘ 𝑆 ) ) ∈ Fin )
276 264 265 267 275 isfsuppd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) finSupp ( 1r ‘ 𝑆 ) )
277 253 mptexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ∈ V )
278 funmpt ⊢ Fun ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) )
279 278 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → Fun ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) )
280 271 272 255 260 273 suppssov1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) supp ( 1r ‘ 𝑆 ) ) ⊆ ( 𝑎 supp 0 ) )
281 205 280 ssfid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) supp ( 1r ‘ 𝑆 ) ) ∈ Fin )
282 277 265 279 281 isfsuppd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) finSupp ( 1r ‘ 𝑆 ) )
283 173 185 246 252 253 258 261 262 263 276 282 gsummptfsadd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) · ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
284 18 19 173 6 7 172 60 11 mhphflem ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) ) = ( 𝑁 ↑ 𝐿 ) )
285 284 oveq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) ) ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
286 283 285 eqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) → ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) · ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
287 286 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( ( 𝑎 ‘ 𝑣 ) ↑ 𝐿 ) · ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
288 251 287 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) )
289 231 288 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) ) ) ) = ( 𝑏 · ( ( 𝑁 ↑ 𝐿 ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( 𝐴 ‘ 𝑣 ) ) ) ) ) ) )
290 220 229 289 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( 𝑄 ‘ ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) · ( ( mulGrp ‘ 𝑆 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) ↑ ( ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ‘ 𝑣 ) ) ) ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) ) )
291 170 290 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) ) )
292 ovex ⊢ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ∈ V
293 fveq2 ⊢ ( 𝑓 = ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑄 ‘ 𝑓 ) = ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) )
294 293 fveq1d ⊢ ( 𝑓 = ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) → ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
295 293 fveq1d ⊢ ( 𝑓 = ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) → ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) )
296 295 oveq2d ⊢ ( 𝑓 = ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) ) )
297 294 296 eqeq12d ⊢ ( 𝑓 = ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) → ( ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) ↔ ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) ) ) )
298 292 297 elab ⊢ ( ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ↔ ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ) ‘ 𝐴 ) ) )
299 291 298 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly 𝑈 ) ) ‘ 𝑏 ) ( .r ‘ ( 𝐼 mPoly 𝑈 ) ) ( 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑤 = 𝑎 , ( 1r ‘ 𝑈 ) , ( 0g ‘ 𝑈 ) ) ) ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } )
300 156 299 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ∧ 𝑏 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑠 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑠 = 𝑎 , 𝑏 , ( 0g ‘ 𝑈 ) ) ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } )
301 elin ⊢ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ↔ ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ 𝑥 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) )
302 vex ⊢ 𝑥 ∈ V
303 fveq2 ⊢ ( 𝑓 = 𝑥 → ( 𝑄 ‘ 𝑓 ) = ( 𝑄 ‘ 𝑥 ) )
304 303 fveq1d ⊢ ( 𝑓 = 𝑥 → ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
305 303 fveq1d ⊢ ( 𝑓 = 𝑥 → ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) )
306 305 oveq2d ⊢ ( 𝑓 = 𝑥 → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) )
307 304 306 eqeq12d ⊢ ( 𝑓 = 𝑥 → ( ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) ↔ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
308 302 307 elab ⊢ ( 𝑥 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ↔ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) )
309 308 anbi2i ⊢ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ 𝑥 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ↔ ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
310 301 309 bitri ⊢ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ↔ ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
311 elin ⊢ ( 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ↔ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ 𝑦 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) )
312 vex ⊢ 𝑦 ∈ V
313 fveq2 ⊢ ( 𝑓 = 𝑦 → ( 𝑄 ‘ 𝑓 ) = ( 𝑄 ‘ 𝑦 ) )
314 313 fveq1d ⊢ ( 𝑓 = 𝑦 → ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
315 313 fveq1d ⊢ ( 𝑓 = 𝑦 → ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) )
316 315 oveq2d ⊢ ( 𝑓 = 𝑦 → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) )
317 314 316 eqeq12d ⊢ ( 𝑓 = 𝑦 → ( ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) ↔ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
318 312 317 elab ⊢ ( 𝑦 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ↔ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) )
319 318 anbi2i ⊢ ( ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ 𝑦 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ↔ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
320 311 319 bitri ⊢ ( 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ↔ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
321 310 320 anbi12i ⊢ ( ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ) ↔ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) )
322 54 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝑆 ∈ Ring )
323 175 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑁 ↑ 𝐿 ) ∈ 𝐾 )
324 eqid ⊢ ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ) = ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) )
325 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ) ) = ( Base ‘ ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ) )
326 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝑆 ∈ CRing )
327 fvexd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ∈ V )
328 eqid ⊢ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
329 1 16 3 328 4 evlsrhm ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( ( 𝐼 mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
330 7 8 9 329 syl3anc ⊢ ( 𝜑 → 𝑄 ∈ ( ( 𝐼 mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
331 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
332 45 331 rhmf ⊢ ( 𝑄 ∈ ( ( 𝐼 mPoly 𝑈 ) RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑄 : ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
333 330 332 syl ⊢ ( 𝜑 → 𝑄 : ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
334 333 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝑄 : ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
335 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝐼 ∈ 𝑉 )
336 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑈 ∈ Ring )
337 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
338 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) )
339 2 16 45 335 336 337 338 mhpmpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
340 339 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
341 340 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
342 334 341 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑄 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
343 eqid ⊢ ( 𝑆 ↑s 𝐼 ) = ( 𝑆 ↑s 𝐼 )
344 343 4 pwsbas ⊢ ( ( 𝑆 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → ( 𝐾 ↑m 𝐼 ) = ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) )
345 8 7 344 syl2anc ⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) = ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) )
346 345 oveq2d ⊢ ( 𝜑 → ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ) )
347 346 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ) ) )
348 347 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ) ) )
349 342 348 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑄 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ) ) )
350 324 4 325 326 327 349 pwselbas ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑄 ‘ 𝑥 ) : ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ⟶ 𝐾 )
351 13 345 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) )
352 351 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝐴 ∈ ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) )
353 350 352 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ∈ 𝐾 )
354 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝐼 ∈ 𝑉 )
355 21 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑈 ∈ Ring )
356 11 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
357 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) )
358 2 16 45 354 355 356 357 mhpmpl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
359 358 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) → 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
360 359 adantrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) )
361 334 360 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑄 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
362 361 348 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑄 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑆 ↑s ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ) ) )
363 324 4 325 326 327 362 pwselbas ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑄 ‘ 𝑦 ) : ( Base ‘ ( 𝑆 ↑s 𝐼 ) ) ⟶ 𝐾 )
364 363 352 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ∈ 𝐾 )
365 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
366 4 365 5 ringdi ⊢ ( ( 𝑆 ∈ Ring ∧ ( ( 𝑁 ↑ 𝐿 ) ∈ 𝐾 ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ∈ 𝐾 ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ∈ 𝐾 ) ) → ( ( 𝑁 ↑ 𝐿 ) · ( ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ( +g ‘ 𝑆 ) ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) = ( ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ( +g ‘ 𝑆 ) ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
367 322 323 353 364 366 syl13anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑁 ↑ 𝐿 ) · ( ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ( +g ‘ 𝑆 ) ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) = ( ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ( +g ‘ 𝑆 ) ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
368 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝐼 ∈ 𝑉 )
369 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
370 13 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
371 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) → ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) )
372 339 371 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) → ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) )
373 372 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) )
374 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) )
375 358 374 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) → ( 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) )
376 375 adantrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) )
377 1 16 3 4 45 368 326 369 370 373 376 17 365 evlsaddval ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ( +g ‘ 𝑆 ) ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
378 377 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ( +g ‘ 𝑆 ) ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) )
379 378 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ( +g ‘ 𝑆 ) ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
380 52 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝐾 ∈ V )
381 57 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑗 · 𝑘 ) ∈ 𝐾 )
382 62 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝐼 × { 𝐿 } ) : 𝐼 ⟶ 𝐾 )
383 64 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → 𝐴 : 𝐼 ⟶ 𝐾 )
384 381 382 383 368 368 65 off ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) : 𝐼 ⟶ 𝐾 )
385 380 368 384 elmapdd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ∈ ( 𝐾 ↑m 𝐼 ) )
386 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) → ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) )
387 339 386 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ) → ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
388 387 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) )
389 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) )
390 358 389 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) → ( 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
391 390 adantrl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
392 1 16 3 4 45 368 326 369 385 388 391 17 365 evlsaddval ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑈 ) ) ∧ ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ( +g ‘ 𝑆 ) ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) )
393 392 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ( +g ‘ 𝑆 ) ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) )
394 367 379 393 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ 𝐴 ) ) )
395 ovex ⊢ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ∈ V
396 fveq2 ⊢ ( 𝑓 = ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) → ( 𝑄 ‘ 𝑓 ) = ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) )
397 396 fveq1d ⊢ ( 𝑓 = ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) → ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
398 396 fveq1d ⊢ ( 𝑓 = ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) → ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ 𝐴 ) )
399 398 oveq2d ⊢ ( 𝑓 = ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ 𝐴 ) ) )
400 397 399 eqeq12d ⊢ ( 𝑓 = ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) → ( ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) ↔ ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ 𝐴 ) ) ) )
401 395 400 elab ⊢ ( ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ↔ ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ) ‘ 𝐴 ) ) )
402 394 401 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑥 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑥 ) ‘ 𝐴 ) ) ) ∧ ( 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( 𝑄 ‘ 𝑦 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑦 ) ‘ 𝐴 ) ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } )
403 321 402 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ∧ 𝑦 ∈ ( ( 𝐻 ‘ 𝑁 ) ∩ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ) ) ) → ( 𝑥 ( +g ‘ ( 𝐼 mPoly 𝑈 ) ) 𝑦 ) ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } )
404 2 14 15 16 17 18 19 7 22 11 12 79 300 403 mhpind ⊢ ( 𝜑 → 𝑋 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } )
405 fveq2 ⊢ ( 𝑓 = 𝑋 → ( 𝑄 ‘ 𝑓 ) = ( 𝑄 ‘ 𝑋 ) )
406 405 fveq1d ⊢ ( 𝑓 = 𝑋 → ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) )
407 405 fveq1d ⊢ ( 𝑓 = 𝑋 → ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) )
408 407 oveq2d ⊢ ( 𝑓 = 𝑋 → ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )
409 406 408 eqeq12d ⊢ ( 𝑓 = 𝑋 → ( ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) ↔ ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) ) )
410 409 elabg ⊢ ( 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) → ( 𝑋 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ↔ ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) ) )
411 12 410 syl ⊢ ( 𝜑 → ( 𝑋 ∈ { 𝑓 ∣ ( ( 𝑄 ‘ 𝑓 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑓 ) ‘ 𝐴 ) ) } ↔ ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) ) )
412 404 411 mpbid ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑋 ) ‘ ( ( 𝐼 × { 𝐿 } ) ∘f · 𝐴 ) ) = ( ( 𝑁 ↑ 𝐿 ) · ( ( 𝑄 ‘ 𝑋 ) ‘ 𝐴 ) ) )