This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqgvscpbl

Description: The left coset equivalence relation is compatible with the scalar multiplication operation. (Contributed by Thierry Arnoux, 18-May-2023)

Ref Expression
Hypotheses eqgvscpbl.v 
|- B = ( Base ` M )
eqgvscpbl.e 
|- .~ = ( M ~QG G )
eqgvscpbl.s 
|- S = ( Base ` ( Scalar ` M ) )
eqgvscpbl.p 
|- .x. = ( .s ` M )
eqgvscpbl.m 
|- ( ph -> M e. LMod )
eqgvscpbl.g 
|- ( ph -> G e. ( LSubSp ` M ) )
eqgvscpbl.k 
|- ( ph -> K e. S )
Assertion eqgvscpbl 
|- ( ph -> ( X .~ Y -> ( K .x. X ) .~ ( K .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 eqgvscpbl.v 
 |-  B = ( Base ` M )
2 eqgvscpbl.e 
 |-  .~ = ( M ~QG G )
3 eqgvscpbl.s 
 |-  S = ( Base ` ( Scalar ` M ) )
4 eqgvscpbl.p 
 |-  .x. = ( .s ` M )
5 eqgvscpbl.m 
 |-  ( ph -> M e. LMod )
6 eqgvscpbl.g 
 |-  ( ph -> G e. ( LSubSp ` M ) )
7 eqgvscpbl.k 
 |-  ( ph -> K e. S )
8 5 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> M e. LMod )
9 7 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> K e. S )
10 simpr1 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> X e. B )
11 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
12 1 11 4 3 lmodvscl 
 |-  ( ( M e. LMod /\ K e. S /\ X e. B ) -> ( K .x. X ) e. B )
13 8 9 10 12 syl3anc 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. X ) e. B )
14 simpr2 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> Y e. B )
15 1 11 4 3 lmodvscl 
 |-  ( ( M e. LMod /\ K e. S /\ Y e. B ) -> ( K .x. Y ) e. B )
16 8 9 14 15 syl3anc 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. Y ) e. B )
17 5 ad2antrr 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> M e. LMod )
18 7 ad2antrr 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> K e. S )
19 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
20 17 19 syl 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> M e. Grp )
21 simplr 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> X e. B )
22 eqid 
 |-  ( invg ` M ) = ( invg ` M )
23 1 22 grpinvcl 
 |-  ( ( M e. Grp /\ X e. B ) -> ( ( invg ` M ) ` X ) e. B )
24 20 21 23 syl2anc 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( ( invg ` M ) ` X ) e. B )
25 simpr 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> Y e. B )
26 eqid 
 |-  ( +g ` M ) = ( +g ` M )
27 1 26 11 4 3 lmodvsdi 
 |-  ( ( M e. LMod /\ ( K e. S /\ ( ( invg ` M ) ` X ) e. B /\ Y e. B ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( K .x. ( ( invg ` M ) ` X ) ) ( +g ` M ) ( K .x. Y ) ) )
28 17 18 24 25 27 syl13anc 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( K .x. ( ( invg ` M ) ` X ) ) ( +g ` M ) ( K .x. Y ) ) )
29 1 11 4 22 3 lmodvsinv2 
 |-  ( ( M e. LMod /\ K e. S /\ X e. B ) -> ( K .x. ( ( invg ` M ) ` X ) ) = ( ( invg ` M ) ` ( K .x. X ) ) )
30 17 18 21 29 syl3anc 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( K .x. ( ( invg ` M ) ` X ) ) = ( ( invg ` M ) ` ( K .x. X ) ) )
31 30 oveq1d 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( ( K .x. ( ( invg ` M ) ` X ) ) ( +g ` M ) ( K .x. Y ) ) = ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) )
32 28 31 eqtrd 
 |-  ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) )
33 32 anasss 
 |-  ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) )
34 33 3adantr3 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) )
35 6 adantr 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> G e. ( LSubSp ` M ) )
36 simpr3 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G )
37 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
38 11 4 3 37 lssvscl 
 |-  ( ( ( M e. LMod /\ G e. ( LSubSp ` M ) ) /\ ( K e. S /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) e. G )
39 8 35 9 36 38 syl22anc 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) e. G )
40 34 39 eqeltrrd 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G )
41 13 16 40 3jca 
 |-  ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( ( K .x. X ) e. B /\ ( K .x. Y ) e. B /\ ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G ) )
42 41 ex 
 |-  ( ph -> ( ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) -> ( ( K .x. X ) e. B /\ ( K .x. Y ) e. B /\ ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G ) ) )
43 5 19 syl 
 |-  ( ph -> M e. Grp )
44 37 lsssubg 
 |-  ( ( M e. LMod /\ G e. ( LSubSp ` M ) ) -> G e. ( SubGrp ` M ) )
45 5 6 44 syl2anc 
 |-  ( ph -> G e. ( SubGrp ` M ) )
46 1 subgss 
 |-  ( G e. ( SubGrp ` M ) -> G C_ B )
47 45 46 syl 
 |-  ( ph -> G C_ B )
48 1 22 26 2 eqgval 
 |-  ( ( M e. Grp /\ G C_ B ) -> ( X .~ Y <-> ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) )
49 43 47 48 syl2anc 
 |-  ( ph -> ( X .~ Y <-> ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) )
50 1 22 26 2 eqgval 
 |-  ( ( M e. Grp /\ G C_ B ) -> ( ( K .x. X ) .~ ( K .x. Y ) <-> ( ( K .x. X ) e. B /\ ( K .x. Y ) e. B /\ ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G ) ) )
51 43 47 50 syl2anc 
 |-  ( ph -> ( ( K .x. X ) .~ ( K .x. Y ) <-> ( ( K .x. X ) e. B /\ ( K .x. Y ) e. B /\ ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G ) ) )
52 42 49 51 3imtr4d 
 |-  ( ph -> ( X .~ Y -> ( K .x. X ) .~ ( K .x. Y ) ) )