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 · ˙ = M
eqgvscpbl.m φ M LMod
eqgvscpbl.g φ G LSubSp M
eqgvscpbl.k φ K S
Assertion eqgvscpbl φ X ˙ Y K · ˙ X ˙ K · ˙ 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 · ˙ = M
5 eqgvscpbl.m φ M LMod
6 eqgvscpbl.g φ G LSubSp M
7 eqgvscpbl.k φ K S
8 5 adantr φ X B Y B inv g M X + M Y G M LMod
9 7 adantr φ X B Y B inv g M X + M Y G K S
10 simpr1 φ X B Y B inv g M X + M Y G X B
11 eqid Scalar M = Scalar M
12 1 11 4 3 lmodvscl M LMod K S X B K · ˙ X B
13 8 9 10 12 syl3anc φ X B Y B inv g M X + M Y G K · ˙ X B
14 simpr2 φ X B Y B inv g M X + M Y G Y B
15 1 11 4 3 lmodvscl M LMod K S Y B K · ˙ Y B
16 8 9 14 15 syl3anc φ X B Y B inv g M X + M Y G K · ˙ Y B
17 5 ad2antrr φ X B Y B M LMod
18 7 ad2antrr φ X B Y B K S
19 lmodgrp M LMod M Grp
20 17 19 syl φ X B Y B M Grp
21 simplr φ X B Y B X B
22 eqid inv g M = inv g M
23 1 22 grpinvcl M Grp X B inv g M X B
24 20 21 23 syl2anc φ X B Y B inv g M X B
25 simpr φ X B Y B Y B
26 eqid + M = + M
27 1 26 11 4 3 lmodvsdi M LMod K S inv g M X B Y B K · ˙ inv g M X + M Y = K · ˙ inv g M X + M K · ˙ Y
28 17 18 24 25 27 syl13anc φ X B Y B K · ˙ inv g M X + M Y = K · ˙ inv g M X + M K · ˙ Y
29 1 11 4 22 3 lmodvsinv2 M LMod K S X B K · ˙ inv g M X = inv g M K · ˙ X
30 17 18 21 29 syl3anc φ X B Y B K · ˙ inv g M X = inv g M K · ˙ X
31 30 oveq1d φ X B Y B K · ˙ inv g M X + M K · ˙ Y = inv g M K · ˙ X + M K · ˙ Y
32 28 31 eqtrd φ X B Y B K · ˙ inv g M X + M Y = inv g M K · ˙ X + M K · ˙ Y
33 32 anasss φ X B Y B K · ˙ inv g M X + M Y = inv g M K · ˙ X + M K · ˙ Y
34 33 3adantr3 φ X B Y B inv g M X + M Y G K · ˙ inv g M X + M Y = inv g M K · ˙ X + M K · ˙ Y
35 6 adantr φ X B Y B inv g M X + M Y G G LSubSp M
36 simpr3 φ X B Y B inv g M X + M Y G inv g M X + M Y G
37 eqid LSubSp M = LSubSp M
38 11 4 3 37 lssvscl M LMod G LSubSp M K S inv g M X + M Y G K · ˙ inv g M X + M Y G
39 8 35 9 36 38 syl22anc φ X B Y B inv g M X + M Y G K · ˙ inv g M X + M Y G
40 34 39 eqeltrrd φ X B Y B inv g M X + M Y G inv g M K · ˙ X + M K · ˙ Y G
41 13 16 40 3jca φ X B Y B inv g M X + M Y G K · ˙ X B K · ˙ Y B inv g M K · ˙ X + M K · ˙ Y G
42 41 ex φ X B Y B inv g M X + M Y G K · ˙ X B K · ˙ Y B inv g M K · ˙ X + M K · ˙ Y G
43 5 19 syl φ M Grp
44 37 lsssubg M LMod G LSubSp M G SubGrp M
45 5 6 44 syl2anc φ G SubGrp M
46 1 subgss G SubGrp M G B
47 45 46 syl φ G B
48 1 22 26 2 eqgval M Grp G B X ˙ Y X B Y B inv g M X + M Y G
49 43 47 48 syl2anc φ X ˙ Y X B Y B inv g M X + M Y G
50 1 22 26 2 eqgval M Grp G B K · ˙ X ˙ K · ˙ Y K · ˙ X B K · ˙ Y B inv g M K · ˙ X + M K · ˙ Y G
51 43 47 50 syl2anc φ K · ˙ X ˙ K · ˙ Y K · ˙ X B K · ˙ Y B inv g M K · ˙ X + M K · ˙ Y G
52 42 49 51 3imtr4d φ X ˙ Y K · ˙ X ˙ K · ˙ Y