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	$$⊢\underset{\dot{}}{0}=0_R$$
	mvrf1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mvrf1.n	$$⊢\phi \to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
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	$$⊢\underset{\dot{}}{0}=0_R$$
7		mvrf1.o	$$⊢\underset{\dot{}}{1}=1_R$$
8		mvrf1.n	$$⊢\phi \to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
9	1 2 3 4 5	mvrf	$$⊢\phi \to V:I⟶B$$
10	8	adantr	$$⊢\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 \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
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 \neg 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 \neg 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({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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 \neg 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 \neg 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 \neg x=y\right)\to x\in I$$
17	2 13 6 7 14 15 16	mvrid	$$⊢\left(\phi \wedge \left(\left(x\in I\wedge y\in I\right)\wedge V\left(x\right)=V\left(y\right)\right)\wedge \neg x=y\right)\to V\left(x\right)\left(\left(z\in I⟼if\left(z=x,1,0\right)\right)\right)=\underset{\dot{}}{1}$$
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 \neg x=y\right)\to y\in I$$
19		1nn0	$$⊢1\in {\mathbb{N}}_0$$
20	13	snifpsrbag	$$⊢\left(I\in W\wedge 1\in {\mathbb{N}}_0\right)\to \left(z\in I⟼if\left(z=x,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\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 \neg x=y\right)\to \left(z\in I⟼if\left(z=x,1,0\right)\right)\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
22	2 13 6 7 14 15 18 21	mvrval2	$$⊢\left(\phi \wedge \left(\left(x\in I\wedge y\in I\right)\wedge V\left(x\right)=V\left(y\right)\right)\wedge \neg x=y\right)\to V\left(y\right)\left(\left(z\in I⟼if\left(z=x,1,0\right)\right)\right)=if\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),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
23	12 17 22	3eqtr3d	$$⊢\left(\phi \wedge \left(\left(x\in I\wedge y\in I\right)\wedge V\left(x\right)=V\left(y\right)\right)\wedge \neg x=y\right)\to \underset{\dot{}}{1}=if\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),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
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 \neg x=y\right)\to \neg x=y$$
25		mpteqb	$$⊢\forall z\in Iif\left(z=x,1,0\right)\in {\mathbb{N}}_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)\leftrightarrow \forall z\in Iif\left(z=x,1,0\right)=if\left(z=y,1,0\right)\right)$$
26		0nn0	$$⊢0\in {\mathbb{N}}_0$$
27	19 26	ifcli	$$⊢if\left(z=x,1,0\right)\in {\mathbb{N}}_0$$
28	27	a1i	$$⊢z\in I\to if\left(z=x,1,0\right)\in {\mathbb{N}}_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)\leftrightarrow \forall z\in Iif\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\leftrightarrow 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)\leftrightarrow 1=if\left(x=y,1,0\right)\right)$$
34	33	rspcv	$$⊢x\in I\to \left(\forall z\in Iif\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 \neg 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\leftrightarrow 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\leftrightarrow \neg if\left(x=y,1,0\right)=0\right)$$
40	37 39	mpbii	$$⊢1=if\left(x=y,1,0\right)\to \neg if\left(x=y,1,0\right)=0$$
41		iffalse	$$⊢\neg 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 \neg 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 \neg x=y\right)\to \neg \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	$$⊢\neg \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 if\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),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
46	44 45	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 \neg x=y\right)\to if\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),\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
47	23 46	eqtrd	$$⊢\left(\phi \wedge \left(\left(x\in I\wedge y\in I\right)\wedge V\left(x\right)=V\left(y\right)\right)\wedge \neg x=y\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
48	47	3expia	$$⊢\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 \left(\neg x=y\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
49	48	necon1ad	$$⊢\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 \left(\underset{\dot{}}{1}\ne \underset{\dot{}}{0}\to x=y\right)$$
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\forall y\in I\left(V\left(x\right)=V\left(y\right)\to x=y\right)$$
53		dff13	$$⊢V:I\underset{1-1}{⟶}B\leftrightarrow \left(V:I⟶B\wedge \forall x\in I\forall y\in I\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$$