Metamath Proof Explorer

Theorem prjspnfv01

Description: Any vector is equivalent to a vector whose zeroth coordinate is .0. or .1. (proof of the value of the zeroth coordinate). (Contributed by SN, 13-Aug-2023)

Ref Expression
Hypotheses prjspnfv01.f 
|- F = ( b e. B |-> if ( ( b ` 0 ) = .0. , b , ( ( I ` ( b ` 0 ) ) .x. b ) ) )
prjspnfv01.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
prjspnfv01.w 
|- W = ( K freeLMod ( 0 ... N ) )
prjspnfv01.t 
|- .x. = ( .s ` W )
prjspnfv01.0 
|- .0. = ( 0g ` K )
prjspnfv01.1 
|- .1. = ( 1r ` K )
prjspnfv01.i 
|- I = ( invr ` K )
prjspnfv01.k 
|- ( ph -> K e. DivRing )
prjspnfv01.n 
|- ( ph -> N e. NN0 )
prjspnfv01.x 
|- ( ph -> X e. B )
Assertion prjspnfv01 
|- ( ph -> ( ( F ` X ) ` 0 ) = if ( ( X ` 0 ) = .0. , .0. , .1. ) )

Proof

Step Hyp Ref Expression
1 prjspnfv01.f 
 |-  F = ( b e. B |-> if ( ( b ` 0 ) = .0. , b , ( ( I ` ( b ` 0 ) ) .x. b ) ) )
2 prjspnfv01.b 
 |-  B = ( ( Base ` W ) \ { ( 0g ` W ) } )
3 prjspnfv01.w 
 |-  W = ( K freeLMod ( 0 ... N ) )
4 prjspnfv01.t 
 |-  .x. = ( .s ` W )
5 prjspnfv01.0 
 |-  .0. = ( 0g ` K )
6 prjspnfv01.1 
 |-  .1. = ( 1r ` K )
7 prjspnfv01.i 
 |-  I = ( invr ` K )
8 prjspnfv01.k 
 |-  ( ph -> K e. DivRing )
9 prjspnfv01.n 
 |-  ( ph -> N e. NN0 )
10 prjspnfv01.x 
 |-  ( ph -> X e. B )
11 fveq1 
 |-  ( b = X -> ( b ` 0 ) = ( X ` 0 ) )
12 11 eqeq1d 
 |-  ( b = X -> ( ( b ` 0 ) = .0. <-> ( X ` 0 ) = .0. ) )
13 id 
 |-  ( b = X -> b = X )
14 11 fveq2d 
 |-  ( b = X -> ( I ` ( b ` 0 ) ) = ( I ` ( X ` 0 ) ) )
15 14 13 oveq12d 
 |-  ( b = X -> ( ( I ` ( b ` 0 ) ) .x. b ) = ( ( I ` ( X ` 0 ) ) .x. X ) )
16 12 13 15 ifbieq12d 
 |-  ( b = X -> if ( ( b ` 0 ) = .0. , b , ( ( I ` ( b ` 0 ) ) .x. b ) ) = if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) )
17 ovexd 
 |-  ( ph -> ( ( I ` ( X ` 0 ) ) .x. X ) e. _V )
18 10 17 ifexd 
 |-  ( ph -> if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) e. _V )
19 1 16 10 18 fvmptd3 
 |-  ( ph -> ( F ` X ) = if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) )
20 19 fveq1d 
 |-  ( ph -> ( ( F ` X ) ` 0 ) = ( if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) ` 0 ) )
21 iffv 
 |-  ( if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) ` 0 ) = if ( ( X ` 0 ) = .0. , ( X ` 0 ) , ( ( ( I ` ( X ` 0 ) ) .x. X ) ` 0 ) )
22 21 a1i 
 |-  ( ph -> ( if ( ( X ` 0 ) = .0. , X , ( ( I ` ( X ` 0 ) ) .x. X ) ) ` 0 ) = if ( ( X ` 0 ) = .0. , ( X ` 0 ) , ( ( ( I ` ( X ` 0 ) ) .x. X ) ` 0 ) ) )
23 simpr 
 |-  ( ( ph /\ ( X ` 0 ) = .0. ) -> ( X ` 0 ) = .0. )
24 eqid 
 |-  ( Base ` W ) = ( Base ` W )
25 eqid 
 |-  ( Base ` K ) = ( Base ` K )
26 ovexd 
 |-  ( ( ph /\ -. ( X ` 0 ) = .0. ) -> ( 0 ... N ) e. _V )
27 ovexd 
 |-  ( ph -> ( 0 ... N ) e. _V )
28 10 2 eleqtrdi 
 |-  ( ph -> X e. ( ( Base ` W ) \ { ( 0g ` W ) } ) )
29 28 eldifad 
 |-  ( ph -> X e. ( Base ` W ) )
30 3 25 24 frlmbasf 
 |-  ( ( ( 0 ... N ) e. _V /\ X e. ( Base ` W ) ) -> X : ( 0 ... N ) --> ( Base ` K ) )
31 27 29 30 syl2anc 
 |-  ( ph -> X : ( 0 ... N ) --> ( Base ` K ) )
32 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
33 9 32 syl 
 |-  ( ph -> 0 e. ( 0 ... N ) )
34 31 33 ffvelcdmd 
 |-  ( ph -> ( X ` 0 ) e. ( Base ` K ) )
35 neqne 
 |-  ( -. ( X ` 0 ) = .0. -> ( X ` 0 ) =/= .0. )
36 25 5 7 drnginvrcl 
 |-  ( ( K e. DivRing /\ ( X ` 0 ) e. ( Base ` K ) /\ ( X ` 0 ) =/= .0. ) -> ( I ` ( X ` 0 ) ) e. ( Base ` K ) )
37 8 34 35 36 syl2an3an 
 |-  ( ( ph /\ -. ( X ` 0 ) = .0. ) -> ( I ` ( X ` 0 ) ) e. ( Base ` K ) )
38 29 adantr 
 |-  ( ( ph /\ -. ( X ` 0 ) = .0. ) -> X e. ( Base ` W ) )
39 33 adantr 
 |-  ( ( ph /\ -. ( X ` 0 ) = .0. ) -> 0 e. ( 0 ... N ) )
40 eqid 
 |-  ( .r ` K ) = ( .r ` K )
41 3 24 25 26 37 38 39 4 40 frlmvscaval 
 |-  ( ( ph /\ -. ( X ` 0 ) = .0. ) -> ( ( ( I ` ( X ` 0 ) ) .x. X ) ` 0 ) = ( ( I ` ( X ` 0 ) ) ( .r ` K ) ( X ` 0 ) ) )
42 25 5 40 6 7 drnginvrl 
 |-  ( ( K e. DivRing /\ ( X ` 0 ) e. ( Base ` K ) /\ ( X ` 0 ) =/= .0. ) -> ( ( I ` ( X ` 0 ) ) ( .r ` K ) ( X ` 0 ) ) = .1. )
43 8 34 35 42 syl2an3an 
 |-  ( ( ph /\ -. ( X ` 0 ) = .0. ) -> ( ( I ` ( X ` 0 ) ) ( .r ` K ) ( X ` 0 ) ) = .1. )
44 41 43 eqtrd 
 |-  ( ( ph /\ -. ( X ` 0 ) = .0. ) -> ( ( ( I ` ( X ` 0 ) ) .x. X ) ` 0 ) = .1. )
45 23 44 ifeq12da 
 |-  ( ph -> if ( ( X ` 0 ) = .0. , ( X ` 0 ) , ( ( ( I ` ( X ` 0 ) ) .x. X ) ` 0 ) ) = if ( ( X ` 0 ) = .0. , .0. , .1. ) )
46 20 22 45 3eqtrd 
 |-  ( ph -> ( ( F ` X ) ` 0 ) = if ( ( X ` 0 ) = .0. , .0. , .1. ) )