selvply1rhmlem1

	Ref	Expression
Hypotheses	selvply1rhm.1	$⊢ B = {Base}_{P}$
	selvply1rhm.2	$⊢ P = I mPoly R$
	selvply1rhm.3	$⊢ U = (I ∖ \{X\}) mPoly R$
	selvply1rhm.4	$⊢ Q = {Poly}_{1} (U)$
	selvply1rhm.5	$⊢ H = (f \in B ⟼ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})))$
	selvply1rhm.6	$⊢ φ \to I \in V$
	selvply1rhm.7	$⊢ φ \to X \in I$
	selvply1rhm.8	$⊢ φ \to R \in CRing$
Assertion	selvply1rhmlem1	$⊢ φ \to H : B ⟶ {Base}_{Q}$

Proof

Step	Hyp	Ref	Expression
1		selvply1rhm.1	$⊢ B = {Base}_{P}$
2		selvply1rhm.2	$⊢ P = I mPoly R$
3		selvply1rhm.3	$⊢ U = (I ∖ \{X\}) mPoly R$
4		selvply1rhm.4	$⊢ Q = {Poly}_{1} (U)$
5		selvply1rhm.5	$⊢ H = (f \in B ⟼ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})))$
6		selvply1rhm.6	$⊢ φ \to I \in V$
7		selvply1rhm.7	$⊢ φ \to X \in I$
8		selvply1rhm.8	$⊢ φ \to R \in CRing$
9		fvexd	$⊢ (φ \land f \in B) \to {Base}_{U} \in V$
10		ovexd	$⊢ (φ \land f \in B) \to {ℕ_{0}}^{1_{𝑜}} \in V$
11		eqid	$⊢ \{X\} mPoly U = \{X\} mPoly U$
12		eqid	$⊢ {Base}_{U} = {Base}_{U}$
13		eqid	$⊢ {Base}_{(\{X\} mPoly U)} = {Base}_{(\{X\} mPoly U)}$
14		eqid	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
15	14	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\}$
16	8	adantr	$⊢ (φ \land f \in B) \to R \in CRing$
17	7	snssd	$⊢ φ \to \{X\} \subseteq I$
18	17	adantr	$⊢ (φ \land f \in B) \to \{X\} \subseteq I$
19		simpr	$⊢ (φ \land f \in B) \to f \in B$
20	2 1 3 11 13 16 18 19	selvcl	$⊢ (φ \land f \in B) \to (I selectVars R) (\{X\}) (f) \in {Base}_{(\{X\} mPoly U)}$
21	11 12 13 15 20	mplelf	$⊢ (φ \land f \in B) \to (I selectVars R) (\{X\}) (f) : \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{U}$
22	21	adantr	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (I selectVars R) (\{X\}) (f) : \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{U}$
23		breq1	$⊢ h = \{⟨X, n (\emptyset)⟩\} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\}))$
24		nn0ex	$⊢ ℕ_{0} \in V$
25	24	a1i	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to ℕ_{0} \in V$
26		snex	$⊢ \{X\} \in V$
27	26	a1i	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in V$
28	7	ad2antrr	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to X \in I$
29		simpr	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n \in ({ℕ_{0}}^{1_{𝑜}})$
30	29	elmaprd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n : 1_{𝑜} ⟶ ℕ_{0}$
31		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
32	31	a1i	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in 1_{𝑜}$
33	30 32	ffvelcdmd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n (\emptyset) \in ℕ_{0}$
34	28 33	fsnd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
35	25 27 34	elmapdd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
36		c0ex	$⊢ 0 \in V$
37	36	a1i	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 0 \in V$
38		snopfsupp	$⊢ (X \in I \land n (\emptyset) \in ℕ_{0} \land 0 \in V) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
39	28 33 37 38	syl3anc	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
40	23 35 39	elrabd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
41	22 40	ffvelcdmd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\}) \in {Base}_{U}$
42	41	fmpttd	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) : {ℕ_{0}}^{1_{𝑜}} ⟶ {Base}_{U}$
43	9 10 42	elmapdd	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) \in ({Base}_{U}^{({ℕ_{0}}^{1_{𝑜}})})$
44		eqid	$⊢ 1_{𝑜} mPwSer U = 1_{𝑜} mPwSer U$
45		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{h \in ({ℕ_{0}}^{1_{𝑜}}) \| h^{-1} [ℕ] \in Fin\}$
46		eqid	$⊢ {Base}_{(1_{𝑜} mPwSer U)} = {Base}_{(1_{𝑜} mPwSer U)}$
47		1oex	$⊢ 1_{𝑜} \in V$
48	47	a1i	$⊢ (φ \land f \in B) \to 1_{𝑜} \in V$
49	44 12 45 46 48	psrbas	$⊢ (φ \land f \in B) \to {Base}_{(1_{𝑜} mPwSer U)} = {Base}_{U}^{({ℕ_{0}}^{1_{𝑜}})}$
50	43 49	eleqtrrd	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) \in {Base}_{(1_{𝑜} mPwSer U)}$
51	21 40	cofmpt	$⊢ (φ \land f \in B) \to (I selectVars R) (\{X\}) (f) \circ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\}))$
52		eqid	$⊢ 0_{U} = 0_{U}$
53	11 13 52 20	mplelsfi	$⊢ (φ \land f \in B) \to {finSupp}_{0_{U}} ((I selectVars R) (\{X\}) (f))$
54	35	ralrimiva	$⊢ (φ \land f \in B) \to \forall n \in ({ℕ_{0}}^{1_{𝑜}}) \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
55	28	ad2antrr	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to X \in I$
56		fvexd	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n (\emptyset) \in V$
57		opex	$⊢ ⟨X, n (\emptyset)⟩ \in V$
58	57	sneqr	$⊢ \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
59	58	adantl	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
60		opthg	$⊢ (X \in I \land n (\emptyset) \in V) \to (⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩ \leftrightarrow (X = X \land n (\emptyset) = m (\emptyset)))$
61	60	simplbda	$⊢ ((X \in I \land n (\emptyset) \in V) \land ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩) \to n (\emptyset) = m (\emptyset)$
62	55 56 59 61	syl21anc	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n (\emptyset) = m (\emptyset)$
63		0ex	$⊢ \emptyset \in V$
64	63	a1i	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to \emptyset \in V$
65		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
66	30	ad2antrr	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n : 1_{𝑜} ⟶ ℕ_{0}$
67	66	ffnd	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n Fn 1_{𝑜}$
68		simplr	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to m \in ({ℕ_{0}}^{1_{𝑜}})$
69	68	elmaprd	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to m : 1_{𝑜} ⟶ ℕ_{0}$
70	69	ffnd	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to m Fn 1_{𝑜}$
71	64 65 67 70	fsneq	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to (n = m \leftrightarrow n (\emptyset) = m (\emptyset))$
72	62 71	mpbird	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n = m$
73	72	ex	$⊢ (((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to n = m)$
74	73	anasss	$⊢ ((φ \land f \in B) \land (n \in ({ℕ_{0}}^{1_{𝑜}}) \land m \in ({ℕ_{0}}^{1_{𝑜}}))) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to n = m)$
75	74	ralrimivva	$⊢ (φ \land f \in B) \to \forall n \in ({ℕ_{0}}^{1_{𝑜}}) \forall m \in ({ℕ_{0}}^{1_{𝑜}}) (\{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to n = m)$
76		eqid	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\})$
77		fveq1	$⊢ n = m \to n (\emptyset) = m (\emptyset)$
78	77	opeq2d	$⊢ n = m \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
79	78	sneqd	$⊢ n = m \to \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}$
80	76 79	f1mpt	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1}{⟶} {ℕ_{0}}^{\{X\}} \leftrightarrow (\forall n \in ({ℕ_{0}}^{1_{𝑜}}) \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}}) \land \forall n \in ({ℕ_{0}}^{1_{𝑜}}) \forall m \in ({ℕ_{0}}^{1_{𝑜}}) (\{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to n = m))$
81	54 75 80	sylanbrc	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1}{⟶} {ℕ_{0}}^{\{X\}}$
82		fvexd	$⊢ (φ \land f \in B) \to 0_{U} \in V$
83	53 81 82 20	fsuppco	$⊢ (φ \land f \in B) \to {finSupp}_{0_{U}} (((I selectVars R) (\{X\}) (f) \circ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\})))$
84	51 83	eqbrtrrd	$⊢ (φ \land f \in B) \to {finSupp}_{0_{U}} ((n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})))$
85		eqid	$⊢ 1_{𝑜} mPoly U = 1_{𝑜} mPoly U$
86		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
87	4 86	ply1bas	$⊢ {Base}_{Q} = {Base}_{(1_{𝑜} mPoly U)}$
88	85 44 46 52 87	mplelbas	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) \in {Base}_{Q} \leftrightarrow ((n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) \in {Base}_{(1_{𝑜} mPwSer U)} \land {finSupp}_{0_{U}} ((n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\}))))$
89	50 84 88	sylanbrc	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) \in {Base}_{Q}$
90	89 5	fmptd	$⊢ φ \to H : B ⟶ {Base}_{Q}$

Metamath Proof Explorer

Theorem selvply1rhmlem1

Proof