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		1oex	$⊢ 1_{𝑜} \in V$
30	29	a1i	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 1_{𝑜} \in V$
31		simpr	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n \in ({ℕ_{0}}^{1_{𝑜}})$
32	30 25 31	elmaprd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n : 1_{𝑜} ⟶ ℕ_{0}$
33		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
34	33	a1i	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in 1_{𝑜}$
35	32 34	ffvelcdmd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n (\emptyset) \in ℕ_{0}$
36	28 35	fsnd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
37	25 27 36	elmapdd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
38		c0ex	$⊢ 0 \in V$
39	38	a1i	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 0 \in V$
40		snopfsupp	$⊢ (X \in I \land n (\emptyset) \in ℕ_{0} \land 0 \in V) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
41	28 35 39 40	syl3anc	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
42	23 37 41	elrabd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
43	22 42	ffvelcdmd	$⊢ ((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\}) \in {Base}_{U}$
44	43	fmpttd	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) : {ℕ_{0}}^{1_{𝑜}} ⟶ {Base}_{U}$
45	9 10 44	elmapdd	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) \in ({Base}_{U}^{({ℕ_{0}}^{1_{𝑜}})})$
46		eqid	$⊢ 1_{𝑜} mPwSer U = 1_{𝑜} mPwSer U$
47		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{h \in ({ℕ_{0}}^{1_{𝑜}}) \| h^{-1} [ℕ] \in Fin\}$
48		eqid	$⊢ {Base}_{(1_{𝑜} mPwSer U)} = {Base}_{(1_{𝑜} mPwSer U)}$
49	29	a1i	$⊢ (φ \land f \in B) \to 1_{𝑜} \in V$
50	46 12 47 48 49	psrbas	$⊢ (φ \land f \in B) \to {Base}_{(1_{𝑜} mPwSer U)} = {Base}_{U}^{({ℕ_{0}}^{1_{𝑜}})}$
51	45 50	eleqtrrd	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) \in {Base}_{(1_{𝑜} mPwSer U)}$
52	21 42	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)⟩\}))$
53		eqid	$⊢ 0_{U} = 0_{U}$
54	11 13 53 20	mplelsfi	$⊢ (φ \land f \in B) \to {finSupp}_{0_{U}} ((I selectVars R) (\{X\}) (f))$
55	37	ralrimiva	$⊢ (φ \land f \in B) \to \forall n \in ({ℕ_{0}}^{1_{𝑜}}) \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
56	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$
57		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$
58		opex	$⊢ ⟨X, n (\emptyset)⟩ \in V$
59	58	sneqr	$⊢ \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
60	59	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)⟩$
61		opthg	$⊢ (X \in I \land n (\emptyset) \in V) \to (⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩ \leftrightarrow (X = X \land n (\emptyset) = m (\emptyset)))$
62	61	simplbda	$⊢ ((X \in I \land n (\emptyset) \in V) \land ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩) \to n (\emptyset) = m (\emptyset)$
63	56 57 60 62	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)$
64		0ex	$⊢ \emptyset \in V$
65	64	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$
66		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
67	32	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}$
68	67	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_{𝑜}$
69	29	a1i	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to 1_{𝑜} \in V$
70	24	a1i	$⊢ ((((φ \land f \in B) \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to ℕ_{0} \in V$
71		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_{𝑜}})$
72	69 70 71	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}$
73	72	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_{𝑜}$
74	65 66 68 73	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))$
75	63 74	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$
76	75	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)$
77	76	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)$
78	77	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)$
79		eqid	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\})$
80		fveq1	$⊢ n = m \to n (\emptyset) = m (\emptyset)$
81	80	opeq2d	$⊢ n = m \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
82	81	sneqd	$⊢ n = m \to \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}$
83	79 82	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))$
84	55 78 83	sylanbrc	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1}{⟶} {ℕ_{0}}^{\{X\}}$
85		fvexd	$⊢ (φ \land f \in B) \to 0_{U} \in V$
86	54 84 85 20	fsuppco	$⊢ (φ \land f \in B) \to {finSupp}_{0_{U}} (((I selectVars R) (\{X\}) (f) \circ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\})))$
87	52 86	eqbrtrrd	$⊢ (φ \land f \in B) \to {finSupp}_{0_{U}} ((n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})))$
88		eqid	$⊢ 1_{𝑜} mPoly U = 1_{𝑜} mPoly U$
89		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
90	4 89	ply1bas	$⊢ {Base}_{Q} = {Base}_{(1_{𝑜} mPoly U)}$
91	88 46 48 53 90	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)⟩\}))))$
92	51 87 91	sylanbrc	$⊢ (φ \land f \in B) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) \in {Base}_{Q}$
93	92 5	fmptd	$⊢ φ \to H : B ⟶ {Base}_{Q}$

Metamath Proof Explorer

Theorem selvply1rhmlem1

Proof