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