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 mPwSer R
mvrf.v V = I mVar R
mvrf.b B = Base S
mvrf.i φ I W
mvrf.r φ R Ring
mvrf1.z 0 ˙ = 0 R
mvrf1.o 1 ˙ = 1 R
mvrf1.n φ 1 ˙ 0 ˙
Assertion mvrf1 φ V : I 1-1 B

Proof

Step Hyp Ref Expression
1 mvrf.s S = I mPwSer R
2 mvrf.v V = I mVar R
3 mvrf.b B = Base S
4 mvrf.i φ I W
5 mvrf.r φ R Ring
6 mvrf1.z 0 ˙ = 0 R
7 mvrf1.o 1 ˙ = 1 R
8 mvrf1.n φ 1 ˙ 0 ˙
9 1 2 3 4 5 mvrf φ V : I B
10 8 adantr φ x I y I V x = V y 1 ˙ 0 ˙
11 simp2r φ x I y I V x = V y ¬ x = y V x = V y
12 11 fveq1d φ x I y I V x = V y ¬ x = y V x z I if z = x 1 0 = V y z I if z = x 1 0
13 eqid h 0 I | h -1 Fin = h 0 I | h -1 Fin
14 4 3ad2ant1 φ x I y I V x = V y ¬ x = y I W
15 5 3ad2ant1 φ x I y I V x = V y ¬ x = y R Ring
16 simp2ll φ x I y I V x = V y ¬ x = y x I
17 2 13 6 7 14 15 16 mvrid φ x I y I V x = V y ¬ x = y V x z I if z = x 1 0 = 1 ˙
18 simp2lr φ x I y I V x = V y ¬ x = y y I
19 1nn0 1 0
20 13 snifpsrbag I W 1 0 z I if z = x 1 0 h 0 I | h -1 Fin
21 14 19 20 sylancl φ x I y I V x = V y ¬ x = y z I if z = x 1 0 h 0 I | h -1 Fin
22 2 13 6 7 14 15 18 21 mvrval2 φ x I y I V x = V y ¬ x = y V y z I if z = x 1 0 = if z I if z = x 1 0 = z I if z = y 1 0 1 ˙ 0 ˙
23 12 17 22 3eqtr3d φ x I y I V x = V y ¬ x = y 1 ˙ = if z I if z = x 1 0 = z I if z = y 1 0 1 ˙ 0 ˙
24 simp3 φ x I y I V x = V y ¬ x = y ¬ x = y
25 mpteqb z I if z = x 1 0 0 z I if z = x 1 0 = z I if z = y 1 0 z I if z = x 1 0 = if z = y 1 0
26 0nn0 0 0
27 19 26 ifcli if z = x 1 0 0
28 27 a1i z I if z = x 1 0 0
29 25 28 mprg z I if z = x 1 0 = z I if z = y 1 0 z I if z = x 1 0 = if z = y 1 0
30 iftrue z = x if z = x 1 0 = 1
31 eqeq1 z = x z = y x = y
32 31 ifbid z = x if z = y 1 0 = if x = y 1 0
33 30 32 eqeq12d z = x if z = x 1 0 = if z = y 1 0 1 = if x = y 1 0
34 33 rspcv x I z I if z = x 1 0 = if z = y 1 0 1 = if x = y 1 0
35 29 34 syl5bi x I z I if z = x 1 0 = z I if z = y 1 0 1 = if x = y 1 0
36 16 35 syl φ x I y I V x = V y ¬ x = y z I if z = x 1 0 = z I if z = y 1 0 1 = if x = y 1 0
37 ax-1ne0 1 0
38 eqeq1 1 = if x = y 1 0 1 = 0 if x = y 1 0 = 0
39 38 necon3abid 1 = if x = y 1 0 1 0 ¬ if x = y 1 0 = 0
40 37 39 mpbii 1 = if x = y 1 0 ¬ if x = y 1 0 = 0
41 iffalse ¬ x = y if x = y 1 0 = 0
42 40 41 nsyl2 1 = if x = y 1 0 x = y
43 36 42 syl6 φ x I y I V x = V y ¬ x = y z I if z = x 1 0 = z I if z = y 1 0 x = y
44 24 43 mtod φ x I y I V x = V y ¬ x = y ¬ z I if z = x 1 0 = z I if z = y 1 0
45 iffalse ¬ z I if z = x 1 0 = z I if z = y 1 0 if z I if z = x 1 0 = z I if z = y 1 0 1 ˙ 0 ˙ = 0 ˙
46 44 45 syl φ x I y I V x = V y ¬ x = y if z I if z = x 1 0 = z I if z = y 1 0 1 ˙ 0 ˙ = 0 ˙
47 23 46 eqtrd φ x I y I V x = V y ¬ x = y 1 ˙ = 0 ˙
48 47 3expia φ x I y I V x = V y ¬ x = y 1 ˙ = 0 ˙
49 48 necon1ad φ x I y I V x = V y 1 ˙ 0 ˙ x = y
50 10 49 mpd φ x I y I V x = V y x = y
51 50 expr φ x I y I V x = V y x = y
52 51 ralrimivva φ x I y I V x = V y x = y
53 dff13 V : I 1-1 B V : I B x I y I V x = V y x = y
54 9 52 53 sylanbrc φ V : I 1-1 B