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

Metamath Proof Explorer

Theorem selvply1rhmlema

Proof