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 
|- ( ph -> I e. W )
mvrf.r 
|- ( ph -> R e. Ring )
mvrf1.z 
|- .0. = ( 0g ` R )
mvrf1.o 
|- .1. = ( 1r ` R )
mvrf1.n 
|- ( ph -> .1. =/= .0. )
Assertion mvrf1 
|- ( ph -> 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 
 |-  ( ph -> I e. W )
5 mvrf.r 
 |-  ( ph -> R e. Ring )
6 mvrf1.z 
 |-  .0. = ( 0g ` R )
7 mvrf1.o 
 |-  .1. = ( 1r ` R )
8 mvrf1.n 
 |-  ( ph -> .1. =/= .0. )
9 1 2 3 4 5 mvrf 
 |-  ( ph -> V : I --> B )
10 8 adantr 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) ) -> .1. =/= .0. )
11 simp2r 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> ( V ` x ) = ( V ` y ) )
12 11 fveq1d 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> ( ( V ` x ) ` ( z e. I |-> if ( z = x , 1 , 0 ) ) ) = ( ( V ` y ) ` ( z e. I |-> if ( z = x , 1 , 0 ) ) ) )
13 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
14 4 3ad2ant1 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> I e. W )
15 5 3ad2ant1 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> R e. Ring )
16 simp2ll 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> x e. I )
17 2 13 6 7 14 15 16 mvrid 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> ( ( V ` x ) ` ( z e. I |-> if ( z = x , 1 , 0 ) ) ) = .1. )
18 simp2lr 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> y e. I )
19 1nn0 
 |-  1 e. NN0
20 13 snifpsrbag 
 |-  ( ( I e. W /\ 1 e. NN0 ) -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
21 14 19 20 sylancl 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
22 2 13 6 7 14 15 18 21 mvrval2 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> ( ( V ` y ) ` ( z e. I |-> if ( z = x , 1 , 0 ) ) ) = if ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) , .1. , .0. ) )
23 12 17 22 3eqtr3d 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> .1. = if ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) , .1. , .0. ) )
24 simp3 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> -. x = y )
25 mpteqb 
 |-  ( A. z e. I if ( z = x , 1 , 0 ) e. NN0 -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) <-> A. z e. I if ( z = x , 1 , 0 ) = if ( z = y , 1 , 0 ) ) )
26 0nn0 
 |-  0 e. NN0
27 19 26 ifcli 
 |-  if ( z = x , 1 , 0 ) e. NN0
28 27 a1i 
 |-  ( z e. I -> if ( z = x , 1 , 0 ) e. NN0 )
29 25 28 mprg 
 |-  ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) <-> A. z e. 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 e. I -> ( A. z e. I if ( z = x , 1 , 0 ) = if ( z = y , 1 , 0 ) -> 1 = if ( x = y , 1 , 0 ) ) )
35 29 34 syl5bi 
 |-  ( x e. I -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) -> 1 = if ( x = y , 1 , 0 ) ) )
36 16 35 syl 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. 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 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) -> x = y ) )
44 24 43 mtod 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> -. ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) )
45 iffalse 
 |-  ( -. ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) -> if ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) , .1. , .0. ) = .0. )
46 44 45 syl 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> if ( ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = y , 1 , 0 ) ) , .1. , .0. ) = .0. )
47 23 46 eqtrd 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) /\ -. x = y ) -> .1. = .0. )
48 47 3expia 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) ) -> ( -. x = y -> .1. = .0. ) )
49 48 necon1ad 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) ) -> ( .1. =/= .0. -> x = y ) )
50 10 49 mpd 
 |-  ( ( ph /\ ( ( x e. I /\ y e. I ) /\ ( V ` x ) = ( V ` y ) ) ) -> x = y )
51 50 expr 
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> ( ( V ` x ) = ( V ` y ) -> x = y ) )
52 51 ralrimivva 
 |-  ( ph -> A. x e. I A. y e. I ( ( V ` x ) = ( V ` y ) -> x = y ) )
53 dff13 
 |-  ( V : I -1-1-> B <-> ( V : I --> B /\ A. x e. I A. y e. I ( ( V ` x ) = ( V ` y ) -> x = y ) ) )
54 9 52 53 sylanbrc 
 |-  ( ph -> V : I -1-1-> B )