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	$⊢ B = {Base}_{S}$
	mpfind.cp	$⊢ \underset{˙}{+} = +_{S}$
	mpfind.ct	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
	mpfind.cq	$⊢ Q = ran (I evalSub S) (R)$
	mpfind.ad	$⊢ (φ \land ((f \in Q \land τ) \land (g \in Q \land η))) \to ζ$
	mpfind.mu	$⊢ (φ \land ((f \in Q \land τ) \land (g \in Q \land η))) \to σ$
	mpfind.wa	$⊢ x = (B^{I}) \times \{f\} \to (ψ \leftrightarrow χ)$
	mpfind.wb	$⊢ x = (g \in (B^{I}) ⟼ g (f)) \to (ψ \leftrightarrow θ)$
	mpfind.wc	$⊢ x = f \to (ψ \leftrightarrow τ)$
	mpfind.wd	$⊢ x = g \to (ψ \leftrightarrow η)$
	mpfind.we	$⊢ x = f {\underset{˙}{+}}_{f} g \to (ψ \leftrightarrow ζ)$
	mpfind.wf	$⊢ x = f {\underset{˙}{\cdot}}_{f} g \to (ψ \leftrightarrow σ)$
	mpfind.wg	$⊢ x = A \to (ψ \leftrightarrow ρ)$
	mpfind.co	$⊢ (φ \land f \in R) \to χ$
	mpfind.pr	$⊢ (φ \land f \in I) \to θ$
	mpfind.a	$⊢ φ \to A \in Q$
Assertion	mpfind	$⊢ φ \to ρ$

Proof

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

Metamath Proof Explorer

Theorem mpfind

Proof