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