This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝜌 )