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 𝐵 = ( Base ‘ 𝑀 )
eqgvscpbl.e = ( 𝑀 ~QG 𝐺 )
eqgvscpbl.s 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
eqgvscpbl.p · = ( ·𝑠𝑀 )
eqgvscpbl.m ( 𝜑𝑀 ∈ LMod )
eqgvscpbl.g ( 𝜑𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
eqgvscpbl.k ( 𝜑𝐾𝑆 )
Assertion eqgvscpbl ( 𝜑 → ( 𝑋 𝑌 → ( 𝐾 · 𝑋 ) ( 𝐾 · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 eqgvscpbl.v 𝐵 = ( Base ‘ 𝑀 )
2 eqgvscpbl.e = ( 𝑀 ~QG 𝐺 )
3 eqgvscpbl.s 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
4 eqgvscpbl.p · = ( ·𝑠𝑀 )
5 eqgvscpbl.m ( 𝜑𝑀 ∈ LMod )
6 eqgvscpbl.g ( 𝜑𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
7 eqgvscpbl.k ( 𝜑𝐾𝑆 )
8 5 adantr ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝑀 ∈ LMod )
9 7 adantr ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝐾𝑆 )
10 simpr1 ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝑋𝐵 )
11 eqid ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
12 1 11 4 3 lmodvscl ( ( 𝑀 ∈ LMod ∧ 𝐾𝑆𝑋𝐵 ) → ( 𝐾 · 𝑋 ) ∈ 𝐵 )
13 8 9 10 12 syl3anc ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · 𝑋 ) ∈ 𝐵 )
14 simpr2 ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝑌𝐵 )
15 1 11 4 3 lmodvscl ( ( 𝑀 ∈ LMod ∧ 𝐾𝑆𝑌𝐵 ) → ( 𝐾 · 𝑌 ) ∈ 𝐵 )
16 8 9 14 15 syl3anc ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · 𝑌 ) ∈ 𝐵 )
17 5 ad2antrr ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → 𝑀 ∈ LMod )
18 7 ad2antrr ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → 𝐾𝑆 )
19 lmodgrp ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
20 17 19 syl ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → 𝑀 ∈ Grp )
21 simplr ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → 𝑋𝐵 )
22 eqid ( invg𝑀 ) = ( invg𝑀 )
23 1 22 grpinvcl ( ( 𝑀 ∈ Grp ∧ 𝑋𝐵 ) → ( ( invg𝑀 ) ‘ 𝑋 ) ∈ 𝐵 )
24 20 21 23 syl2anc ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → ( ( invg𝑀 ) ‘ 𝑋 ) ∈ 𝐵 )
25 simpr ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → 𝑌𝐵 )
26 eqid ( +g𝑀 ) = ( +g𝑀 )
27 1 26 11 4 3 lmodvsdi ( ( 𝑀 ∈ LMod ∧ ( 𝐾𝑆 ∧ ( ( invg𝑀 ) ‘ 𝑋 ) ∈ 𝐵𝑌𝐵 ) ) → ( 𝐾 · ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ) = ( ( 𝐾 · ( ( invg𝑀 ) ‘ 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) )
28 17 18 24 25 27 syl13anc ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → ( 𝐾 · ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ) = ( ( 𝐾 · ( ( invg𝑀 ) ‘ 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) )
29 1 11 4 22 3 lmodvsinv2 ( ( 𝑀 ∈ LMod ∧ 𝐾𝑆𝑋𝐵 ) → ( 𝐾 · ( ( invg𝑀 ) ‘ 𝑋 ) ) = ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) )
30 17 18 21 29 syl3anc ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → ( 𝐾 · ( ( invg𝑀 ) ‘ 𝑋 ) ) = ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) )
31 30 oveq1d ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → ( ( 𝐾 · ( ( invg𝑀 ) ‘ 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) = ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) )
32 28 31 eqtrd ( ( ( 𝜑𝑋𝐵 ) ∧ 𝑌𝐵 ) → ( 𝐾 · ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ) = ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) )
33 32 anasss ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝐾 · ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ) = ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) )
34 33 3adantr3 ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ) = ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) )
35 6 adantr ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
36 simpr3 ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 )
37 eqid ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
38 11 4 3 37 lssvscl ( ( ( 𝑀 ∈ LMod ∧ 𝐺 ∈ ( LSubSp ‘ 𝑀 ) ) ∧ ( 𝐾𝑆 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ) ∈ 𝐺 )
39 8 35 9 36 38 syl22anc ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ) ∈ 𝐺 )
40 34 39 eqeltrrd ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 )
41 13 16 40 3jca ( ( 𝜑 ∧ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( ( 𝐾 · 𝑋 ) ∈ 𝐵 ∧ ( 𝐾 · 𝑌 ) ∈ 𝐵 ∧ ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 ) )
42 41 ex ( 𝜑 → ( ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) → ( ( 𝐾 · 𝑋 ) ∈ 𝐵 ∧ ( 𝐾 · 𝑌 ) ∈ 𝐵 ∧ ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 ) ) )
43 5 19 syl ( 𝜑𝑀 ∈ Grp )
44 37 lsssubg ( ( 𝑀 ∈ LMod ∧ 𝐺 ∈ ( LSubSp ‘ 𝑀 ) ) → 𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
45 5 6 44 syl2anc ( 𝜑𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
46 1 subgss ( 𝐺 ∈ ( SubGrp ‘ 𝑀 ) → 𝐺𝐵 )
47 45 46 syl ( 𝜑𝐺𝐵 )
48 1 22 26 2 eqgval ( ( 𝑀 ∈ Grp ∧ 𝐺𝐵 ) → ( 𝑋 𝑌 ↔ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) )
49 43 47 48 syl2anc ( 𝜑 → ( 𝑋 𝑌 ↔ ( 𝑋𝐵𝑌𝐵 ∧ ( ( ( invg𝑀 ) ‘ 𝑋 ) ( +g𝑀 ) 𝑌 ) ∈ 𝐺 ) ) )
50 1 22 26 2 eqgval ( ( 𝑀 ∈ Grp ∧ 𝐺𝐵 ) → ( ( 𝐾 · 𝑋 ) ( 𝐾 · 𝑌 ) ↔ ( ( 𝐾 · 𝑋 ) ∈ 𝐵 ∧ ( 𝐾 · 𝑌 ) ∈ 𝐵 ∧ ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 ) ) )
51 43 47 50 syl2anc ( 𝜑 → ( ( 𝐾 · 𝑋 ) ( 𝐾 · 𝑌 ) ↔ ( ( 𝐾 · 𝑋 ) ∈ 𝐵 ∧ ( 𝐾 · 𝑌 ) ∈ 𝐵 ∧ ( ( ( invg𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 ) ) )
52 42 49 51 3imtr4d ( 𝜑 → ( 𝑋 𝑌 → ( 𝐾 · 𝑋 ) ( 𝐾 · 𝑌 ) ) )