Metamath Proof Explorer

Theorem prjsprellsp

Description: Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-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 prjsprellsp 
|- ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( X .~ Y <-> ( N ` { X } ) = ( N ` { Y } ) ) )

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 ibar 
 |-  ( ( X e. B /\ Y e. B ) -> ( E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) ) ) )
8 7 bicomd 
 |-  ( ( X e. B /\ Y e. B ) -> ( ( ( X e. B /\ Y e. B ) /\ E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) ) <-> E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) ) )
9 8 adantl 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( ( ( X e. B /\ Y e. B ) /\ E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) ) <-> E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) ) )
10 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
11 1 2 3 4 5 10 prjspreln0 
 |-  ( V e. LVec -> ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) ) ) )
12 11 adantr 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) ) ) )
13 eqid 
 |-  ( Base ` V ) = ( Base ` V )
14 simpl 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> V e. LVec )
15 eldifi 
 |-  ( X e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> X e. ( Base ` V ) )
16 15 2 eleq2s 
 |-  ( X e. B -> X e. ( Base ` V ) )
17 16 ad2antrl 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> X e. ( Base ` V ) )
18 eldifi 
 |-  ( Y e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> Y e. ( Base ` V ) )
19 18 2 eleq2s 
 |-  ( Y e. B -> Y e. ( Base ` V ) )
20 19 ad2antll 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> Y e. ( Base ` V ) )
21 13 3 5 10 4 6 14 17 20 lspsneq 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( ( N ` { X } ) = ( N ` { Y } ) <-> E. m e. ( K \ { ( 0g ` S ) } ) X = ( m .x. Y ) ) )
22 9 12 21 3bitr4d 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( X .~ Y <-> ( N ` { X } ) = ( N ` { Y } ) ) )