Metamath Proof Explorer

Theorem prjspner01

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

Ref Expression
Hypotheses prjspner01.e 
|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. S x = ( l .x. y ) ) }
prjspner01.f 
|- F = ( b e. B |-> if ( ( b ` 0 ) = .0. , b , ( ( I ` ( b ` 0 ) ) .x. b ) ) )
prjspner01.b 
|- B = ( ( Base ` W ) \ { ( 0g ` W ) } )
prjspner01.w 
|- W = ( K freeLMod ( 0 ... N ) )
prjspner01.t 
|- .x. = ( .s ` W )
prjspner01.s 
|- S = ( Base ` K )
prjspner01.0 
|- .0. = ( 0g ` K )
prjspner01.i 
|- I = ( invr ` K )
prjspner01.k 
|- ( ph -> K e. DivRing )
prjspner01.n 
|- ( ph -> N e. NN0 )
prjspner01.x 
|- ( ph -> X e. B )
Assertion prjspner01 
|- ( ph -> X .~ ( F ` X ) )

Proof

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