Metamath Proof Explorer

Theorem prjsperref

Description: The relation in PrjSp is reflexive. (Contributed by Steven Nguyen, 30-Apr-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 )
Assertion prjsperref 
|- ( V e. LMod -> ( X e. B <-> X .~ X ) )

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 oveq1 
 |-  ( m = ( 1r ` S ) -> ( m .x. X ) = ( ( 1r ` S ) .x. X ) )
7 6 eqeq2d 
 |-  ( m = ( 1r ` S ) -> ( X = ( m .x. X ) <-> X = ( ( 1r ` S ) .x. X ) ) )
8 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
9 3 5 8 lmod1cl 
 |-  ( V e. LMod -> ( 1r ` S ) e. K )
10 9 adantr 
 |-  ( ( V e. LMod /\ X e. B ) -> ( 1r ` S ) e. K )
11 eldifi 
 |-  ( X e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> X e. ( Base ` V ) )
12 11 2 eleq2s 
 |-  ( X e. B -> X e. ( Base ` V ) )
13 eqid 
 |-  ( Base ` V ) = ( Base ` V )
14 13 3 4 8 lmodvs1 
 |-  ( ( V e. LMod /\ X e. ( Base ` V ) ) -> ( ( 1r ` S ) .x. X ) = X )
15 12 14 sylan2 
 |-  ( ( V e. LMod /\ X e. B ) -> ( ( 1r ` S ) .x. X ) = X )
16 15 eqcomd 
 |-  ( ( V e. LMod /\ X e. B ) -> X = ( ( 1r ` S ) .x. X ) )
17 7 10 16 rspcedvdw 
 |-  ( ( V e. LMod /\ X e. B ) -> E. m e. K X = ( m .x. X ) )
18 17 ex 
 |-  ( V e. LMod -> ( X e. B -> E. m e. K X = ( m .x. X ) ) )
19 18 pm4.71d 
 |-  ( V e. LMod -> ( X e. B <-> ( X e. B /\ E. m e. K X = ( m .x. X ) ) ) )
20 pm4.24 
 |-  ( X e. B <-> ( X e. B /\ X e. B ) )
21 20 anbi1i 
 |-  ( ( X e. B /\ E. m e. K X = ( m .x. X ) ) <-> ( ( X e. B /\ X e. B ) /\ E. m e. K X = ( m .x. X ) ) )
22 1 prjsprel 
 |-  ( X .~ X <-> ( ( X e. B /\ X e. B ) /\ E. m e. K X = ( m .x. X ) ) )
23 21 22 bitr4i 
 |-  ( ( X e. B /\ E. m e. K X = ( m .x. X ) ) <-> X .~ X )
24 19 23 bitrdi 
 |-  ( V e. LMod -> ( X e. B <-> X .~ X ) )