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	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ◡ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥 ∣ 𝜓 } ) ∧ 𝑗 ∈ ( ◡ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ { 𝑥 ∣ 𝜓 } ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ 𝑖 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) )
73	71 60	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( ◡ ( ( 𝐼 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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 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		vsnex	⊢ { 𝑓 } ∈ 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	⊢ ( 𝜑 → 𝜌 )