Metamath Proof Explorer

Theorem prjspeclsp

Description: The vectors equivalent to a vector X are the nonzero vectors in the span of X . (Contributed by Steven Nguyen, 6-Jun-2023)

Ref Expression
Hypotheses prjsprel.1 
|- .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
prjspertr.b 
|- B = ( ( Base ` V ) \ { ( 0g ` V ) } )
prjspertr.s 
|- S = ( Scalar ` V )
prjspertr.x 
|- .x. = ( .s ` V )
prjspertr.k 
|- K = ( Base ` S )
prjsprellsp.n 
|- N = ( LSpan ` V )
Assertion prjspeclsp 
|- ( ( V e. LVec /\ X e. B ) -> [ X ] .~ = ( ( N ` { X } ) \ { ( 0g ` V ) } ) )

Proof

Step Hyp Ref Expression
1 prjsprel.1 
 |-  .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
2 prjspertr.b 
 |-  B = ( ( Base ` V ) \ { ( 0g ` V ) } )
3 prjspertr.s 
 |-  S = ( Scalar ` V )
4 prjspertr.x 
 |-  .x. = ( .s ` V )
5 prjspertr.k 
 |-  K = ( Base ` S )
6 prjsprellsp.n 
 |-  N = ( LSpan ` V )
7 1 cnveqi 
 |-  `' .~ = `' { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
8 cnvopab 
 |-  `' { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } = { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
9 7 8 eqtri 
 |-  `' .~ = { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
10 9 eceq2i 
 |-  [ X ] `' .~ = [ X ] { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
11 df-ec 
 |-  [ X ] { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } = ( { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } " { X } )
12 11 a1i 
 |-  ( ( V e. LVec /\ X e. B ) -> [ X ] { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } = ( { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } " { X } ) )
13 imaopab 
 |-  ( { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } " { X } ) = { x | E. y e. { X } ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
14 13 a1i 
 |-  ( ( V e. LVec /\ X e. B ) -> ( { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } " { X } ) = { x | E. y e. { X } ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } )
15 df-rex 
 |-  ( E. y e. { X } ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) <-> E. y ( y e. { X } /\ ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) ) )
16 velsn 
 |-  ( y e. { X } <-> y = X )
17 16 anbi1i 
 |-  ( ( y e. { X } /\ ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) ) <-> ( y = X /\ ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) ) )
18 eleq1 
 |-  ( y = X -> ( y e. B <-> X e. B ) )
19 18 anbi2d 
 |-  ( y = X -> ( ( x e. B /\ y e. B ) <-> ( x e. B /\ X e. B ) ) )
20 oveq2 
 |-  ( y = X -> ( l .x. y ) = ( l .x. X ) )
21 20 eqeq2d 
 |-  ( y = X -> ( x = ( l .x. y ) <-> x = ( l .x. X ) ) )
22 21 rexbidv 
 |-  ( y = X -> ( E. l e. K x = ( l .x. y ) <-> E. l e. K x = ( l .x. X ) ) )
23 19 22 anbi12d 
 |-  ( y = X -> ( ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) <-> ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) ) )
24 23 pm5.32i 
 |-  ( ( y = X /\ ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) ) <-> ( y = X /\ ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) ) )
25 17 24 bitri 
 |-  ( ( y e. { X } /\ ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) ) <-> ( y = X /\ ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) ) )
26 25 exbii 
 |-  ( E. y ( y e. { X } /\ ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) ) <-> E. y ( y = X /\ ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) ) )
27 19.41v 
 |-  ( E. y ( y = X /\ ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) ) <-> ( E. y y = X /\ ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) ) )
28 elisset 
 |-  ( X e. B -> E. y y = X )
29 28 ad2antlr 
 |-  ( ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) -> E. y y = X )
30 29 pm4.71ri 
 |-  ( ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) <-> ( E. y y = X /\ ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) ) )
31 27 30 bitr4i 
 |-  ( E. y ( y = X /\ ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) ) <-> ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) )
32 15 26 31 3bitri 
 |-  ( E. y e. { X } ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) <-> ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) )
33 32 abbii 
 |-  { x | E. y e. { X } ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } = { x | ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) }
34 iba 
 |-  ( X e. B -> ( x e. B <-> ( x e. B /\ X e. B ) ) )
35 34 bicomd 
 |-  ( X e. B -> ( ( x e. B /\ X e. B ) <-> x e. B ) )
36 35 anbi1d 
 |-  ( X e. B -> ( ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) <-> ( x e. B /\ E. l e. K x = ( l .x. X ) ) ) )
37 36 abbidv 
 |-  ( X e. B -> { x | ( ( x e. B /\ X e. B ) /\ E. l e. K x = ( l .x. X ) ) } = { x | ( x e. B /\ E. l e. K x = ( l .x. X ) ) } )
38 33 37 syl5eq 
 |-  ( X e. B -> { x | E. y e. { X } ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } = { x | ( x e. B /\ E. l e. K x = ( l .x. X ) ) } )
39 38 adantl 
 |-  ( ( V e. LVec /\ X e. B ) -> { x | E. y e. { X } ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } = { x | ( x e. B /\ E. l e. K x = ( l .x. X ) ) } )
40 12 14 39 3eqtrd 
 |-  ( ( V e. LVec /\ X e. B ) -> [ X ] { <. y , x >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) } = { x | ( x e. B /\ E. l e. K x = ( l .x. X ) ) } )
41 10 40 syl5eq 
 |-  ( ( V e. LVec /\ X e. B ) -> [ X ] `' .~ = { x | ( x e. B /\ E. l e. K x = ( l .x. X ) ) } )
42 df-rab 
 |-  { x e. B | E. l e. K x = ( l .x. X ) } = { x | ( x e. B /\ E. l e. K x = ( l .x. X ) ) }
43 42 a1i 
 |-  ( ( V e. LVec /\ X e. B ) -> { x e. B | E. l e. K x = ( l .x. X ) } = { x | ( x e. B /\ E. l e. K x = ( l .x. X ) ) } )
44 2 rabeqi 
 |-  { x e. B | E. l e. K x = ( l .x. X ) } = { x e. ( ( Base ` V ) \ { ( 0g ` V ) } ) | E. l e. K x = ( l .x. X ) }
45 rabdif 
 |-  ( { x e. ( Base ` V ) | E. l e. K x = ( l .x. X ) } \ { ( 0g ` V ) } ) = { x e. ( ( Base ` V ) \ { ( 0g ` V ) } ) | E. l e. K x = ( l .x. X ) }
46 45 a1i 
 |-  ( ( V e. LVec /\ X e. B ) -> ( { x e. ( Base ` V ) | E. l e. K x = ( l .x. X ) } \ { ( 0g ` V ) } ) = { x e. ( ( Base ` V ) \ { ( 0g ` V ) } ) | E. l e. K x = ( l .x. X ) } )
47 44 46 eqtr4id 
 |-  ( ( V e. LVec /\ X e. B ) -> { x e. B | E. l e. K x = ( l .x. X ) } = ( { x e. ( Base ` V ) | E. l e. K x = ( l .x. X ) } \ { ( 0g ` V ) } ) )
48 41 43 47 3eqtr2d 
 |-  ( ( V e. LVec /\ X e. B ) -> [ X ] `' .~ = ( { x e. ( Base ` V ) | E. l e. K x = ( l .x. X ) } \ { ( 0g ` V ) } ) )
49 1 2 3 4 5 prjsper 
 |-  ( V e. LVec -> .~ Er B )
50 49 adantr 
 |-  ( ( V e. LVec /\ X e. B ) -> .~ Er B )
51 ercnv 
 |-  ( .~ Er B -> `' .~ = .~ )
52 51 eqcomd 
 |-  ( .~ Er B -> .~ = `' .~ )
53 50 52 syl 
 |-  ( ( V e. LVec /\ X e. B ) -> .~ = `' .~ )
54 53 eceq2d 
 |-  ( ( V e. LVec /\ X e. B ) -> [ X ] .~ = [ X ] `' .~ )
55 lveclmod 
 |-  ( V e. LVec -> V e. LMod )
56 difss 
 |-  ( ( Base ` V ) \ { ( 0g ` V ) } ) C_ ( Base ` V )
57 2 56 eqsstri 
 |-  B C_ ( Base ` V )
58 57 sseli 
 |-  ( X e. B -> X e. ( Base ` V ) )
59 eqid 
 |-  ( Base ` V ) = ( Base ` V )
60 3 5 59 4 6 lspsn 
 |-  ( ( V e. LMod /\ X e. ( Base ` V ) ) -> ( N ` { X } ) = { x | E. l e. K x = ( l .x. X ) } )
61 55 58 60 syl2an 
 |-  ( ( V e. LVec /\ X e. B ) -> ( N ` { X } ) = { x | E. l e. K x = ( l .x. X ) } )
62 simpr 
 |-  ( ( ( ( V e. LVec /\ X e. B ) /\ l e. K ) /\ x = ( l .x. X ) ) -> x = ( l .x. X ) )
63 55 adantr 
 |-  ( ( V e. LVec /\ X e. B ) -> V e. LMod )
64 63 adantr 
 |-  ( ( ( V e. LVec /\ X e. B ) /\ l e. K ) -> V e. LMod )
65 simpr 
 |-  ( ( ( V e. LVec /\ X e. B ) /\ l e. K ) -> l e. K )
66 58 ad2antlr 
 |-  ( ( ( V e. LVec /\ X e. B ) /\ l e. K ) -> X e. ( Base ` V ) )
67 59 3 4 5 lmodvscl 
 |-  ( ( V e. LMod /\ l e. K /\ X e. ( Base ` V ) ) -> ( l .x. X ) e. ( Base ` V ) )
68 64 65 66 67 syl3anc 
 |-  ( ( ( V e. LVec /\ X e. B ) /\ l e. K ) -> ( l .x. X ) e. ( Base ` V ) )
69 68 adantr 
 |-  ( ( ( ( V e. LVec /\ X e. B ) /\ l e. K ) /\ x = ( l .x. X ) ) -> ( l .x. X ) e. ( Base ` V ) )
70 62 69 eqeltrd 
 |-  ( ( ( ( V e. LVec /\ X e. B ) /\ l e. K ) /\ x = ( l .x. X ) ) -> x e. ( Base ` V ) )
71 70 rexlimdva2 
 |-  ( ( V e. LVec /\ X e. B ) -> ( E. l e. K x = ( l .x. X ) -> x e. ( Base ` V ) ) )
72 71 pm4.71rd 
 |-  ( ( V e. LVec /\ X e. B ) -> ( E. l e. K x = ( l .x. X ) <-> ( x e. ( Base ` V ) /\ E. l e. K x = ( l .x. X ) ) ) )
73 72 abbidv 
 |-  ( ( V e. LVec /\ X e. B ) -> { x | E. l e. K x = ( l .x. X ) } = { x | ( x e. ( Base ` V ) /\ E. l e. K x = ( l .x. X ) ) } )
74 df-rab 
 |-  { x e. ( Base ` V ) | E. l e. K x = ( l .x. X ) } = { x | ( x e. ( Base ` V ) /\ E. l e. K x = ( l .x. X ) ) }
75 73 74 eqtr4di 
 |-  ( ( V e. LVec /\ X e. B ) -> { x | E. l e. K x = ( l .x. X ) } = { x e. ( Base ` V ) | E. l e. K x = ( l .x. X ) } )
76 61 75 eqtrd 
 |-  ( ( V e. LVec /\ X e. B ) -> ( N ` { X } ) = { x e. ( Base ` V ) | E. l e. K x = ( l .x. X ) } )
77 76 difeq1d 
 |-  ( ( V e. LVec /\ X e. B ) -> ( ( N ` { X } ) \ { ( 0g ` V ) } ) = ( { x e. ( Base ` V ) | E. l e. K x = ( l .x. X ) } \ { ( 0g ` V ) } ) )
78 48 54 77 3eqtr4d 
 |-  ( ( V e. LVec /\ X e. B ) -> [ X ] .~ = ( ( N ` { X } ) \ { ( 0g ` V ) } ) )