Metamath Proof Explorer

Theorem prjspersym

Description: The relation in PrjSp is symmetric. (Contributed by Steven Nguyen, 1-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 )
Assertion prjspersym 
|- ( ( V e. LVec /\ X .~ Y ) -> Y .~ 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 simpllr 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> X .~ Y )
7 1 prjsprel 
 |-  ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) )
8 pm3.22 
 |-  ( ( X e. B /\ Y e. B ) -> ( Y e. B /\ X e. B ) )
9 8 adantr 
 |-  ( ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) -> ( Y e. B /\ X e. B ) )
10 7 9 sylbi 
 |-  ( X .~ Y -> ( Y e. B /\ X e. B ) )
11 6 10 syl 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> ( Y e. B /\ X e. B ) )
12 oveq1 
 |-  ( n = ( ( invr ` S ) ` m ) -> ( n .x. X ) = ( ( ( invr ` S ) ` m ) .x. X ) )
13 12 eqeq2d 
 |-  ( n = ( ( invr ` S ) ` m ) -> ( Y = ( n .x. X ) <-> Y = ( ( ( invr ` S ) ` m ) .x. X ) ) )
14 simplll 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> V e. LVec )
15 3 lvecdrng 
 |-  ( V e. LVec -> S e. DivRing )
16 14 15 syl 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> S e. DivRing )
17 simplr 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> m e. K )
18 simpll 
 |-  ( ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) -> X e. B )
19 7 18 sylbi 
 |-  ( X .~ Y -> X e. B )
20 eldifsni 
 |-  ( X e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> X =/= ( 0g ` V ) )
21 20 2 eleq2s 
 |-  ( X e. B -> X =/= ( 0g ` V ) )
22 6 19 21 3syl 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> X =/= ( 0g ` V ) )
23 simplr 
 |-  ( ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) /\ m = ( 0g ` S ) ) -> X = ( m .x. Y ) )
24 simpr 
 |-  ( ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) /\ m = ( 0g ` S ) ) -> m = ( 0g ` S ) )
25 24 oveq1d 
 |-  ( ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) /\ m = ( 0g ` S ) ) -> ( m .x. Y ) = ( ( 0g ` S ) .x. Y ) )
26 lveclmod 
 |-  ( V e. LVec -> V e. LMod )
27 26 ad4antr 
 |-  ( ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) /\ m = ( 0g ` S ) ) -> V e. LMod )
28 simplr 
 |-  ( ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) -> Y e. B )
29 7 28 sylbi 
 |-  ( X .~ Y -> Y e. B )
30 eldifi 
 |-  ( Y e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> Y e. ( Base ` V ) )
31 30 2 eleq2s 
 |-  ( Y e. B -> Y e. ( Base ` V ) )
32 6 29 31 3syl 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> Y e. ( Base ` V ) )
33 32 adantr 
 |-  ( ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) /\ m = ( 0g ` S ) ) -> Y e. ( Base ` V ) )
34 eqid 
 |-  ( Base ` V ) = ( Base ` V )
35 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
36 eqid 
 |-  ( 0g ` V ) = ( 0g ` V )
37 34 3 4 35 36 lmod0vs 
 |-  ( ( V e. LMod /\ Y e. ( Base ` V ) ) -> ( ( 0g ` S ) .x. Y ) = ( 0g ` V ) )
38 27 33 37 syl2anc 
 |-  ( ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) /\ m = ( 0g ` S ) ) -> ( ( 0g ` S ) .x. Y ) = ( 0g ` V ) )
39 23 25 38 3eqtrd 
 |-  ( ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) /\ m = ( 0g ` S ) ) -> X = ( 0g ` V ) )
40 22 39 mteqand 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> m =/= ( 0g ` S ) )
41 eqid 
 |-  ( invr ` S ) = ( invr ` S )
42 5 35 41 drnginvrcl 
 |-  ( ( S e. DivRing /\ m e. K /\ m =/= ( 0g ` S ) ) -> ( ( invr ` S ) ` m ) e. K )
43 16 17 40 42 syl3anc 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> ( ( invr ` S ) ` m ) e. K )
44 simpr 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> X = ( m .x. Y ) )
45 nelsn 
 |-  ( m =/= ( 0g ` S ) -> -. m e. { ( 0g ` S ) } )
46 40 45 syl 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> -. m e. { ( 0g ` S ) } )
47 17 46 eldifd 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> m e. ( K \ { ( 0g ` S ) } ) )
48 eldifi 
 |-  ( X e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> X e. ( Base ` V ) )
49 48 2 eleq2s 
 |-  ( X e. B -> X e. ( Base ` V ) )
50 6 19 49 3syl 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> X e. ( Base ` V ) )
51 34 4 3 5 35 41 14 47 50 32 lvecinv 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> ( X = ( m .x. Y ) <-> Y = ( ( ( invr ` S ) ` m ) .x. X ) ) )
52 44 51 mpbid 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> Y = ( ( ( invr ` S ) ` m ) .x. X ) )
53 13 43 52 rspcedvdw 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> E. n e. K Y = ( n .x. X ) )
54 1 prjsprel 
 |-  ( Y .~ X <-> ( ( Y e. B /\ X e. B ) /\ E. n e. K Y = ( n .x. X ) ) )
55 11 53 54 sylanbrc 
 |-  ( ( ( ( V e. LVec /\ X .~ Y ) /\ m e. K ) /\ X = ( m .x. Y ) ) -> Y .~ X )
56 simpr 
 |-  ( ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) -> E. m e. K X = ( m .x. Y ) )
57 7 56 sylbi 
 |-  ( X .~ Y -> E. m e. K X = ( m .x. Y ) )
58 57 adantl 
 |-  ( ( V e. LVec /\ X .~ Y ) -> E. m e. K X = ( m .x. Y ) )
59 55 58 r19.29a 
 |-  ( ( V e. LVec /\ X .~ Y ) -> Y .~ X )