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