selvply1rhmlem2

Description: Lemma for selvply1rhm : Image of the ring unit by the mapping H (Contributed by Thierry Arnoux, 4-May-2026)

	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	selvply1rhmlem2	$⊢ φ \to H (1_{P}) = 1_{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		fveq2	$⊢ f = 1_{P} \to (I selectVars R) (\{X\}) (f) = (I selectVars R) (\{X\}) (1_{P})$
10	9	fveq1d	$⊢ f = 1_{P} \to (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\}) = (I selectVars R) (\{X\}) (1_{P}) (\{⟨X, n (\emptyset)⟩\})$
11	10	mpteq2dv	$⊢ f = 1_{P} \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (1_{P}) (\{⟨X, n (\emptyset)⟩\}))$
12		eqid	$⊢ algSc (P) = algSc (P)$
13		eqid	$⊢ 1_{R} = 1_{R}$
14		eqid	$⊢ 1_{P} = 1_{P}$
15	8	crngringd	$⊢ φ \to R \in Ring$
16	2 12 13 14 6 15	mplascl1	$⊢ φ \to algSc (P) (1_{R}) = 1_{P}$
17	16	fveq2d	$⊢ φ \to (I selectVars R) (\{X\}) (algSc (P) (1_{R})) = (I selectVars R) (\{X\}) (1_{P})$
18		eqid	$⊢ {Base}_{R} = {Base}_{R}$
19		eqid	$⊢ algSc (\{X\} mPoly U) = algSc (\{X\} mPoly U)$
20	18 13 15	ringidcld	$⊢ φ \to 1_{R} \in {Base}_{R}$
21		eqid	$⊢ \{X\} mPoly U = \{X\} mPoly U$
22		eqid	$⊢ algSc (\{X\} mPoly U) \circ algSc (U) = algSc (\{X\} mPoly U) \circ algSc (U)$
23	7	snssd	$⊢ φ \to \{X\} \subseteq I$
24	18 2 12 19 6 20 3 21 22 8 23	selvascl	$⊢ φ \to (I selectVars R) (\{X\}) (algSc (P) (1_{R})) = (algSc (\{X\} mPoly U) \circ algSc (U)) (1_{R})$
25	17 24	eqtr3d	$⊢ φ \to (I selectVars R) (\{X\}) (1_{P}) = (algSc (\{X\} mPoly U) \circ algSc (U)) (1_{R})$
26	25	fveq1d	$⊢ φ \to (I selectVars R) (\{X\}) (1_{P}) (\{⟨X, n (\emptyset)⟩\}) = (algSc (\{X\} mPoly U) \circ algSc (U)) (1_{R}) (\{⟨X, n (\emptyset)⟩\})$
27	26	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (I selectVars R) (\{X\}) (1_{P}) (\{⟨X, n (\emptyset)⟩\}) = (algSc (\{X\} mPoly U) \circ algSc (U)) (1_{R}) (\{⟨X, n (\emptyset)⟩\})$
28		eqid	$⊢ {Base}_{U} = {Base}_{U}$
29		eqid	$⊢ algSc (U) = algSc (U)$
30	6	difexd	$⊢ φ \to I ∖ \{X\} \in V$
31	3 28 18 29 30 15	mplasclf	$⊢ φ \to algSc (U) : {Base}_{R} ⟶ {Base}_{U}$
32	31 20	fvco3d	$⊢ φ \to (algSc (\{X\} mPoly U) \circ algSc (U)) (1_{R}) = algSc (\{X\} mPoly U) (algSc (U) (1_{R}))$
33		eqid	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\}$
34		eqid	$⊢ 0_{U} = 0_{U}$
35		snex	$⊢ \{X\} \in V$
36	35	a1i	$⊢ φ \to \{X\} \in V$
37	3 30 15	mplringd	$⊢ φ \to U \in Ring$
38	31 20	ffvelcdmd	$⊢ φ \to algSc (U) (1_{R}) \in {Base}_{U}$
39	21 33 34 28 19 36 37 38	mplascl	$⊢ φ \to algSc (\{X\} mPoly U) (algSc (U) (1_{R})) = (p \in \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (p = \{X\} \times \{0\}, algSc (U) (1_{R}), 0_{U}))$
40	32 39	eqtrd	$⊢ φ \to (algSc (\{X\} mPoly U) \circ algSc (U)) (1_{R}) = (p \in \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (p = \{X\} \times \{0\}, algSc (U) (1_{R}), 0_{U}))$
41	40	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (algSc (\{X\} mPoly U) \circ algSc (U)) (1_{R}) = (p \in \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\} ⟼ if (p = \{X\} \times \{0\}, algSc (U) (1_{R}), 0_{U}))$
42		eqeq1	$⊢ p = \{⟨X, n (\emptyset)⟩\} \to (p = \{X\} \times \{0\} \leftrightarrow \{⟨X, n (\emptyset)⟩\} = \{X\} \times \{0\})$
43	42	adantl	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to (p = \{X\} \times \{0\} \leftrightarrow \{⟨X, n (\emptyset)⟩\} = \{X\} \times \{0\})$
44		c0ex	$⊢ 0 \in V$
45	44	a1i	$⊢ φ \to 0 \in V$
46		xpsng	$⊢ (X \in I \land 0 \in V) \to \{X\} \times \{0\} = \{⟨X, 0⟩\}$
47	7 45 46	syl2anc	$⊢ φ \to \{X\} \times \{0\} = \{⟨X, 0⟩\}$
48	47	eqeq2d	$⊢ φ \to (\{⟨X, n (\emptyset)⟩\} = \{X\} \times \{0\} \leftrightarrow \{⟨X, n (\emptyset)⟩\} = \{⟨X, 0⟩\})$
49	48	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to (\{⟨X, n (\emptyset)⟩\} = \{X\} \times \{0\} \leftrightarrow \{⟨X, n (\emptyset)⟩\} = \{⟨X, 0⟩\})$
50		opex	$⊢ ⟨X, n (\emptyset)⟩ \in V$
51		sneqbg	$⊢ ⟨X, n (\emptyset)⟩ \in V \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, 0⟩\} \leftrightarrow ⟨X, n (\emptyset)⟩ = ⟨X, 0⟩)$
52	50 51	mp1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, 0⟩\} \leftrightarrow ⟨X, n (\emptyset)⟩ = ⟨X, 0⟩)$
53		eqidd	$⊢ φ \to X = X$
54		fvexd	$⊢ φ \to n (\emptyset) \in V$
55		opthg	$⊢ (X \in I \land n (\emptyset) \in V) \to (⟨X, n (\emptyset)⟩ = ⟨X, 0⟩ \leftrightarrow (X = X \land n (\emptyset) = 0))$
56	7 54 55	syl2anc	$⊢ φ \to (⟨X, n (\emptyset)⟩ = ⟨X, 0⟩ \leftrightarrow (X = X \land n (\emptyset) = 0))$
57	53 56	mpbirand	$⊢ φ \to (⟨X, n (\emptyset)⟩ = ⟨X, 0⟩ \leftrightarrow n (\emptyset) = 0)$
58	57	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (⟨X, n (\emptyset)⟩ = ⟨X, 0⟩ \leftrightarrow n (\emptyset) = 0)$
59		simpr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n \in ({ℕ_{0}}^{1_{𝑜}})$
60	59	elmaprd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n : 1_{𝑜} ⟶ ℕ_{0}$
61	60	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to n : 1_{𝑜} ⟶ ℕ_{0}$
62	61	feqmptd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to n = (u \in 1_{𝑜} ⟼ n (u))$
63		el1o	$⊢ u \in 1_{𝑜} \leftrightarrow u = \emptyset$
64	63	bilani	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \land u \in 1_{𝑜}) \to u = \emptyset$
65	64	fveq2d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \land u \in 1_{𝑜}) \to n (u) = n (\emptyset)$
66		simplr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \land u \in 1_{𝑜}) \to n (\emptyset) = 0$
67	65 66	eqtrd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \land u \in 1_{𝑜}) \to n (u) = 0$
68	67	mpteq2dva	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to (u \in 1_{𝑜} ⟼ n (u)) = (u \in 1_{𝑜} ⟼ 0)$
69	62 68	eqtrd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to n = (u \in 1_{𝑜} ⟼ 0)$
70		fconstmpt	$⊢ 1_{𝑜} \times \{0\} = (u \in 1_{𝑜} ⟼ 0)$
71	70	eqeq2i	$⊢ n = 1_{𝑜} \times \{0\} \leftrightarrow n = (u \in 1_{𝑜} ⟼ 0)$
72	69 71	sylibr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to n = 1_{𝑜} \times \{0\}$
73	71	bilani	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \to n = (u \in 1_{𝑜} ⟼ 0)$
74		eqidd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \land u = \emptyset) \to 0 = 0$
75		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
76	75	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \to \emptyset \in 1_{𝑜}$
77	44	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \to 0 \in V$
78	73 74 76 77	fvmptd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \to n (\emptyset) = 0$
79	72 78	impbida	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (n (\emptyset) = 0 \leftrightarrow n = 1_{𝑜} \times \{0\})$
80	52 58 79	3bitrd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, 0⟩\} \leftrightarrow n = 1_{𝑜} \times \{0\})$
81	80	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, 0⟩\} \leftrightarrow n = 1_{𝑜} \times \{0\})$
82	43 49 81	3bitrd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to (p = \{X\} \times \{0\} \leftrightarrow n = 1_{𝑜} \times \{0\})$
83		eqid	$⊢ 1_{U} = 1_{U}$
84	3 29 13 83 30 15	mplascl1	$⊢ φ \to algSc (U) (1_{R}) = 1_{U}$
85	84	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to algSc (U) (1_{R}) = 1_{U}$
86	82 85	ifbieq1d	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to if (p = \{X\} \times \{0\}, algSc (U) (1_{R}), 0_{U}) = if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U})$
87		breq1	$⊢ h = \{⟨X, n (\emptyset)⟩\} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\}))$
88		nn0ex	$⊢ ℕ_{0} \in V$
89	88	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to ℕ_{0} \in V$
90	35	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in V$
91	7	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to X \in I$
92	75	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in 1_{𝑜}$
93	60 92	ffvelcdmd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n (\emptyset) \in ℕ_{0}$
94	91 93	fsnd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
95	89 90 94	elmapdd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
96		snopfsupp	$⊢ (X \in I \land n (\emptyset) \in V \land 0 \in V) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
97	7 54 45 96	syl3anc	$⊢ φ \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
98	97	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
99	87 95 98	elrabd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
100		eqid	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
101	100	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\}$
102	99 101	eleqtrdi	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\}$
103	28 83 37	ringidcld	$⊢ φ \to 1_{U} \in {Base}_{U}$
104	37	ringgrpd	$⊢ φ \to U \in Grp$
105	28 34 104	grpidcld	$⊢ φ \to 0_{U} \in {Base}_{U}$
106	103 105	ifcld	$⊢ φ \to if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U}) \in {Base}_{U}$
107	106	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U}) \in {Base}_{U}$
108	41 86 102 107	fvmptd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (algSc (\{X\} mPoly U) \circ algSc (U)) (1_{R}) (\{⟨X, n (\emptyset)⟩\}) = if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U})$
109	27 108	eqtrd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (I selectVars R) (\{X\}) (1_{P}) (\{⟨X, n (\emptyset)⟩\}) = if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U})$
110	109	mpteq2dva	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (1_{P}) (\{⟨X, n (\emptyset)⟩\})) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U}))$
111		eqid	$⊢ 1_{𝑜} mPoly U = 1_{𝑜} mPoly U$
112		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{h \in ({ℕ_{0}}^{1_{𝑜}}) \| h^{-1} [ℕ] \in Fin\}$
113		eqid	$⊢ algSc (Q) = algSc (Q)$
114	4 113	ply1ascl	$⊢ algSc (Q) = algSc (1_{𝑜} mPoly U)$
115		1oex	$⊢ 1_{𝑜} \in V$
116	115	a1i	$⊢ φ \to 1_{𝑜} \in V$
117	111 112 34 28 114 116 37 103	mplascl	$⊢ φ \to algSc (Q) (1_{U}) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U}))$
118		eqid	$⊢ 1_{Q} = 1_{Q}$
119	4 113 83 118 37	ply1ascl1	$⊢ φ \to algSc (Q) (1_{U}) = 1_{Q}$
120	110 117 119	3eqtr2d	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (1_{P}) (\{⟨X, n (\emptyset)⟩\})) = 1_{Q}$
121	11 120	sylan9eqr	$⊢ (φ \land f = 1_{P}) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) = 1_{Q}$
122	2 6 15	mplringd	$⊢ φ \to P \in Ring$
123	1 14 122	ringidcld	$⊢ φ \to 1_{P} \in B$
124		fvexd	$⊢ φ \to 1_{Q} \in V$
125	5 121 123 124	fvmptd2	$⊢ φ \to H (1_{P}) = 1_{Q}$

Metamath Proof Explorer

Theorem selvply1rhmlem2

Proof