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		1oex	$⊢ 1_{𝑜} \in V$
60	59	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 1_{𝑜} \in V$
61		nn0ex	$⊢ ℕ_{0} \in V$
62	61	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to ℕ_{0} \in V$
63		simpr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n \in ({ℕ_{0}}^{1_{𝑜}})$
64	60 62 63	elmaprd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n : 1_{𝑜} ⟶ ℕ_{0}$
65	64	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to n : 1_{𝑜} ⟶ ℕ_{0}$
66	65	feqmptd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to n = (u \in 1_{𝑜} ⟼ n (u))$
67		el1o	$⊢ u \in 1_{𝑜} \leftrightarrow u = \emptyset$
68	67	biimpi	$⊢ u \in 1_{𝑜} \to u = \emptyset$
69	68	adantl	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \land u \in 1_{𝑜}) \to u = \emptyset$
70	69	fveq2d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \land u \in 1_{𝑜}) \to n (u) = n (\emptyset)$
71		simplr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \land u \in 1_{𝑜}) \to n (\emptyset) = 0$
72	70 71	eqtrd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \land u \in 1_{𝑜}) \to n (u) = 0$
73	72	mpteq2dva	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to (u \in 1_{𝑜} ⟼ n (u)) = (u \in 1_{𝑜} ⟼ 0)$
74	66 73	eqtrd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to n = (u \in 1_{𝑜} ⟼ 0)$
75		fconstmpt	$⊢ 1_{𝑜} \times \{0\} = (u \in 1_{𝑜} ⟼ 0)$
76	75	eqeq2i	$⊢ n = 1_{𝑜} \times \{0\} \leftrightarrow n = (u \in 1_{𝑜} ⟼ 0)$
77	74 76	sylibr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n (\emptyset) = 0) \to n = 1_{𝑜} \times \{0\}$
78	76	biimpi	$⊢ n = 1_{𝑜} \times \{0\} \to n = (u \in 1_{𝑜} ⟼ 0)$
79	78	adantl	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \to n = (u \in 1_{𝑜} ⟼ 0)$
80		eqidd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \land u = \emptyset) \to 0 = 0$
81		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
82	81	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \to \emptyset \in 1_{𝑜}$
83	44	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \to 0 \in V$
84	79 80 82 83	fvmptd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land n = 1_{𝑜} \times \{0\}) \to n (\emptyset) = 0$
85	77 84	impbida	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (n (\emptyset) = 0 \leftrightarrow n = 1_{𝑜} \times \{0\})$
86	52 58 85	3bitrd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, 0⟩\} \leftrightarrow n = 1_{𝑜} \times \{0\})$
87	86	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, 0⟩\} \leftrightarrow n = 1_{𝑜} \times \{0\})$
88	43 49 87	3bitrd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to (p = \{X\} \times \{0\} \leftrightarrow n = 1_{𝑜} \times \{0\})$
89		eqid	$⊢ 1_{U} = 1_{U}$
90	3 29 13 89 30 15	mplascl1	$⊢ φ \to algSc (U) (1_{R}) = 1_{U}$
91	90	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land p = \{⟨X, n (\emptyset)⟩\}) \to algSc (U) (1_{R}) = 1_{U}$
92	88 91	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})$
93		breq1	$⊢ h = \{⟨X, n (\emptyset)⟩\} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\}))$
94	35	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in V$
95	7	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to X \in I$
96	81	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in 1_{𝑜}$
97	64 96	ffvelcdmd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n (\emptyset) \in ℕ_{0}$
98	95 97	fsnd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
99	62 94 98	elmapdd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
100		snopfsupp	$⊢ (X \in I \land n (\emptyset) \in V \land 0 \in V) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
101	7 54 45 100	syl3anc	$⊢ φ \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
102	101	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
103	93 99 102	elrabd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
104		eqid	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
105	104	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\}$
106	103 105	eleqtrdi	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\}$
107	28 89 37	ringidcld	$⊢ φ \to 1_{U} \in {Base}_{U}$
108	37	ringgrpd	$⊢ φ \to U \in Grp$
109	28 34 108	grpidcld	$⊢ φ \to 0_{U} \in {Base}_{U}$
110	107 109	ifcld	$⊢ φ \to if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U}) \in {Base}_{U}$
111	110	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U}) \in {Base}_{U}$
112	41 92 106 111	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})$
113	27 112	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})$
114	113	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}))$
115		eqid	$⊢ 1_{𝑜} mPoly U = 1_{𝑜} mPoly U$
116		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{h \in ({ℕ_{0}}^{1_{𝑜}}) \| h^{-1} [ℕ] \in Fin\}$
117		eqid	$⊢ algSc (Q) = algSc (Q)$
118	4 117	ply1ascl	$⊢ algSc (Q) = algSc (1_{𝑜} mPoly U)$
119	59	a1i	$⊢ φ \to 1_{𝑜} \in V$
120	115 116 34 28 118 119 37 107	mplascl	$⊢ φ \to algSc (Q) (1_{U}) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ if (n = 1_{𝑜} \times \{0\}, 1_{U}, 0_{U}))$
121		eqid	$⊢ 1_{Q} = 1_{Q}$
122	4 117 89 121 37	ply1ascl1	$⊢ φ \to algSc (Q) (1_{U}) = 1_{Q}$
123	114 120 122	3eqtr2d	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (1_{P}) (\{⟨X, n (\emptyset)⟩\})) = 1_{Q}$
124	11 123	sylan9eqr	$⊢ (φ \land f = 1_{P}) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (I selectVars R) (\{X\}) (f) (\{⟨X, n (\emptyset)⟩\})) = 1_{Q}$
125	2 6 15	mplringd	$⊢ φ \to P \in Ring$
126	1 14 125	ringidcld	$⊢ φ \to 1_{P} \in B$
127		fvexd	$⊢ φ \to 1_{Q} \in V$
128	5 124 126 127	fvmptd2	$⊢ φ \to H (1_{P}) = 1_{Q}$

Metamath Proof Explorer

Theorem selvply1rhmlem2

Proof