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