Metamath Proof Explorer

Theorem prjspertr

Description: The relation in PrjSp is transitive. (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 prjspertr 
|- ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) -> X .~ Z )

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 1 prjsprel 
 |-  ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) )
7 6 simprbi 
 |-  ( X .~ Y -> E. m e. K X = ( m .x. Y ) )
8 7 ad2antrl 
 |-  ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) -> E. m e. K X = ( m .x. Y ) )
9 simplrr 
 |-  ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> Y .~ Z )
10 1 prjsprel 
 |-  ( Y .~ Z <-> ( ( Y e. B /\ Z e. B ) /\ E. n e. K Y = ( n .x. Z ) ) )
11 10 simprbi 
 |-  ( Y .~ Z -> E. n e. K Y = ( n .x. Z ) )
12 9 11 syl 
 |-  ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> E. n e. K Y = ( n .x. Z ) )
13 simplrl 
 |-  ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( ( m e. K /\ X = ( m .x. Y ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) ) -> X .~ Y )
14 13 anassrs 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> X .~ Y )
15 simpll 
 |-  ( ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) -> X e. B )
16 6 15 sylbi 
 |-  ( X .~ Y -> X e. B )
17 14 16 syl 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> X e. B )
18 9 adantr 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> Y .~ Z )
19 simplr 
 |-  ( ( ( Y e. B /\ Z e. B ) /\ E. n e. K Y = ( n .x. Z ) ) -> Z e. B )
20 10 19 sylbi 
 |-  ( Y .~ Z -> Z e. B )
21 18 20 syl 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> Z e. B )
22 oveq1 
 |-  ( o = ( m ( .r ` S ) n ) -> ( o .x. Z ) = ( ( m ( .r ` S ) n ) .x. Z ) )
23 22 eqeq2d 
 |-  ( o = ( m ( .r ` S ) n ) -> ( X = ( o .x. Z ) <-> X = ( ( m ( .r ` S ) n ) .x. Z ) ) )
24 eqid 
 |-  ( .r ` S ) = ( .r ` S )
25 3 lmodring 
 |-  ( V e. LMod -> S e. Ring )
26 25 ad3antrrr 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> S e. Ring )
27 simplrl 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> m e. K )
28 simprl 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> n e. K )
29 5 24 26 27 28 ringcld 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> ( m ( .r ` S ) n ) e. K )
30 simprr 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> Y = ( n .x. Z ) )
31 30 oveq2d 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> ( m .x. Y ) = ( m .x. ( n .x. Z ) ) )
32 simplrr 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> X = ( m .x. Y ) )
33 simplll 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> V e. LMod )
34 eldifi 
 |-  ( Z e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> Z e. ( Base ` V ) )
35 34 2 eleq2s 
 |-  ( Z e. B -> Z e. ( Base ` V ) )
36 21 35 syl 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> Z e. ( Base ` V ) )
37 eqid 
 |-  ( Base ` V ) = ( Base ` V )
38 37 3 4 5 24 lmodvsass 
 |-  ( ( V e. LMod /\ ( m e. K /\ n e. K /\ Z e. ( Base ` V ) ) ) -> ( ( m ( .r ` S ) n ) .x. Z ) = ( m .x. ( n .x. Z ) ) )
39 33 27 28 36 38 syl13anc 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> ( ( m ( .r ` S ) n ) .x. Z ) = ( m .x. ( n .x. Z ) ) )
40 31 32 39 3eqtr4d 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> X = ( ( m ( .r ` S ) n ) .x. Z ) )
41 23 29 40 rspcedvdw 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> E. o e. K X = ( o .x. Z ) )
42 1 prjsprel 
 |-  ( X .~ Z <-> ( ( X e. B /\ Z e. B ) /\ E. o e. K X = ( o .x. Z ) ) )
43 17 21 41 42 syl21anbrc 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> X .~ Z )
44 12 43 rexlimddv 
 |-  ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> X .~ Z )
45 8 44 rexlimddv 
 |-  ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) -> X .~ Z )