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