Metamath Proof Explorer


Theorem mpfind

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses mpfind.cb 𝐵 = ( Base ‘ 𝑆 )
mpfind.cp + = ( +g𝑆 )
mpfind.ct · = ( .r𝑆 )
mpfind.cq 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
mpfind.ad ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) → 𝜁 )
mpfind.mu ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) → 𝜎 )
mpfind.wa ( 𝑥 = ( ( 𝐵m 𝐼 ) × { 𝑓 } ) → ( 𝜓𝜒 ) )
mpfind.wb ( 𝑥 = ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) → ( 𝜓𝜃 ) )
mpfind.wc ( 𝑥 = 𝑓 → ( 𝜓𝜏 ) )
mpfind.wd ( 𝑥 = 𝑔 → ( 𝜓𝜂 ) )
mpfind.we ( 𝑥 = ( 𝑓f + 𝑔 ) → ( 𝜓𝜁 ) )
mpfind.wf ( 𝑥 = ( 𝑓f · 𝑔 ) → ( 𝜓𝜎 ) )
mpfind.wg ( 𝑥 = 𝐴 → ( 𝜓𝜌 ) )
mpfind.co ( ( 𝜑𝑓𝑅 ) → 𝜒 )
mpfind.pr ( ( 𝜑𝑓𝐼 ) → 𝜃 )
mpfind.a ( 𝜑𝐴𝑄 )
Assertion mpfind ( 𝜑𝜌 )

Proof

Step Hyp Ref Expression
1 mpfind.cb 𝐵 = ( Base ‘ 𝑆 )
2 mpfind.cp + = ( +g𝑆 )
3 mpfind.ct · = ( .r𝑆 )
4 mpfind.cq 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
5 mpfind.ad ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) → 𝜁 )
6 mpfind.mu ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) → 𝜎 )
7 mpfind.wa ( 𝑥 = ( ( 𝐵m 𝐼 ) × { 𝑓 } ) → ( 𝜓𝜒 ) )
8 mpfind.wb ( 𝑥 = ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) → ( 𝜓𝜃 ) )
9 mpfind.wc ( 𝑥 = 𝑓 → ( 𝜓𝜏 ) )
10 mpfind.wd ( 𝑥 = 𝑔 → ( 𝜓𝜂 ) )
11 mpfind.we ( 𝑥 = ( 𝑓f + 𝑔 ) → ( 𝜓𝜁 ) )
12 mpfind.wf ( 𝑥 = ( 𝑓f · 𝑔 ) → ( 𝜓𝜎 ) )
13 mpfind.wg ( 𝑥 = 𝐴 → ( 𝜓𝜌 ) )
14 mpfind.co ( ( 𝜑𝑓𝑅 ) → 𝜒 )
15 mpfind.pr ( ( 𝜑𝑓𝐼 ) → 𝜃 )
16 mpfind.a ( 𝜑𝐴𝑄 )
17 16 4 eleqtrdi ( 𝜑𝐴 ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
18 4 mpfrcl ( 𝐴𝑄 → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) )
19 16 18 syl ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) )
20 eqid ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
21 eqid ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) = ( 𝐼 mPoly ( 𝑆s 𝑅 ) )
22 eqid ( 𝑆s 𝑅 ) = ( 𝑆s 𝑅 )
23 eqid ( 𝑆s ( 𝐵m 𝐼 ) ) = ( 𝑆s ( 𝐵m 𝐼 ) )
24 20 21 22 23 1 evlsrhm ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) RingHom ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
25 eqid ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) )
26 eqid ( Base ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) = ( Base ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) )
27 25 26 rhmf ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) RingHom ( 𝑆s ( 𝐵m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
28 19 24 27 3syl ( 𝜑 → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
29 28 ffnd ( 𝜑 → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
30 fvelrnb ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) → ( 𝐴 ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) = 𝐴 ) )
31 29 30 syl ( 𝜑 → ( 𝐴 ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ↔ ∃ 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) = 𝐴 ) )
32 17 31 mpbid ( 𝜑 → ∃ 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) = 𝐴 )
33 28 ffund ( 𝜑 → Fun ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
34 eqid ( Base ‘ ( 𝑆s 𝑅 ) ) = ( Base ‘ ( 𝑆s 𝑅 ) )
35 eqid ( 𝐼 mVar ( 𝑆s 𝑅 ) ) = ( 𝐼 mVar ( 𝑆s 𝑅 ) )
36 eqid ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) = ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) )
37 eqid ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) = ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) )
38 eqid ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) )
39 19 simp1d ( 𝜑𝐼 ∈ V )
40 19 simp2d ( 𝜑𝑆 ∈ CRing )
41 19 simp3d ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
42 22 subrgcrng ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑆s 𝑅 ) ∈ CRing )
43 40 41 42 syl2anc ( 𝜑 → ( 𝑆s 𝑅 ) ∈ CRing )
44 crngring ( ( 𝑆s 𝑅 ) ∈ CRing → ( 𝑆s 𝑅 ) ∈ Ring )
45 43 44 syl ( 𝜑 → ( 𝑆s 𝑅 ) ∈ Ring )
46 21 39 45 mplringd ( 𝜑 → ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ∈ Ring )
47 46 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ∈ Ring )
48 simprl ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
49 elpreima ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) → ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ) )
50 29 49 syl ( 𝜑 → ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ) )
51 50 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ) )
52 48 51 mpbid ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) )
53 52 simpld ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
54 simprr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
55 elpreima ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) → ( 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) )
56 29 55 syl ( 𝜑 → ( 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) )
57 56 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) )
58 54 57 mpbid ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) )
59 58 simpld ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
60 25 36 ringacl ( ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ∈ Ring ∧ 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
61 47 53 59 60 syl3anc ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
62 rhmghm ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) RingHom ( 𝑆s ( 𝐵m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) GrpHom ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
63 19 24 62 3syl ( 𝜑 → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) GrpHom ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
64 63 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) GrpHom ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
65 eqid ( +g ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) = ( +g ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) )
66 25 36 65 ghmlin ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) GrpHom ( 𝑆s ( 𝐵m 𝐼 ) ) ) ∧ 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ( +g ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
67 64 53 59 66 syl3anc ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ( +g ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
68 40 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → 𝑆 ∈ CRing )
69 ovexd ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝐵m 𝐼 ) ∈ V )
70 28 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
71 70 53 ffvelcdmd ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
72 70 59 ffvelcdmd ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ ( Base ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
73 23 26 68 69 71 72 2 65 pwsplusgval ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ( +g ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f + ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
74 67 73 eqtrd ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f + ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
75 simpl ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → 𝜑 )
76 fnfvelrn ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
77 29 53 76 syl2an2r ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
78 77 4 eleqtrrdi ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 )
79 fvimacnvi ( ( Fun ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∧ 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } )
80 33 48 79 syl2an2r ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } )
81 78 80 jca ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) )
82 fnfvelrn ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
83 29 59 82 syl2an2r ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
84 83 4 eleqtrrdi ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 )
85 fvimacnvi ( ( Fun ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } )
86 33 54 85 syl2an2r ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } )
87 84 86 jca ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) )
88 fvex ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ V
89 fvex ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ V
90 eleq1 ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) → ( 𝑓𝑄 ↔ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ) )
91 vex 𝑓 ∈ V
92 91 9 elab ( 𝑓 ∈ { 𝑥𝜓 } ↔ 𝜏 )
93 eleq1 ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) → ( 𝑓 ∈ { 𝑥𝜓 } ↔ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) )
94 92 93 bitr3id ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) → ( 𝜏 ↔ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) )
95 90 94 anbi12d ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) → ( ( 𝑓𝑄𝜏 ) ↔ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ) )
96 eleq1 ( 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) → ( 𝑔𝑄 ↔ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ) )
97 vex 𝑔 ∈ V
98 97 10 elab ( 𝑔 ∈ { 𝑥𝜓 } ↔ 𝜂 )
99 eleq1 ( 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) → ( 𝑔 ∈ { 𝑥𝜓 } ↔ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) )
100 98 99 bitr3id ( 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) → ( 𝜂 ↔ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) )
101 96 100 anbi12d ( 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) → ( ( 𝑔𝑄𝜂 ) ↔ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) )
102 95 101 bi2anan9 ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ↔ ( ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ∧ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) ) )
103 102 anbi2d ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) ↔ ( 𝜑 ∧ ( ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ∧ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) ) ) )
104 ovex ( 𝑓f + 𝑔 ) ∈ V
105 104 11 elab ( ( 𝑓f + 𝑔 ) ∈ { 𝑥𝜓 } ↔ 𝜁 )
106 oveq12 ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( 𝑓f + 𝑔 ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f + ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
107 106 eleq1d ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( ( 𝑓f + 𝑔 ) ∈ { 𝑥𝜓 } ↔ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f + ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } ) )
108 105 107 bitr3id ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( 𝜁 ↔ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f + ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } ) )
109 103 108 imbi12d ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) → 𝜁 ) ↔ ( ( 𝜑 ∧ ( ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ∧ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f + ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } ) ) )
110 88 89 109 5 vtocl2 ( ( 𝜑 ∧ ( ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ∧ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f + ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } )
111 75 81 87 110 syl12anc ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f + ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } )
112 74 111 eqeltrd ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) ∈ { 𝑥𝜓 } )
113 elpreima ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) → ( ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) ∈ { 𝑥𝜓 } ) ) )
114 29 113 syl ( 𝜑 → ( ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) ∈ { 𝑥𝜓 } ) ) )
115 114 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) ∈ { 𝑥𝜓 } ) ) )
116 61 112 115 mpbir2and ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
117 116 adantlr ( ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑖 ( +g ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
118 25 37 ringcl ( ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ∈ Ring ∧ 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
119 47 53 59 118 syl3anc ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
120 eqid ( mulGrp ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) = ( mulGrp ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) )
121 eqid ( mulGrp ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) = ( mulGrp ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) )
122 120 121 rhmmhm ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) RingHom ( 𝑆s ( 𝐵m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( mulGrp ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) MndHom ( mulGrp ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ) )
123 19 24 122 3syl ( 𝜑 → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( mulGrp ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) MndHom ( mulGrp ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ) )
124 123 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( mulGrp ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) MndHom ( mulGrp ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ) )
125 120 25 mgpbas ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) = ( Base ‘ ( mulGrp ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
126 120 37 mgpplusg ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) = ( +g ‘ ( mulGrp ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
127 eqid ( .r ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) = ( .r ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) )
128 121 127 mgpplusg ( .r ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) = ( +g ‘ ( mulGrp ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) )
129 125 126 128 mhmlin ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( mulGrp ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) MndHom ( mulGrp ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ) ∧ 𝑖 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ 𝑗 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ( .r ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
130 124 53 59 129 syl3anc ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ( .r ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
131 23 26 68 69 71 72 3 127 pwsmulrval ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ( .r ‘ ( 𝑆s ( 𝐵m 𝐼 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f · ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
132 130 131 eqtrd ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f · ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
133 ovex ( 𝑓f · 𝑔 ) ∈ V
134 133 12 elab ( ( 𝑓f · 𝑔 ) ∈ { 𝑥𝜓 } ↔ 𝜎 )
135 oveq12 ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( 𝑓f · 𝑔 ) = ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f · ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) )
136 135 eleq1d ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( ( 𝑓f · 𝑔 ) ∈ { 𝑥𝜓 } ↔ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f · ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } ) )
137 134 136 bitr3id ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( 𝜎 ↔ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f · ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } ) )
138 103 137 imbi12d ( ( 𝑓 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∧ 𝑔 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) → ( ( ( 𝜑 ∧ ( ( 𝑓𝑄𝜏 ) ∧ ( 𝑔𝑄𝜂 ) ) ) → 𝜎 ) ↔ ( ( 𝜑 ∧ ( ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ∧ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f · ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } ) ) )
139 88 89 138 6 vtocl2 ( ( 𝜑 ∧ ( ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ { 𝑥𝜓 } ) ∧ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ 𝑄 ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ∈ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f · ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } )
140 75 81 87 139 syl12anc ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∘f · ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑗 ) ) ∈ { 𝑥𝜓 } )
141 132 140 eqeltrd ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) ∈ { 𝑥𝜓 } )
142 elpreima ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) → ( ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) ∈ { 𝑥𝜓 } ) ) )
143 29 142 syl ( 𝜑 → ( ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) ∈ { 𝑥𝜓 } ) ) )
144 143 adantr ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ) ∈ { 𝑥𝜓 } ) ) )
145 119 141 144 mpbir2and ( ( 𝜑 ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
146 145 adantlr ( ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) ∧ ( 𝑖 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ∧ 𝑗 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) ) → ( 𝑖 ( .r ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) 𝑗 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
147 21 mplassa ( ( 𝐼 ∈ V ∧ ( 𝑆s 𝑅 ) ∈ CRing ) → ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ∈ AssAlg )
148 39 43 147 syl2anc ( 𝜑 → ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ∈ AssAlg )
149 eqid ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) = ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) )
150 38 149 asclrhm ( ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ∈ AssAlg → ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∈ ( ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) RingHom ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
151 eqid ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
152 151 25 rhmf ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∈ ( ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) RingHom ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) → ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) : ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) ⟶ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
153 148 150 152 3syl ( 𝜑 → ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) : ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) ⟶ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
154 153 adantr ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) : ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) ⟶ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
155 21 39 43 mplsca ( 𝜑 → ( 𝑆s 𝑅 ) = ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
156 155 fveq2d ( 𝜑 → ( Base ‘ ( 𝑆s 𝑅 ) ) = ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) )
157 156 eleq2d ( 𝜑 → ( 𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ↔ 𝑖 ∈ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) ) )
158 157 biimpa ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → 𝑖 ∈ ( Base ‘ ( Scalar ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) )
159 154 158 ffvelcdmd ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
160 39 adantr ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → 𝐼 ∈ V )
161 40 adantr ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → 𝑆 ∈ CRing )
162 41 adantr ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
163 1 subrgss ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅𝐵 )
164 22 1 ressbas2 ( 𝑅𝐵𝑅 = ( Base ‘ ( 𝑆s 𝑅 ) ) )
165 41 163 164 3syl ( 𝜑𝑅 = ( Base ‘ ( 𝑆s 𝑅 ) ) )
166 165 eleq2d ( 𝜑 → ( 𝑖𝑅𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) )
167 166 biimpar ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → 𝑖𝑅 )
168 20 21 22 1 38 160 161 162 167 evlssca ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ) = ( ( 𝐵m 𝐼 ) × { 𝑖 } ) )
169 14 ralrimiva ( 𝜑 → ∀ 𝑓𝑅 𝜒 )
170 ovex ( 𝐵m 𝐼 ) ∈ V
171 vsnex { 𝑓 } ∈ V
172 170 171 xpex ( ( 𝐵m 𝐼 ) × { 𝑓 } ) ∈ V
173 172 7 elab ( ( ( 𝐵m 𝐼 ) × { 𝑓 } ) ∈ { 𝑥𝜓 } ↔ 𝜒 )
174 sneq ( 𝑓 = 𝑖 → { 𝑓 } = { 𝑖 } )
175 174 xpeq2d ( 𝑓 = 𝑖 → ( ( 𝐵m 𝐼 ) × { 𝑓 } ) = ( ( 𝐵m 𝐼 ) × { 𝑖 } ) )
176 175 eleq1d ( 𝑓 = 𝑖 → ( ( ( 𝐵m 𝐼 ) × { 𝑓 } ) ∈ { 𝑥𝜓 } ↔ ( ( 𝐵m 𝐼 ) × { 𝑖 } ) ∈ { 𝑥𝜓 } ) )
177 173 176 bitr3id ( 𝑓 = 𝑖 → ( 𝜒 ↔ ( ( 𝐵m 𝐼 ) × { 𝑖 } ) ∈ { 𝑥𝜓 } ) )
178 177 cbvralvw ( ∀ 𝑓𝑅 𝜒 ↔ ∀ 𝑖𝑅 ( ( 𝐵m 𝐼 ) × { 𝑖 } ) ∈ { 𝑥𝜓 } )
179 169 178 sylib ( 𝜑 → ∀ 𝑖𝑅 ( ( 𝐵m 𝐼 ) × { 𝑖 } ) ∈ { 𝑥𝜓 } )
180 179 r19.21bi ( ( 𝜑𝑖𝑅 ) → ( ( 𝐵m 𝐼 ) × { 𝑖 } ) ∈ { 𝑥𝜓 } )
181 167 180 syldan ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → ( ( 𝐵m 𝐼 ) × { 𝑖 } ) ∈ { 𝑥𝜓 } )
182 168 181 eqeltrd ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ) ∈ { 𝑥𝜓 } )
183 elpreima ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ) ∈ { 𝑥𝜓 } ) ) )
184 29 183 syl ( 𝜑 → ( ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ) ∈ { 𝑥𝜓 } ) ) )
185 184 adantr ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → ( ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ) ∈ { 𝑥𝜓 } ) ) )
186 159 182 185 mpbir2and ( ( 𝜑𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
187 186 adantlr ( ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) ∧ 𝑖 ∈ ( Base ‘ ( 𝑆s 𝑅 ) ) ) → ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
188 39 adantr ( ( 𝜑𝑖𝐼 ) → 𝐼 ∈ V )
189 45 adantr ( ( 𝜑𝑖𝐼 ) → ( 𝑆s 𝑅 ) ∈ Ring )
190 simpr ( ( 𝜑𝑖𝐼 ) → 𝑖𝐼 )
191 21 35 25 188 189 190 mvrcl ( ( 𝜑𝑖𝐼 ) → ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
192 40 adantr ( ( 𝜑𝑖𝐼 ) → 𝑆 ∈ CRing )
193 41 adantr ( ( 𝜑𝑖𝐼 ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
194 20 35 22 1 188 192 193 190 evlsvar ( ( 𝜑𝑖𝐼 ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ) = ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑖 ) ) )
195 170 mptex ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) ∈ V
196 195 8 elab ( ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) ∈ { 𝑥𝜓 } ↔ 𝜃 )
197 15 196 sylibr ( ( 𝜑𝑓𝐼 ) → ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) ∈ { 𝑥𝜓 } )
198 197 ralrimiva ( 𝜑 → ∀ 𝑓𝐼 ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) ∈ { 𝑥𝜓 } )
199 fveq2 ( 𝑓 = 𝑖 → ( 𝑔𝑓 ) = ( 𝑔𝑖 ) )
200 199 mpteq2dv ( 𝑓 = 𝑖 → ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) = ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑖 ) ) )
201 200 eleq1d ( 𝑓 = 𝑖 → ( ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) ∈ { 𝑥𝜓 } ↔ ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑖 ) ) ∈ { 𝑥𝜓 } ) )
202 201 cbvralvw ( ∀ 𝑓𝐼 ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑓 ) ) ∈ { 𝑥𝜓 } ↔ ∀ 𝑖𝐼 ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑖 ) ) ∈ { 𝑥𝜓 } )
203 198 202 sylib ( 𝜑 → ∀ 𝑖𝐼 ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑖 ) ) ∈ { 𝑥𝜓 } )
204 203 r19.21bi ( ( 𝜑𝑖𝐼 ) → ( 𝑔 ∈ ( 𝐵m 𝐼 ) ↦ ( 𝑔𝑖 ) ) ∈ { 𝑥𝜓 } )
205 194 204 eqeltrd ( ( 𝜑𝑖𝐼 ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ) ∈ { 𝑥𝜓 } )
206 elpreima ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) → ( ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ) ∈ { 𝑥𝜓 } ) ) )
207 29 206 syl ( 𝜑 → ( ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ) ∈ { 𝑥𝜓 } ) ) )
208 207 adantr ( ( 𝜑𝑖𝐼 ) → ( ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ↔ ( ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ∧ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ) ∈ { 𝑥𝜓 } ) ) )
209 191 205 208 mpbir2and ( ( 𝜑𝑖𝐼 ) → ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
210 209 adantlr ( ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) ∧ 𝑖𝐼 ) → ( ( 𝐼 mVar ( 𝑆s 𝑅 ) ) ‘ 𝑖 ) ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
211 simpr ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) )
212 39 adantr ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → 𝐼 ∈ V )
213 43 adantr ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( 𝑆s 𝑅 ) ∈ CRing )
214 34 35 21 36 37 38 25 117 146 187 210 211 212 213 mplind ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → 𝑦 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) )
215 fvimacnvi ( ( Fun ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∧ 𝑦 ∈ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥𝜓 } ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) ∈ { 𝑥𝜓 } )
216 33 214 215 syl2an2r ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) ∈ { 𝑥𝜓 } )
217 eleq1 ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) = 𝐴 → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) ∈ { 𝑥𝜓 } ↔ 𝐴 ∈ { 𝑥𝜓 } ) )
218 216 217 syl5ibcom ( ( 𝜑𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ) → ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) = 𝐴𝐴 ∈ { 𝑥𝜓 } ) )
219 218 rexlimdva ( 𝜑 → ( ∃ 𝑦 ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆s 𝑅 ) ) ) ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑦 ) = 𝐴𝐴 ∈ { 𝑥𝜓 } ) )
220 32 219 mpd ( 𝜑𝐴 ∈ { 𝑥𝜓 } )
221 13 elabg ( 𝐴𝑄 → ( 𝐴 ∈ { 𝑥𝜓 } ↔ 𝜌 ) )
222 16 221 syl ( 𝜑 → ( 𝐴 ∈ { 𝑥𝜓 } ↔ 𝜌 ) )
223 220 222 mpbid ( 𝜑𝜌 )