# Metamath Proof Explorer

## Theorem mvrf1

Description: The power series variable function is injective if the base ring is nonzero. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses mvrf.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
mvrf.v ${⊢}{V}={I}\mathrm{mVar}{R}$
mvrf.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
mvrf.i ${⊢}{\phi }\to {I}\in {W}$
mvrf.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
mvrf1.z
mvrf1.o
mvrf1.n
Assertion mvrf1 ${⊢}{\phi }\to {V}:{I}\underset{1-1}{⟶}{B}$

### Proof

Step Hyp Ref Expression
1 mvrf.s ${⊢}{S}={I}\mathrm{mPwSer}{R}$
2 mvrf.v ${⊢}{V}={I}\mathrm{mVar}{R}$
3 mvrf.b ${⊢}{B}={\mathrm{Base}}_{{S}}$
4 mvrf.i ${⊢}{\phi }\to {I}\in {W}$
5 mvrf.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
6 mvrf1.z
7 mvrf1.o
8 mvrf1.n
9 1 2 3 4 5 mvrf ${⊢}{\phi }\to {V}:{I}⟶{B}$
11 simp2r ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to {V}\left({x}\right)={V}\left({y}\right)$
12 11 fveq1d ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to {V}\left({x}\right)\left(\left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)\right)={V}\left({y}\right)\left(\left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)\right)$
13 eqid ${⊢}\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}=\left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
14 4 3ad2ant1 ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to {I}\in {W}$
15 5 3ad2ant1 ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to {R}\in \mathrm{Ring}$
16 simp2ll ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to {x}\in {I}$
17 2 13 6 7 14 15 16 mvrid
18 simp2lr ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to {y}\in {I}$
19 1nn0 ${⊢}1\in {ℕ}_{0}$
20 13 snifpsrbag ${⊢}\left({I}\in {W}\wedge 1\in {ℕ}_{0}\right)\to \left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)\in \left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
21 14 19 20 sylancl ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to \left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)\in \left\{{h}\in \left({{ℕ}_{0}}^{{I}}\right)|{{h}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
22 2 13 6 7 14 15 18 21 mvrval2
23 12 17 22 3eqtr3d
24 simp3 ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to ¬{x}={y}$
25 mpteqb ${⊢}\forall {z}\in {I}\phantom{\rule{.4em}{0ex}}if\left({z}={x},1,0\right)\in {ℕ}_{0}\to \left(\left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)=\left({z}\in {I}⟼if\left({z}={y},1,0\right)\right)↔\forall {z}\in {I}\phantom{\rule{.4em}{0ex}}if\left({z}={x},1,0\right)=if\left({z}={y},1,0\right)\right)$
26 0nn0 ${⊢}0\in {ℕ}_{0}$
27 19 26 ifcli ${⊢}if\left({z}={x},1,0\right)\in {ℕ}_{0}$
28 27 a1i ${⊢}{z}\in {I}\to if\left({z}={x},1,0\right)\in {ℕ}_{0}$
29 25 28 mprg ${⊢}\left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)=\left({z}\in {I}⟼if\left({z}={y},1,0\right)\right)↔\forall {z}\in {I}\phantom{\rule{.4em}{0ex}}if\left({z}={x},1,0\right)=if\left({z}={y},1,0\right)$
30 iftrue ${⊢}{z}={x}\to if\left({z}={x},1,0\right)=1$
31 eqeq1 ${⊢}{z}={x}\to \left({z}={y}↔{x}={y}\right)$
32 31 ifbid ${⊢}{z}={x}\to if\left({z}={y},1,0\right)=if\left({x}={y},1,0\right)$
33 30 32 eqeq12d ${⊢}{z}={x}\to \left(if\left({z}={x},1,0\right)=if\left({z}={y},1,0\right)↔1=if\left({x}={y},1,0\right)\right)$
34 33 rspcv ${⊢}{x}\in {I}\to \left(\forall {z}\in {I}\phantom{\rule{.4em}{0ex}}if\left({z}={x},1,0\right)=if\left({z}={y},1,0\right)\to 1=if\left({x}={y},1,0\right)\right)$
35 29 34 syl5bi ${⊢}{x}\in {I}\to \left(\left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)=\left({z}\in {I}⟼if\left({z}={y},1,0\right)\right)\to 1=if\left({x}={y},1,0\right)\right)$
36 16 35 syl ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to \left(\left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)=\left({z}\in {I}⟼if\left({z}={y},1,0\right)\right)\to 1=if\left({x}={y},1,0\right)\right)$
37 ax-1ne0 ${⊢}1\ne 0$
38 eqeq1 ${⊢}1=if\left({x}={y},1,0\right)\to \left(1=0↔if\left({x}={y},1,0\right)=0\right)$
39 38 necon3abid ${⊢}1=if\left({x}={y},1,0\right)\to \left(1\ne 0↔¬if\left({x}={y},1,0\right)=0\right)$
40 37 39 mpbii ${⊢}1=if\left({x}={y},1,0\right)\to ¬if\left({x}={y},1,0\right)=0$
41 iffalse ${⊢}¬{x}={y}\to if\left({x}={y},1,0\right)=0$
42 40 41 nsyl2 ${⊢}1=if\left({x}={y},1,0\right)\to {x}={y}$
43 36 42 syl6 ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to \left(\left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)=\left({z}\in {I}⟼if\left({z}={y},1,0\right)\right)\to {x}={y}\right)$
44 24 43 mtod ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\wedge ¬{x}={y}\right)\to ¬\left({z}\in {I}⟼if\left({z}={x},1,0\right)\right)=\left({z}\in {I}⟼if\left({z}={y},1,0\right)\right)$
45 iffalse
46 44 45 syl
47 23 46 eqtrd
48 47 3expia
50 10 49 mpd ${⊢}\left({\phi }\wedge \left(\left({x}\in {I}\wedge {y}\in {I}\right)\wedge {V}\left({x}\right)={V}\left({y}\right)\right)\right)\to {x}={y}$
51 50 expr ${⊢}\left({\phi }\wedge \left({x}\in {I}\wedge {y}\in {I}\right)\right)\to \left({V}\left({x}\right)={V}\left({y}\right)\to {x}={y}\right)$
52 51 ralrimivva ${⊢}{\phi }\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({V}\left({x}\right)={V}\left({y}\right)\to {x}={y}\right)$
53 dff13 ${⊢}{V}:{I}\underset{1-1}{⟶}{B}↔\left({V}:{I}⟶{B}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({V}\left({x}\right)={V}\left({y}\right)\to {x}={y}\right)\right)$
54 9 52 53 sylanbrc ${⊢}{\phi }\to {V}:{I}\underset{1-1}{⟶}{B}$