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 ⊢ 𝐵 = ( 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 ⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 → ( 𝐾 · 𝑋 ) ∼ ( 𝐾 · 𝑌 ) ) )