Metamath Proof Explorer

Theorem qusvscpbl

Description: The quotient map distributes over the scalar multiplication. (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 )
qusscaval.n 
|- N = ( M /s ( M ~QG G ) )
qusscaval.m 
|- .xb = ( .s ` N )
qusvscpbl.f 
|- F = ( x e. B |-> [ x ] ( M ~QG G ) )
qusvscpbl.u 
|- ( ph -> U e. B )
qusvscpbl.v 
|- ( ph -> V e. B )
Assertion qusvscpbl 
|- ( ph -> ( ( F ` U ) = ( F ` V ) -> ( F ` ( K .x. U ) ) = ( F ` ( K .x. V ) ) ) )

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 qusscaval.n 
 |-  N = ( M /s ( M ~QG G ) )
9 qusscaval.m 
 |-  .xb = ( .s ` N )
10 qusvscpbl.f 
 |-  F = ( x e. B |-> [ x ] ( M ~QG G ) )
11 qusvscpbl.u 
 |-  ( ph -> U e. B )
12 qusvscpbl.v 
 |-  ( ph -> V e. B )
13 eqid 
 |-  ( M ~QG G ) = ( M ~QG G )
14 1 13 3 4 5 6 7 eqgvscpbl 
 |-  ( ph -> ( U ( M ~QG G ) V -> ( K .x. U ) ( M ~QG G ) ( K .x. V ) ) )
15 eqid 
 |-  ( LSubSp ` M ) = ( LSubSp ` M )
16 15 lsssubg 
 |-  ( ( M e. LMod /\ G e. ( LSubSp ` M ) ) -> G e. ( SubGrp ` M ) )
17 5 6 16 syl2anc 
 |-  ( ph -> G e. ( SubGrp ` M ) )
18 1 13 eqger 
 |-  ( G e. ( SubGrp ` M ) -> ( M ~QG G ) Er B )
19 17 18 syl 
 |-  ( ph -> ( M ~QG G ) Er B )
20 19 11 erth 
 |-  ( ph -> ( U ( M ~QG G ) V <-> [ U ] ( M ~QG G ) = [ V ] ( M ~QG G ) ) )
21 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
22 1 21 4 3 lmodvscl 
 |-  ( ( M e. LMod /\ K e. S /\ U e. B ) -> ( K .x. U ) e. B )
23 5 7 11 22 syl3anc 
 |-  ( ph -> ( K .x. U ) e. B )
24 19 23 erth 
 |-  ( ph -> ( ( K .x. U ) ( M ~QG G ) ( K .x. V ) <-> [ ( K .x. U ) ] ( M ~QG G ) = [ ( K .x. V ) ] ( M ~QG G ) ) )
25 14 20 24 3imtr3d 
 |-  ( ph -> ( [ U ] ( M ~QG G ) = [ V ] ( M ~QG G ) -> [ ( K .x. U ) ] ( M ~QG G ) = [ ( K .x. V ) ] ( M ~QG G ) ) )
26 eceq1 
 |-  ( x = U -> [ x ] ( M ~QG G ) = [ U ] ( M ~QG G ) )
27 ovex 
 |-  ( M ~QG G ) e. _V
28 ecexg 
 |-  ( ( M ~QG G ) e. _V -> [ U ] ( M ~QG G ) e. _V )
29 27 28 ax-mp 
 |-  [ U ] ( M ~QG G ) e. _V
30 26 10 29 fvmpt 
 |-  ( U e. B -> ( F ` U ) = [ U ] ( M ~QG G ) )
31 11 30 syl 
 |-  ( ph -> ( F ` U ) = [ U ] ( M ~QG G ) )
32 eceq1 
 |-  ( x = V -> [ x ] ( M ~QG G ) = [ V ] ( M ~QG G ) )
33 ecexg 
 |-  ( ( M ~QG G ) e. _V -> [ V ] ( M ~QG G ) e. _V )
34 27 33 ax-mp 
 |-  [ V ] ( M ~QG G ) e. _V
35 32 10 34 fvmpt 
 |-  ( V e. B -> ( F ` V ) = [ V ] ( M ~QG G ) )
36 12 35 syl 
 |-  ( ph -> ( F ` V ) = [ V ] ( M ~QG G ) )
37 31 36 eqeq12d 
 |-  ( ph -> ( ( F ` U ) = ( F ` V ) <-> [ U ] ( M ~QG G ) = [ V ] ( M ~QG G ) ) )
38 eceq1 
 |-  ( x = ( K .x. U ) -> [ x ] ( M ~QG G ) = [ ( K .x. U ) ] ( M ~QG G ) )
39 ecexg 
 |-  ( ( M ~QG G ) e. _V -> [ ( K .x. U ) ] ( M ~QG G ) e. _V )
40 27 39 ax-mp 
 |-  [ ( K .x. U ) ] ( M ~QG G ) e. _V
41 38 10 40 fvmpt 
 |-  ( ( K .x. U ) e. B -> ( F ` ( K .x. U ) ) = [ ( K .x. U ) ] ( M ~QG G ) )
42 23 41 syl 
 |-  ( ph -> ( F ` ( K .x. U ) ) = [ ( K .x. U ) ] ( M ~QG G ) )
43 1 21 4 3 lmodvscl 
 |-  ( ( M e. LMod /\ K e. S /\ V e. B ) -> ( K .x. V ) e. B )
44 5 7 12 43 syl3anc 
 |-  ( ph -> ( K .x. V ) e. B )
45 eceq1 
 |-  ( x = ( K .x. V ) -> [ x ] ( M ~QG G ) = [ ( K .x. V ) ] ( M ~QG G ) )
46 ecexg 
 |-  ( ( M ~QG G ) e. _V -> [ ( K .x. V ) ] ( M ~QG G ) e. _V )
47 27 46 ax-mp 
 |-  [ ( K .x. V ) ] ( M ~QG G ) e. _V
48 45 10 47 fvmpt 
 |-  ( ( K .x. V ) e. B -> ( F ` ( K .x. V ) ) = [ ( K .x. V ) ] ( M ~QG G ) )
49 44 48 syl 
 |-  ( ph -> ( F ` ( K .x. V ) ) = [ ( K .x. V ) ] ( M ~QG G ) )
50 42 49 eqeq12d 
 |-  ( ph -> ( ( F ` ( K .x. U ) ) = ( F ` ( K .x. V ) ) <-> [ ( K .x. U ) ] ( M ~QG G ) = [ ( K .x. V ) ] ( M ~QG G ) ) )
51 25 37 50 3imtr4d 
 |-  ( ph -> ( ( F ` U ) = ( F ` V ) -> ( F ` ( K .x. U ) ) = ( F ` ( K .x. V ) ) ) )