0mplrim

Description: Build a ring isomorphism between multivariate polynomials with no variables and the underlying ring. (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	0mplric.b	$⊢ B = {Base}_{P}$
	0mplric.p	$⊢ P = \emptyset mPoly R$
	0mplric.r	$⊢ φ \to R \in Ring$
	0mplrim.f	$⊢ F = (p \in B ⟼ p (\emptyset))$
Assertion	0mplrim	$⊢ φ \to F \in (P RingIso R)$

Proof

Step	Hyp	Ref	Expression
1		0mplric.b	$⊢ B = {Base}_{P}$
2		0mplric.p	$⊢ P = \emptyset mPoly R$
3		0mplric.r	$⊢ φ \to R \in Ring$
4		0mplrim.f	$⊢ F = (p \in B ⟼ p (\emptyset))$
5		eqid	$⊢ 1_{P} = 1_{P}$
6		eqid	$⊢ 1_{R} = 1_{R}$
7		eqid	$⊢ \cdot_{P} = \cdot_{P}$
8		eqid	$⊢ \cdot_{R} = \cdot_{R}$
9		0ex	$⊢ \emptyset \in V$
10	9	a1i	$⊢ φ \to \emptyset \in V$
11	2 10 3	mplringd	$⊢ φ \to P \in Ring$
12		fveq1	$⊢ p = 1_{P} \to p (\emptyset) = 1_{P} (\emptyset)$
13		eqid	$⊢ algSc (P) = algSc (P)$
14	2 13 6 5 10 3	mplascl1	$⊢ φ \to algSc (P) (1_{R}) = 1_{P}$
15	14	fveq1d	$⊢ φ \to algSc (P) (1_{R}) (\emptyset) = 1_{P} (\emptyset)$
16		eqid	$⊢ \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
17	16	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{\emptyset}) \| h^{-1} [ℕ] \in Fin\}$
18		eqid	$⊢ 0_{R} = 0_{R}$
19		eqid	$⊢ {Base}_{R} = {Base}_{R}$
20	19 6 3	ringidcld	$⊢ φ \to 1_{R} \in {Base}_{R}$
21	2 17 18 19 13 10 3 20	mplascl	$⊢ φ \to algSc (P) (1_{R}) = (p \in \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\} ⟼ if (p = \emptyset \times \{0\}, 1_{R}, 0_{R}))$
22		simpr	$⊢ (φ \land p = \emptyset) \to p = \emptyset$
23		0xp	$⊢ \emptyset \times \{0\} = \emptyset$
24	22 23	eqtr4di	$⊢ (φ \land p = \emptyset) \to p = \emptyset \times \{0\}$
25	24	iftrued	$⊢ (φ \land p = \emptyset) \to if (p = \emptyset \times \{0\}, 1_{R}, 0_{R}) = 1_{R}$
26		breq1	$⊢ h = \emptyset \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (\emptyset))$
27		nn0ex	$⊢ ℕ_{0} \in V$
28	27	a1i	$⊢ ⊤ \to ℕ_{0} \in V$
29	9	a1i	$⊢ ⊤ \to \emptyset \in V$
30		f0	$⊢ \emptyset : \emptyset ⟶ ℕ_{0}$
31	30	a1i	$⊢ ⊤ \to \emptyset : \emptyset ⟶ ℕ_{0}$
32	28 29 31	elmapdd	$⊢ ⊤ \to \emptyset \in ({ℕ_{0}}^{\emptyset})$
33		0fi	$⊢ \emptyset \in Fin$
34	33	a1i	$⊢ ⊤ \to \emptyset \in Fin$
35		c0ex	$⊢ 0 \in V$
36	35	a1i	$⊢ ⊤ \to 0 \in V$
37	31 34 36	fidmfisupp	$⊢ ⊤ \to {finSupp}_{0} (\emptyset)$
38	26 32 37	elrabd	$⊢ ⊤ \to \emptyset \in \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
39	38	mptru	$⊢ \emptyset \in \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
40	39	a1i	$⊢ φ \to \emptyset \in \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
41	21 25 40 20	fvmptd	$⊢ φ \to algSc (P) (1_{R}) (\emptyset) = 1_{R}$
42	15 41	eqtr3d	$⊢ φ \to 1_{P} (\emptyset) = 1_{R}$
43	12 42	sylan9eqr	$⊢ (φ \land p = 1_{P}) \to p (\emptyset) = 1_{R}$
44	1 5 11	ringidcld	$⊢ φ \to 1_{P} \in B$
45	4 43 44 20	fvmptd2	$⊢ φ \to F (1_{P}) = 1_{R}$
46		fveq1	$⊢ p = x \cdot_{P} y \to p (\emptyset) = (x \cdot_{P} y) (\emptyset)$
47	11	ad2antrr	$⊢ ((φ \land x \in B) \land y \in B) \to P \in Ring$
48		simplr	$⊢ ((φ \land x \in B) \land y \in B) \to x \in B$
49		simpr	$⊢ ((φ \land x \in B) \land y \in B) \to y \in B$
50	1 7 47 48 49	ringcld	$⊢ ((φ \land x \in B) \land y \in B) \to x \cdot_{P} y \in B$
51		fvexd	$⊢ ((φ \land x \in B) \land y \in B) \to (x \cdot_{P} y) (\emptyset) \in V$
52	4 46 50 51	fvmptd3	$⊢ ((φ \land x \in B) \land y \in B) \to F (x \cdot_{P} y) = (x \cdot_{P} y) (\emptyset)$
53		elsni	$⊢ p \in \{\emptyset\} \to p = \emptyset$
54	39	a1i	$⊢ p \in \{\emptyset\} \to \emptyset \in \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
55	53 54	eqeltrd	$⊢ p \in \{\emptyset\} \to p \in \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
56		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{\emptyset}$
57		mapdm0	$⊢ ℕ_{0} \in V \to {ℕ_{0}}^{\emptyset} = \{\emptyset\}$
58	27 57	ax-mp	$⊢ {ℕ_{0}}^{\emptyset} = \{\emptyset\}$
59	56 58	sseqtri	$⊢ \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\} \subseteq \{\emptyset\}$
60	59	sseli	$⊢ p \in \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\} \to p \in \{\emptyset\}$
61	55 60	impbii	$⊢ p \in \{\emptyset\} \leftrightarrow p \in \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
62	61	eqriv	$⊢ \{\emptyset\} = \{h \in ({ℕ_{0}}^{\emptyset}) \| {finSupp}_{0} (h)\}$
63	62	psrbasfsupp	$⊢ \{\emptyset\} = \{h \in ({ℕ_{0}}^{\emptyset}) \| h^{-1} [ℕ] \in Fin\}$
64	2 1 8 7 63 48 49	mplmul	$⊢ ((φ \land x \in B) \land y \in B) \to x \cdot_{P} y = (p \in \{\emptyset\} ⟼ \underset{q \in \{r \in \{\emptyset\} \| r \leq_{f} p\}}{\sum_{R}} (x (q) \cdot_{R} y (p -_{f} q)))$
65	3	ringgrpd	$⊢ φ \to R \in Grp$
66	65	grpmndd	$⊢ φ \to R \in Mnd$
67	66	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to R \in Mnd$
68	9	a1i	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to \emptyset \in V$
69	3	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to R \in Ring$
70	2 19 1 63 48	mplelf	$⊢ ((φ \land x \in B) \land y \in B) \to x : \{\emptyset\} ⟶ {Base}_{R}$
71	70	adantr	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to x : \{\emptyset\} ⟶ {Base}_{R}$
72	9	snid	$⊢ \emptyset \in \{\emptyset\}$
73	72	a1i	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to \emptyset \in \{\emptyset\}$
74	71 73	ffvelcdmd	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to x (\emptyset) \in {Base}_{R}$
75	2 19 1 63 49	mplelf	$⊢ ((φ \land x \in B) \land y \in B) \to y : \{\emptyset\} ⟶ {Base}_{R}$
76	75	adantr	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to y : \{\emptyset\} ⟶ {Base}_{R}$
77	76 73	ffvelcdmd	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to y (\emptyset) \in {Base}_{R}$
78	19 8 69 74 77	ringcld	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to x (\emptyset) \cdot_{R} y (\emptyset) \in {Base}_{R}$
79		simpr	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to q = \emptyset$
80	79	fveq2d	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to x (q) = x (\emptyset)$
81	9	a1i	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to \emptyset \in V$
82		simplr	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to p = \emptyset$
83	82	eqcomd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to \emptyset = p$
84	30	a1i	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to \emptyset : \emptyset ⟶ ℕ_{0}$
85	83 84	feq1dd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to p : \emptyset ⟶ ℕ_{0}$
86	85	ffnd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to p Fn \emptyset$
87	79	eqcomd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to \emptyset = q$
88	87 84	feq1dd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to q : \emptyset ⟶ ℕ_{0}$
89	88	ffnd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to q Fn \emptyset$
90	81 86 89	offvalfv	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to p -_{f} q = (a \in \emptyset ⟼ p (a) - q (a))$
91		mpt0	$⊢ (a \in \emptyset ⟼ p (a) - q (a)) = \emptyset$
92	90 91	eqtrdi	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to p -_{f} q = \emptyset$
93	92	fveq2d	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to y (p -_{f} q) = y (\emptyset)$
94	80 93	oveq12d	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land q = \emptyset) \to x (q) \cdot_{R} y (p -_{f} q) = x (\emptyset) \cdot_{R} y (\emptyset)$
95	19 67 68 78 94	gsumsnd	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to \underset{q \in \{\emptyset\}}{\sum_{R}} (x (q) \cdot_{R} y (p -_{f} q)) = x (\emptyset) \cdot_{R} y (\emptyset)$
96		simpr	$⊢ (((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \land a \in \emptyset) \to a \in \emptyset$
97		noel	$⊢ \neg a \in \emptyset$
98	97	a1i	$⊢ (((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \land a \in \emptyset) \to \neg a \in \emptyset$
99	96 98	pm2.21dd	$⊢ (((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \land a \in \emptyset) \to r (a) \leq p (a)$
100	99	ralrimiva	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to \forall a \in \emptyset r (a) \leq p (a)$
101		simpr	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to r \in \{\emptyset\}$
102	101	elsnd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to r = \emptyset$
103	102	eqcomd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to \emptyset = r$
104	30	a1i	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to \emptyset : \emptyset ⟶ ℕ_{0}$
105	103 104	feq1dd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to r : \emptyset ⟶ ℕ_{0}$
106	105	ffnd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to r Fn \emptyset$
107		simplr	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to p = \emptyset$
108	107	eqcomd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to \emptyset = p$
109	108 104	feq1dd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to p : \emptyset ⟶ ℕ_{0}$
110	109	ffnd	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to p Fn \emptyset$
111		vex	$⊢ p \in V$
112	111	a1i	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to p \in V$
113		inidm	$⊢ \emptyset \cap \emptyset = \emptyset$
114		eqidd	$⊢ (((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \land a \in \emptyset) \to r (a) = r (a)$
115		eqidd	$⊢ (((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \land a \in \emptyset) \to p (a) = p (a)$
116	106 110 101 112 113 114 115	ofrfvalg	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to (r \leq_{f} p \leftrightarrow \forall a \in \emptyset r (a) \leq p (a))$
117	100 116	mpbird	$⊢ ((((φ \land x \in B) \land y \in B) \land p = \emptyset) \land r \in \{\emptyset\}) \to r \leq_{f} p$
118	117	rabeqcda	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to \{r \in \{\emptyset\} \| r \leq_{f} p\} = \{\emptyset\}$
119	118	mpteq1d	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to (q \in \{r \in \{\emptyset\} \| r \leq_{f} p\} ⟼ x (q) \cdot_{R} y (p -_{f} q)) = (q \in \{\emptyset\} ⟼ x (q) \cdot_{R} y (p -_{f} q))$
120	119	oveq2d	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to \underset{q \in \{r \in \{\emptyset\} \| r \leq_{f} p\}}{\sum_{R}} (x (q) \cdot_{R} y (p -_{f} q)) = \underset{q \in \{\emptyset\}}{\sum_{R}} (x (q) \cdot_{R} y (p -_{f} q))$
121		fveq1	$⊢ p = x \to p (\emptyset) = x (\emptyset)$
122		fvexd	$⊢ ((φ \land x \in B) \land y \in B) \to x (\emptyset) \in V$
123	4 121 48 122	fvmptd3	$⊢ ((φ \land x \in B) \land y \in B) \to F (x) = x (\emptyset)$
124	123	adantr	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to F (x) = x (\emptyset)$
125		fveq1	$⊢ p = y \to p (\emptyset) = y (\emptyset)$
126		fvexd	$⊢ ((φ \land x \in B) \land y \in B) \to y (\emptyset) \in V$
127	4 125 49 126	fvmptd3	$⊢ ((φ \land x \in B) \land y \in B) \to F (y) = y (\emptyset)$
128	127	adantr	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to F (y) = y (\emptyset)$
129	124 128	oveq12d	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to F (x) \cdot_{R} F (y) = x (\emptyset) \cdot_{R} y (\emptyset)$
130	95 120 129	3eqtr4d	$⊢ (((φ \land x \in B) \land y \in B) \land p = \emptyset) \to \underset{q \in \{r \in \{\emptyset\} \| r \leq_{f} p\}}{\sum_{R}} (x (q) \cdot_{R} y (p -_{f} q)) = F (x) \cdot_{R} F (y)$
131	72	a1i	$⊢ ((φ \land x \in B) \land y \in B) \to \emptyset \in \{\emptyset\}$
132		ovexd	$⊢ ((φ \land x \in B) \land y \in B) \to F (x) \cdot_{R} F (y) \in V$
133	64 130 131 132	fvmptd	$⊢ ((φ \land x \in B) \land y \in B) \to (x \cdot_{P} y) (\emptyset) = F (x) \cdot_{R} F (y)$
134	52 133	eqtrd	$⊢ ((φ \land x \in B) \land y \in B) \to F (x \cdot_{P} y) = F (x) \cdot_{R} F (y)$
135	134	anasss	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \cdot_{P} y) = F (x) \cdot_{R} F (y)$
136		eqid	$⊢ +_{P} = +_{P}$
137		eqid	$⊢ +_{R} = +_{R}$
138		fvexd	$⊢ (φ \land p \in B) \to p (\emptyset) \in V$
139		snex	$⊢ \{⟨\emptyset, a⟩\} \in V$
140	139	a1i	$⊢ (φ \land a \in {Base}_{R}) \to \{⟨\emptyset, a⟩\} \in V$
141		simpr	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to a = p (\emptyset)$
142		simplr	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to p \in B$
143	2 19 1 63 142	mplelf	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to p : \{\emptyset\} ⟶ {Base}_{R}$
144	72	a1i	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to \emptyset \in \{\emptyset\}$
145	143 144	ffvelcdmd	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to p (\emptyset) \in {Base}_{R}$
146	141 145	eqeltrd	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to a \in {Base}_{R}$
147	146	elexd	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to a \in V$
148		fvsng	$⊢ (\emptyset \in V \land a \in V) \to \{⟨\emptyset, a⟩\} (\emptyset) = a$
149	9 147 148	sylancr	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to \{⟨\emptyset, a⟩\} (\emptyset) = a$
150	149 141	eqtr2d	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to p (\emptyset) = \{⟨\emptyset, a⟩\} (\emptyset)$
151	9	a1i	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to \emptyset \in V$
152		eqid	$⊢ \{\emptyset\} = \{\emptyset\}$
153	143	ffnd	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to p Fn \{\emptyset\}$
154	151 147	fsnd	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to \{⟨\emptyset, a⟩\} : \{\emptyset\} ⟶ V$
155	154	ffnd	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to \{⟨\emptyset, a⟩\} Fn \{\emptyset\}$
156	151 152 153 155	fsneq	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to (p = \{⟨\emptyset, a⟩\} \leftrightarrow p (\emptyset) = \{⟨\emptyset, a⟩\} (\emptyset))$
157	150 156	mpbird	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to p = \{⟨\emptyset, a⟩\}$
158	146 157	jca	$⊢ ((φ \land p \in B) \land a = p (\emptyset)) \to (a \in {Base}_{R} \land p = \{⟨\emptyset, a⟩\})$
159	158	anasss	$⊢ (φ \land (p \in B \land a = p (\emptyset))) \to (a \in {Base}_{R} \land p = \{⟨\emptyset, a⟩\})$
160		simpr	$⊢ ((φ \land a \in {Base}_{R}) \land p = \{⟨\emptyset, a⟩\}) \to p = \{⟨\emptyset, a⟩\}$
161		fvexd	$⊢ (φ \land a \in {Base}_{R}) \to {Base}_{R} \in V$
162		snex	$⊢ \{\emptyset\} \in V$
163	162	a1i	$⊢ (φ \land a \in {Base}_{R}) \to \{\emptyset\} \in V$
164	9	a1i	$⊢ (φ \land a \in {Base}_{R}) \to \emptyset \in V$
165		simpr	$⊢ (φ \land a \in {Base}_{R}) \to a \in {Base}_{R}$
166	164 165	fsnd	$⊢ (φ \land a \in {Base}_{R}) \to \{⟨\emptyset, a⟩\} : \{\emptyset\} ⟶ {Base}_{R}$
167	161 163 166	elmapdd	$⊢ (φ \land a \in {Base}_{R}) \to \{⟨\emptyset, a⟩\} \in ({Base}_{R}^{\{\emptyset\}})$
168		eqid	$⊢ \emptyset mPwSer R = \emptyset mPwSer R$
169		eqid	$⊢ {Base}_{(\emptyset mPwSer R)} = {Base}_{(\emptyset mPwSer R)}$
170	168 19 63 169 164	psrbas	$⊢ (φ \land a \in {Base}_{R}) \to {Base}_{(\emptyset mPwSer R)} = {Base}_{R}^{\{\emptyset\}}$
171	167 170	eleqtrrd	$⊢ (φ \land a \in {Base}_{R}) \to \{⟨\emptyset, a⟩\} \in {Base}_{(\emptyset mPwSer R)}$
172		fvexd	$⊢ (φ \land a \in {Base}_{R}) \to 0_{R} \in V$
173		snopfsupp	$⊢ (\emptyset \in V \land a \in {Base}_{R} \land 0_{R} \in V) \to {finSupp}_{0_{R}} (\{⟨\emptyset, a⟩\})$
174	9 165 172 173	mp3an2i	$⊢ (φ \land a \in {Base}_{R}) \to {finSupp}_{0_{R}} (\{⟨\emptyset, a⟩\})$
175	2 168 169 18 1	mplelbas	$⊢ \{⟨\emptyset, a⟩\} \in B \leftrightarrow (\{⟨\emptyset, a⟩\} \in {Base}_{(\emptyset mPwSer R)} \land {finSupp}_{0_{R}} (\{⟨\emptyset, a⟩\}))$
176	171 174 175	sylanbrc	$⊢ (φ \land a \in {Base}_{R}) \to \{⟨\emptyset, a⟩\} \in B$
177	176	adantr	$⊢ ((φ \land a \in {Base}_{R}) \land p = \{⟨\emptyset, a⟩\}) \to \{⟨\emptyset, a⟩\} \in B$
178	160 177	eqeltrd	$⊢ ((φ \land a \in {Base}_{R}) \land p = \{⟨\emptyset, a⟩\}) \to p \in B$
179	160	fveq1d	$⊢ ((φ \land a \in {Base}_{R}) \land p = \{⟨\emptyset, a⟩\}) \to p (\emptyset) = \{⟨\emptyset, a⟩\} (\emptyset)$
180		fvsng	$⊢ (\emptyset \in V \land a \in {Base}_{R}) \to \{⟨\emptyset, a⟩\} (\emptyset) = a$
181	9 165 180	sylancr	$⊢ (φ \land a \in {Base}_{R}) \to \{⟨\emptyset, a⟩\} (\emptyset) = a$
182	181	adantr	$⊢ ((φ \land a \in {Base}_{R}) \land p = \{⟨\emptyset, a⟩\}) \to \{⟨\emptyset, a⟩\} (\emptyset) = a$
183	179 182	eqtr2d	$⊢ ((φ \land a \in {Base}_{R}) \land p = \{⟨\emptyset, a⟩\}) \to a = p (\emptyset)$
184	178 183	jca	$⊢ ((φ \land a \in {Base}_{R}) \land p = \{⟨\emptyset, a⟩\}) \to (p \in B \land a = p (\emptyset))$
185	184	anasss	$⊢ (φ \land (a \in {Base}_{R} \land p = \{⟨\emptyset, a⟩\})) \to (p \in B \land a = p (\emptyset))$
186	159 185	impbida	$⊢ φ \to ((p \in B \land a = p (\emptyset)) \leftrightarrow (a \in {Base}_{R} \land p = \{⟨\emptyset, a⟩\}))$
187	4 138 140 186	f1od	$⊢ φ \to F : B \underset{1-1 onto}{⟶} {Base}_{R}$
188		f1of	$⊢ F : B \underset{1-1 onto}{⟶} {Base}_{R} \to F : B ⟶ {Base}_{R}$
189	187 188	syl	$⊢ φ \to F : B ⟶ {Base}_{R}$
190		simpr	$⊢ (((φ \land x \in B) \land y \in B) \land p = x +_{P} y) \to p = x +_{P} y$
191	190	fveq1d	$⊢ (((φ \land x \in B) \land y \in B) \land p = x +_{P} y) \to p (\emptyset) = (x +_{P} y) (\emptyset)$
192		simpllr	$⊢ (((φ \land x \in B) \land y \in B) \land p = x +_{P} y) \to x \in B$
193		simplr	$⊢ (((φ \land x \in B) \land y \in B) \land p = x +_{P} y) \to y \in B$
194	2 1 137 136 192 193	mpladd	$⊢ (((φ \land x \in B) \land y \in B) \land p = x +_{P} y) \to x +_{P} y = x {+_{R}}_{f} y$
195	194	fveq1d	$⊢ (((φ \land x \in B) \land y \in B) \land p = x +_{P} y) \to (x +_{P} y) (\emptyset) = (x {+_{R}}_{f} y) (\emptyset)$
196	70	ffnd	$⊢ ((φ \land x \in B) \land y \in B) \to x Fn \{\emptyset\}$
197	75	ffnd	$⊢ ((φ \land x \in B) \land y \in B) \to y Fn \{\emptyset\}$
198	162	a1i	$⊢ ((φ \land x \in B) \land y \in B) \to \{\emptyset\} \in V$
199		inidm	$⊢ \{\emptyset\} \cap \{\emptyset\} = \{\emptyset\}$
200		eqidd	$⊢ (((φ \land x \in B) \land y \in B) \land \emptyset \in \{\emptyset\}) \to x (\emptyset) = x (\emptyset)$
201		eqidd	$⊢ (((φ \land x \in B) \land y \in B) \land \emptyset \in \{\emptyset\}) \to y (\emptyset) = y (\emptyset)$
202	196 197 198 198 199 200 201	ofval	$⊢ (((φ \land x \in B) \land y \in B) \land \emptyset \in \{\emptyset\}) \to (x {+_{R}}_{f} y) (\emptyset) = x (\emptyset) +_{R} y (\emptyset)$
203	72 202	mpan2	$⊢ ((φ \land x \in B) \land y \in B) \to (x {+_{R}}_{f} y) (\emptyset) = x (\emptyset) +_{R} y (\emptyset)$
204	203	adantr	$⊢ (((φ \land x \in B) \land y \in B) \land p = x +_{P} y) \to (x {+_{R}}_{f} y) (\emptyset) = x (\emptyset) +_{R} y (\emptyset)$
205	191 195 204	3eqtrd	$⊢ (((φ \land x \in B) \land y \in B) \land p = x +_{P} y) \to p (\emptyset) = x (\emptyset) +_{R} y (\emptyset)$
206	11	ringgrpd	$⊢ φ \to P \in Grp$
207	206	ad2antrr	$⊢ ((φ \land x \in B) \land y \in B) \to P \in Grp$
208	1 136 207 48 49	grpcld	$⊢ ((φ \land x \in B) \land y \in B) \to x +_{P} y \in B$
209		ovexd	$⊢ ((φ \land x \in B) \land y \in B) \to x (\emptyset) +_{R} y (\emptyset) \in V$
210	4 205 208 209	fvmptd2	$⊢ ((φ \land x \in B) \land y \in B) \to F (x +_{P} y) = x (\emptyset) +_{R} y (\emptyset)$
211	123 127	oveq12d	$⊢ ((φ \land x \in B) \land y \in B) \to F (x) +_{R} F (y) = x (\emptyset) +_{R} y (\emptyset)$
212	210 211	eqtr4d	$⊢ ((φ \land x \in B) \land y \in B) \to F (x +_{P} y) = F (x) +_{R} F (y)$
213	212	anasss	$⊢ (φ \land (x \in B \land y \in B)) \to F (x +_{P} y) = F (x) +_{R} F (y)$
214	1 5 6 7 8 11 3 45 135 19 136 137 189 213	isrhmd	$⊢ φ \to F \in (P RingHom R)$
215	1 19	isrim	$⊢ F \in (P RingIso R) \leftrightarrow (F \in (P RingHom R) \land F : B \underset{1-1 onto}{⟶} {Base}_{R})$
216	214 187 215	sylanbrc	$⊢ φ \to F \in (P RingIso R)$

Metamath Proof Explorer

Theorem 0mplrim

Proof