selvply1rhmlema

	Ref	Expression
Hypotheses	selvply1rhmlema.1	$⊢ B = {Base}_{P}$
	selvply1rhmlema.2	$⊢ P = \{X\} mPoly R$
	selvply1rhmlema.3	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	selvply1rhmlema.4	$⊢ \underset{˙}{\times} = \cdot_{Q}$
	selvply1rhmlema.5	$⊢ Q = {Poly}_{1} (R)$
	selvply1rhmlema.6	$⊢ M = (f \in B ⟼ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})))$
	selvply1rhmlema.7	$⊢ φ \to X \in V$
	selvply1rhmlema.8	$⊢ φ \to R \in Ring$
	selvply1rhmlema.9	$⊢ φ \to F \in B$
Assertion	selvply1rhmlema	$⊢ φ \to M (F) \in {Base}_{Q}$

Proof

Step	Hyp	Ref	Expression
1		selvply1rhmlema.1	$⊢ B = {Base}_{P}$
2		selvply1rhmlema.2	$⊢ P = \{X\} mPoly R$
3		selvply1rhmlema.3	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
4		selvply1rhmlema.4	$⊢ \underset{˙}{\times} = \cdot_{Q}$
5		selvply1rhmlema.5	$⊢ Q = {Poly}_{1} (R)$
6		selvply1rhmlema.6	$⊢ M = (f \in B ⟼ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})))$
7		selvply1rhmlema.7	$⊢ φ \to X \in V$
8		selvply1rhmlema.8	$⊢ φ \to R \in Ring$
9		selvply1rhmlema.9	$⊢ φ \to F \in B$
10		fvexd	$⊢ φ \to {Base}_{R} \in V$
11		ovexd	$⊢ φ \to {ℕ_{0}}^{1_{𝑜}} \in V$
12		fvexd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to F (\{⟨X, n (\emptyset)⟩\}) \in V$
13		fveq1	$⊢ f = F \to f (\{⟨X, n (\emptyset)⟩\}) = F (\{⟨X, n (\emptyset)⟩\})$
14	13	mpteq2dv	$⊢ f = F \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\}))$
15	11	mptexd	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\})) \in V$
16	6 14 9 15	fvmptd3	$⊢ φ \to M (F) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\}))$
17		fveq1	$⊢ n = m \to n (\emptyset) = m (\emptyset)$
18	17	opeq2d	$⊢ n = m \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
19	18	sneqd	$⊢ n = m \to \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}$
20	19	fveq2d	$⊢ n = m \to F (\{⟨X, n (\emptyset)⟩\}) = F (\{⟨X, m (\emptyset)⟩\})$
21	16	adantr	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to M (F) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\}))$
22		simpr	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to m \in ({ℕ_{0}}^{1_{𝑜}})$
23		eqid	$⊢ {Base}_{R} = {Base}_{R}$
24		eqid	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
25	24	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\{X\}}) \| h^{-1} [ℕ] \in Fin\}$
26	9	adantr	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to F \in B$
27	2 23 1 25 26	mplelf	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to F : \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
28		breq1	$⊢ h = \{⟨X, m (\emptyset)⟩\} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (\{⟨X, m (\emptyset)⟩\}))$
29		nn0ex	$⊢ ℕ_{0} \in V$
30	29	a1i	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to ℕ_{0} \in V$
31		snex	$⊢ \{X\} \in V$
32	31	a1i	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in V$
33	7	adantr	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to X \in V$
34	22	elmaprd	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to m : 1_{𝑜} ⟶ ℕ_{0}$
35		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
36	35	a1i	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in 1_{𝑜}$
37	34 36	ffvelcdmd	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to m (\emptyset) \in ℕ_{0}$
38	33 37	fsnd	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, m (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
39	30 32 38	elmapdd	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, m (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
40		snfi	$⊢ \{X\} \in Fin$
41	40	a1i	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in Fin$
42		c0ex	$⊢ 0 \in V$
43	42	a1i	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to 0 \in V$
44	38 41 43	fdmfifsupp	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0} (\{⟨X, m (\emptyset)⟩\})$
45	28 39 44	elrabd	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, m (\emptyset)⟩\} \in \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
46	27 45	ffvelcdmd	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to F (\{⟨X, m (\emptyset)⟩\}) \in {Base}_{R}$
47	20 21 22 46	fvmptd4	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to M (F) (m) = F (\{⟨X, m (\emptyset)⟩\})$
48	47 46	eqeltrd	$⊢ (φ \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to M (F) (m) \in {Base}_{R}$
49	12 16 48	fmpt2d	$⊢ φ \to M (F) : {ℕ_{0}}^{1_{𝑜}} ⟶ {Base}_{R}$
50	10 11 49	elmapdd	$⊢ φ \to M (F) \in ({Base}_{R}^{({ℕ_{0}}^{1_{𝑜}})})$
51		eqid	$⊢ 1_{𝑜} mPwSer R = 1_{𝑜} mPwSer R$
52		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{h \in ({ℕ_{0}}^{1_{𝑜}}) \| h^{-1} [ℕ] \in Fin\}$
53		eqid	$⊢ {Base}_{(1_{𝑜} mPwSer R)} = {Base}_{(1_{𝑜} mPwSer R)}$
54		1oex	$⊢ 1_{𝑜} \in V$
55	54	a1i	$⊢ φ \to 1_{𝑜} \in V$
56	51 23 52 53 55	psrbas	$⊢ φ \to {Base}_{(1_{𝑜} mPwSer R)} = {Base}_{R}^{({ℕ_{0}}^{1_{𝑜}})}$
57	50 56	eleqtrrd	$⊢ φ \to M (F) \in {Base}_{(1_{𝑜} mPwSer R)}$
58	2 23 1 25 9	mplelf	$⊢ φ \to F : \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
59		breq1	$⊢ h = \{⟨X, n (\emptyset)⟩\} \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\}))$
60	29	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to ℕ_{0} \in V$
61	31	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in V$
62	7	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to X \in V$
63		simpr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n \in ({ℕ_{0}}^{1_{𝑜}})$
64	63	elmaprd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n : 1_{𝑜} ⟶ ℕ_{0}$
65	35	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in 1_{𝑜}$
66	64 65	ffvelcdmd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n (\emptyset) \in ℕ_{0}$
67	62 66	fsnd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
68	60 61 67	elmapdd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
69	40	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in Fin$
70	42	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 0 \in V$
71	67 69 70	fdmfifsupp	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
72	59 68 71	elrabd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in \{h \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (h)\}$
73	58 72	cofmpt	$⊢ φ \to F \circ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\}))$
74		eqid	$⊢ 0_{R} = 0_{R}$
75	2 1 74 9	mplelsfi	$⊢ φ \to {finSupp}_{0_{R}} (F)$
76	68	ralrimiva	$⊢ φ \to \forall n \in ({ℕ_{0}}^{1_{𝑜}}) \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
77	62	ad2antrr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to X \in V$
78		fvexd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n (\emptyset) \in V$
79		opex	$⊢ ⟨X, n (\emptyset)⟩ \in V$
80	79	sneqr	$⊢ \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
81	80	adantl	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
82		opthg	$⊢ (X \in V \land n (\emptyset) \in V) \to (⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩ \leftrightarrow (X = X \land n (\emptyset) = m (\emptyset)))$
83	82	simplbda	$⊢ ((X \in V \land n (\emptyset) \in V) \land ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩) \to n (\emptyset) = m (\emptyset)$
84	77 78 81 83	syl21anc	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n (\emptyset) = m (\emptyset)$
85		0ex	$⊢ \emptyset \in V$
86	85	a1i	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to \emptyset \in V$
87		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
88	64	ad2antrr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n : 1_{𝑜} ⟶ ℕ_{0}$
89	88	ffnd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n Fn 1_{𝑜}$
90	34	ad4ant13	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to m : 1_{𝑜} ⟶ ℕ_{0}$
91	90	ffnd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to m Fn 1_{𝑜}$
92	86 87 89 91	fsneq	$⊢ (((φ \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))$
93	84 92	mpbird	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \land \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}) \to n = m$
94	93	ex	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m \in ({ℕ_{0}}^{1_{𝑜}})) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to n = m)$
95	94	anasss	$⊢ (φ \land (n \in ({ℕ_{0}}^{1_{𝑜}}) \land m \in ({ℕ_{0}}^{1_{𝑜}}))) \to (\{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to n = m)$
96	95	ralrimivva	$⊢ φ \to \forall n \in ({ℕ_{0}}^{1_{𝑜}}) \forall m \in ({ℕ_{0}}^{1_{𝑜}}) (\{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\} \to n = m)$
97		eqid	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\})$
98	97 19	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))$
99	76 96 98	sylanbrc	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\}) : {ℕ_{0}}^{1_{𝑜}} \underset{1-1}{⟶} {ℕ_{0}}^{\{X\}}$
100		fvexd	$⊢ φ \to 0_{R} \in V$
101	75 99 100 9	fsuppco	$⊢ φ \to {finSupp}_{0_{R}} ((F \circ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \{⟨X, n (\emptyset)⟩\})))$
102	73 101	eqbrtrrd	$⊢ φ \to {finSupp}_{0_{R}} ((n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\})))$
103	16 102	eqbrtrd	$⊢ φ \to {finSupp}_{0_{R}} (M (F))$
104		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
105		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
106	5 105	ply1bas	$⊢ {Base}_{Q} = {Base}_{(1_{𝑜} mPoly R)}$
107	104 51 53 74 106	mplelbas	$⊢ M (F) \in {Base}_{Q} \leftrightarrow (M (F) \in {Base}_{(1_{𝑜} mPwSer R)} \land {finSupp}_{0_{R}} (M (F)))$
108	57 103 107	sylanbrc	$⊢ φ \to M (F) \in {Base}_{Q}$

Metamath Proof Explorer

Theorem selvply1rhmlema

Proof