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 3 lmodring 
 |-  ( V e. LMod -> S e. Ring )
23 22 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 )
24 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 )
25 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 )
26 eqid 
 |-  ( .r ` S ) = ( .r ` S )
27 5 26 ringcl 
 |-  ( ( S e. Ring /\ m e. K /\ n e. K ) -> ( m ( .r ` S ) n ) e. K )
28 23 24 25 27 syl3anc 
 |-  ( ( ( ( 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 )
29 oveq1 
 |-  ( o = ( m ( .r ` S ) n ) -> ( o .x. Z ) = ( ( m ( .r ` S ) n ) .x. Z ) )
30 29 eqeq2d 
 |-  ( o = ( m ( .r ` S ) n ) -> ( X = ( o .x. Z ) <-> X = ( ( m ( .r ` S ) n ) .x. Z ) ) )
31 30 adantl 
 |-  ( ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) /\ o = ( m ( .r ` S ) n ) ) -> ( X = ( o .x. Z ) <-> X = ( ( m ( .r ` S ) n ) .x. Z ) ) )
32 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 ) )
33 32 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 ) ) )
34 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 ) )
35 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 )
36 eldifi 
 |-  ( Z e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> Z e. ( Base ` V ) )
37 36 2 eleq2s 
 |-  ( Z e. B -> Z e. ( Base ` V ) )
38 21 37 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 ) )
39 eqid 
 |-  ( Base ` V ) = ( Base ` V )
40 39 3 4 5 26 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 ) ) )
41 35 24 25 38 40 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 ) ) )
42 33 34 41 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 ) )
43 28 31 42 rspcedvd 
 |-  ( ( ( ( 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 ) )
44 1 prjsprel 
 |-  ( X .~ Z <-> ( ( X e. B /\ Z e. B ) /\ E. o e. K X = ( o .x. Z ) ) )
45 17 21 43 44 syl21anbrc 
 |-  ( ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ ( n e. K /\ Y = ( n .x. Z ) ) ) -> X .~ Z )
46 12 45 rexlimddv 
 |-  ( ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> X .~ Z )
47 8 46 rexlimddv 
 |-  ( ( V e. LMod /\ ( X .~ Y /\ Y .~ Z ) ) -> X .~ Z )