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	mplring	$⊢ (I \in V \land S ↾_{𝑠} R \in Ring) \to I mPoly (S ↾_{𝑠} R) \in Ring$
47	39 45 46	syl2anc	$⊢ φ \to I mPoly (S ↾_{𝑠} R) \in Ring$
48	47	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$
49		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 \| ψ\}]$
50		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 \| ψ\}))$
51	29 50	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 \| ψ\}))$
52	51	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 \| ψ\}))$
53	49 52	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 \| ψ\})$
54	53	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))}$
55		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 \| ψ\}]$
56		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 \| ψ\}))$
57	29 56	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 \| ψ\}))$
58	57	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 \| ψ\}))$
59	55 58	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 \| ψ\})$
60	59	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))}$
61	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))}$
62	48 54 60 61	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))}$
63		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})))$
64	19 24 63	3syl	$⊢ φ \to (I evalSub S) (R) \in ((I mPoly (S ↾_{𝑠} R)) GrpHom (S ↑_{𝑠} (B^{I})))$
65	64	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})))$
66		eqid	$⊢ +_{(S ↑_{𝑠} (B^{I}))} = +_{(S ↑_{𝑠} (B^{I}))}$
67	25 36 66	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)$
68	65 54 60 67	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)$
69	40	adantr	$⊢ (φ \land (i \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}] \land j \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}])) \to S \in CRing$
70		ovexd	$⊢ (φ \land (i \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}] \land j \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}])) \to B^{I} \in V$
71	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}))}$
72	71 54	ffvelrnd	$⊢ (φ \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}))}$
73	71 60	ffvelrnd	$⊢ (φ \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}))}$
74	23 26 69 70 72 73 2 66	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)$
75	68 74	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)$
76		simpl	$⊢ (φ \land (i \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}] \land j \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}])) \to φ$
77		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)$
78	29 54 77	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)$
79	78 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$
80		fvimacnvi	$⊢ (Fun (I evalSub S) (R) \land i \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}]) \to (I evalSub S) (R) (i) \in \{x \| ψ\}$
81	33 49 80	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 \| ψ\}$
82	79 81	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 \| ψ\})$
83		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)$
84	29 60 83	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)$
85	84 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$
86		fvimacnvi	$⊢ (Fun (I evalSub S) (R) \land j \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}]) \to (I evalSub S) (R) (j) \in \{x \| ψ\}$
87	33 55 86	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 \| ψ\}$
88	85 87	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 \| ψ\})$
89		fvex	$⊢ (I evalSub S) (R) (i) \in V$
90		fvex	$⊢ (I evalSub S) (R) (j) \in V$
91		eleq1	$⊢ f = (I evalSub S) (R) (i) \to (f \in Q \leftrightarrow (I evalSub S) (R) (i) \in Q)$
92		vex	$⊢ f \in V$
93	92 9	elab	$⊢ f \in \{x \| ψ\} \leftrightarrow τ$
94		eleq1	$⊢ f = (I evalSub S) (R) (i) \to (f \in \{x \| ψ\} \leftrightarrow (I evalSub S) (R) (i) \in \{x \| ψ\})$
95	93 94	syl5bbr	$⊢ f = (I evalSub S) (R) (i) \to (τ \leftrightarrow (I evalSub S) (R) (i) \in \{x \| ψ\})$
96	91 95	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 \| ψ\}))$
97		eleq1	$⊢ g = (I evalSub S) (R) (j) \to (g \in Q \leftrightarrow (I evalSub S) (R) (j) \in Q)$
98		vex	$⊢ g \in V$
99	98 10	elab	$⊢ g \in \{x \| ψ\} \leftrightarrow η$
100		eleq1	$⊢ g = (I evalSub S) (R) (j) \to (g \in \{x \| ψ\} \leftrightarrow (I evalSub S) (R) (j) \in \{x \| ψ\})$
101	99 100	syl5bbr	$⊢ g = (I evalSub S) (R) (j) \to (η \leftrightarrow (I evalSub S) (R) (j) \in \{x \| ψ\})$
102	97 101	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 \| ψ\}))$
103	96 102	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 \| ψ\})))$
104	103	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 \| ψ\}))))$
105		ovex	$⊢ f {\underset{˙}{+}}_{f} g \in V$
106	105 11	elab	$⊢ f {\underset{˙}{+}}_{f} g \in \{x \| ψ\} \leftrightarrow ζ$
107		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)$
108	107	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 \| ψ\})$
109	106 108	syl5bbr	$⊢ (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 \| ψ\})$
110	104 109	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 \| ψ\}))$
111	89 90 110 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 \| ψ\}$
112	76 82 88 111	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 \| ψ\}$
113	75 112	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 \| ψ\}$
114		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 \| ψ\}))$
115	29 114	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 \| ψ\}))$
116	115	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 \| ψ\}))$
117	62 113 116	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 \| ψ\}]$
118	117	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 \| ψ\}]$
119	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))}$
120	48 54 60 119	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))}$
121		eqid	$⊢ {mulGrp}_{(I mPoly (S ↾_{𝑠} R))} = {mulGrp}_{(I mPoly (S ↾_{𝑠} R))}$
122		eqid	$⊢ {mulGrp}_{(S ↑_{𝑠} (B^{I}))} = {mulGrp}_{(S ↑_{𝑠} (B^{I}))}$
123	121 122	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}))})$
124	19 24 123	3syl	$⊢ φ \to (I evalSub S) (R) \in ({mulGrp}_{(I mPoly (S ↾_{𝑠} R))} MndHom {mulGrp}_{(S ↑_{𝑠} (B^{I}))})$
125	124	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}))})$
126	121 25	mgpbas	$⊢ {Base}_{(I mPoly (S ↾_{𝑠} R))} = {Base}_{{mulGrp}_{(I mPoly (S ↾_{𝑠} R))}}$
127	121 37	mgpplusg	$⊢ \cdot_{(I mPoly (S ↾_{𝑠} R))} = +_{{mulGrp}_{(I mPoly (S ↾_{𝑠} R))}}$
128		eqid	$⊢ \cdot_{(S ↑_{𝑠} (B^{I}))} = \cdot_{(S ↑_{𝑠} (B^{I}))}$
129	122 128	mgpplusg	$⊢ \cdot_{(S ↑_{𝑠} (B^{I}))} = +_{{mulGrp}_{(S ↑_{𝑠} (B^{I}))}}$
130	126 127 129	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)$
131	125 54 60 130	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)$
132	23 26 69 70 72 73 3 128	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)$
133	131 132	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)$
134		ovex	$⊢ f {\underset{˙}{\cdot}}_{f} g \in V$
135	134 12	elab	$⊢ f {\underset{˙}{\cdot}}_{f} g \in \{x \| ψ\} \leftrightarrow σ$
136		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)$
137	136	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 \| ψ\})$
138	135 137	syl5bbr	$⊢ (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 \| ψ\})$
139	104 138	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 \| ψ\}))$
140	89 90 139 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 \| ψ\}$
141	76 82 88 140	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 \| ψ\}$
142	133 141	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 \| ψ\}$
143		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 \| ψ\}))$
144	29 143	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 \| ψ\}))$
145	144	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 \| ψ\}))$
146	120 142 145	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 \| ψ\}]$
147	146	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 \| ψ\}]$
148	21	mplassa	$⊢ (I \in V \land S ↾_{𝑠} R \in CRing) \to I mPoly (S ↾_{𝑠} R) \in AssAlg$
149	39 43 148	syl2anc	$⊢ φ \to I mPoly (S ↾_{𝑠} R) \in AssAlg$
150		eqid	$⊢ Scalar (I mPoly (S ↾_{𝑠} R)) = Scalar (I mPoly (S ↾_{𝑠} R))$
151	38 150	asclrhm	$⊢ I mPoly (S ↾_{𝑠} R) \in AssAlg \to algSc (I mPoly (S ↾_{𝑠} R)) \in (Scalar (I mPoly (S ↾_{𝑠} R)) RingHom (I mPoly (S ↾_{𝑠} R)))$
152		eqid	$⊢ {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))} = {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))}$
153	152 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))}$
154	149 151 153	3syl	$⊢ φ \to algSc (I mPoly (S ↾_{𝑠} R)) : {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(I mPoly (S ↾_{𝑠} R))}$
155	154	adantr	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to algSc (I mPoly (S ↾_{𝑠} R)) : {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))} ⟶ {Base}_{(I mPoly (S ↾_{𝑠} R))}$
156	21 39 43	mplsca	$⊢ φ \to S ↾_{𝑠} R = Scalar (I mPoly (S ↾_{𝑠} R))$
157	156	fveq2d	$⊢ φ \to {Base}_{(S ↾_{𝑠} R)} = {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))}$
158	157	eleq2d	$⊢ φ \to (i \in {Base}_{(S ↾_{𝑠} R)} \leftrightarrow i \in {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))})$
159	158	biimpa	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to i \in {Base}_{Scalar (I mPoly (S ↾_{𝑠} R))}$
160	155 159	ffvelrnd	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to algSc (I mPoly (S ↾_{𝑠} R)) (i) \in {Base}_{(I mPoly (S ↾_{𝑠} R))}$
161	39	adantr	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to I \in V$
162	40	adantr	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to S \in CRing$
163	41	adantr	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to R \in SubRing (S)$
164	1	subrgss	$⊢ R \in SubRing (S) \to R \subseteq B$
165	22 1	ressbas2	$⊢ R \subseteq B \to R = {Base}_{(S ↾_{𝑠} R)}$
166	41 164 165	3syl	$⊢ φ \to R = {Base}_{(S ↾_{𝑠} R)}$
167	166	eleq2d	$⊢ φ \to (i \in R \leftrightarrow i \in {Base}_{(S ↾_{𝑠} R)})$
168	167	biimpar	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to i \in R$
169	20 21 22 1 38 161 162 163 168	evlssca	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to (I evalSub S) (R) (algSc (I mPoly (S ↾_{𝑠} R)) (i)) = (B^{I}) \times \{i\}$
170	14	ralrimiva	$⊢ φ \to \forall f \in R χ$
171		ovex	$⊢ B^{I} \in V$
172		snex	$⊢ \{f\} \in V$
173	171 172	xpex	$⊢ (B^{I}) \times \{f\} \in V$
174	173 7	elab	$⊢ (B^{I}) \times \{f\} \in \{x \| ψ\} \leftrightarrow χ$
175		sneq	$⊢ f = i \to \{f\} = \{i\}$
176	175	xpeq2d	$⊢ f = i \to (B^{I}) \times \{f\} = (B^{I}) \times \{i\}$
177	176	eleq1d	$⊢ f = i \to ((B^{I}) \times \{f\} \in \{x \| ψ\} \leftrightarrow (B^{I}) \times \{i\} \in \{x \| ψ\})$
178	174 177	syl5bbr	$⊢ f = i \to (χ \leftrightarrow (B^{I}) \times \{i\} \in \{x \| ψ\})$
179	178	cbvralvw	$⊢ \forall f \in R χ \leftrightarrow \forall i \in R (B^{I}) \times \{i\} \in \{x \| ψ\}$
180	170 179	sylib	$⊢ φ \to \forall i \in R (B^{I}) \times \{i\} \in \{x \| ψ\}$
181	180	r19.21bi	$⊢ (φ \land i \in R) \to (B^{I}) \times \{i\} \in \{x \| ψ\}$
182	168 181	syldan	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to (B^{I}) \times \{i\} \in \{x \| ψ\}$
183	169 182	eqeltrd	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to (I evalSub S) (R) (algSc (I mPoly (S ↾_{𝑠} R)) (i)) \in \{x \| ψ\}$
184		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 \| ψ\}))$
185	29 184	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 \| ψ\}))$
186	185	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 \| ψ\}))$
187	160 183 186	mpbir2and	$⊢ (φ \land i \in {Base}_{(S ↾_{𝑠} R)}) \to algSc (I mPoly (S ↾_{𝑠} R)) (i) \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}]$
188	187	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 \| ψ\}]$
189	39	adantr	$⊢ (φ \land i \in I) \to I \in V$
190	45	adantr	$⊢ (φ \land i \in I) \to S ↾_{𝑠} R \in Ring$
191		simpr	$⊢ (φ \land i \in I) \to i \in I$
192	21 35 25 189 190 191	mvrcl	$⊢ (φ \land i \in I) \to (I mVar (S ↾_{𝑠} R)) (i) \in {Base}_{(I mPoly (S ↾_{𝑠} R))}$
193	40	adantr	$⊢ (φ \land i \in I) \to S \in CRing$
194	41	adantr	$⊢ (φ \land i \in I) \to R \in SubRing (S)$
195	20 35 22 1 189 193 194 191	evlsvar	$⊢ (φ \land i \in I) \to (I evalSub S) (R) ((I mVar (S ↾_{𝑠} R)) (i)) = (g \in (B^{I}) ⟼ g (i))$
196	171	mptex	$⊢ (g \in (B^{I}) ⟼ g (f)) \in V$
197	196 8	elab	$⊢ (g \in (B^{I}) ⟼ g (f)) \in \{x \| ψ\} \leftrightarrow θ$
198	15 197	sylibr	$⊢ (φ \land f \in I) \to (g \in (B^{I}) ⟼ g (f)) \in \{x \| ψ\}$
199	198	ralrimiva	$⊢ φ \to \forall f \in I (g \in (B^{I}) ⟼ g (f)) \in \{x \| ψ\}$
200		fveq2	$⊢ f = i \to g (f) = g (i)$
201	200	mpteq2dv	$⊢ f = i \to (g \in (B^{I}) ⟼ g (f)) = (g \in (B^{I}) ⟼ g (i))$
202	201	eleq1d	$⊢ f = i \to ((g \in (B^{I}) ⟼ g (f)) \in \{x \| ψ\} \leftrightarrow (g \in (B^{I}) ⟼ g (i)) \in \{x \| ψ\})$
203	202	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 \| ψ\}$
204	199 203	sylib	$⊢ φ \to \forall i \in I (g \in (B^{I}) ⟼ g (i)) \in \{x \| ψ\}$
205	204	r19.21bi	$⊢ (φ \land i \in I) \to (g \in (B^{I}) ⟼ g (i)) \in \{x \| ψ\}$
206	195 205	eqeltrd	$⊢ (φ \land i \in I) \to (I evalSub S) (R) ((I mVar (S ↾_{𝑠} R)) (i)) \in \{x \| ψ\}$
207		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 \| ψ\}))$
208	29 207	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 \| ψ\}))$
209	208	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 \| ψ\}))$
210	192 206 209	mpbir2and	$⊢ (φ \land i \in I) \to (I mVar (S ↾_{𝑠} R)) (i) \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}]$
211	210	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 \| ψ\}]$
212		simpr	$⊢ (φ \land y \in {Base}_{(I mPoly (S ↾_{𝑠} R))}) \to y \in {Base}_{(I mPoly (S ↾_{𝑠} R))}$
213	39	adantr	$⊢ (φ \land y \in {Base}_{(I mPoly (S ↾_{𝑠} R))}) \to I \in V$
214	43	adantr	$⊢ (φ \land y \in {Base}_{(I mPoly (S ↾_{𝑠} R))}) \to S ↾_{𝑠} R \in CRing$
215	34 35 21 36 37 38 25 118 147 188 211 212 213 214	mplind	$⊢ (φ \land y \in {Base}_{(I mPoly (S ↾_{𝑠} R))}) \to y \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}]$
216		fvimacnvi	$⊢ (Fun (I evalSub S) (R) \land y \in {(I evalSub S) (R)}^{-1} [\{x \| ψ\}]) \to (I evalSub S) (R) (y) \in \{x \| ψ\}$
217	33 215 216	syl2an2r	$⊢ (φ \land y \in {Base}_{(I mPoly (S ↾_{𝑠} R))}) \to (I evalSub S) (R) (y) \in \{x \| ψ\}$
218		eleq1	$⊢ (I evalSub S) (R) (y) = A \to ((I evalSub S) (R) (y) \in \{x \| ψ\} \leftrightarrow A \in \{x \| ψ\})$
219	217 218	syl5ibcom	$⊢ (φ \land y \in {Base}_{(I mPoly (S ↾_{𝑠} R))}) \to ((I evalSub S) (R) (y) = A \to A \in \{x \| ψ\})$
220	219	rexlimdva	$⊢ φ \to (\exists y \in {Base}_{(I mPoly (S ↾_{𝑠} R))} (I evalSub S) (R) (y) = A \to A \in \{x \| ψ\})$
221	32 220	mpd	$⊢ φ \to A \in \{x \| ψ\}$
222	13	elabg	$⊢ A \in Q \to (A \in \{x \| ψ\} \leftrightarrow ρ)$
223	16 222	syl	$⊢ φ \to (A \in \{x \| ψ\} \leftrightarrow ρ)$
224	221 223	mpbid	$⊢ φ \to ρ$

Metamath Proof Explorer

Theorem mpfind

Proof