Metamath Proof Explorer

Theorem qusvsval

Description: Value of the scalar multiplication operation on the quotient structure. (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 )
qusvsval.n 
|- N = ( M /s ( M ~QG G ) )
qusvsval.m 
|- .xb = ( .s ` N )
qusvsval.x 
|- ( ph -> X e. B )
Assertion qusvsval 
|- ( ph -> ( K .xb [ X ] ( M ~QG G ) ) = [ ( K .x. X ) ] ( M ~QG G ) )

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 qusvsval.n 
 |-  N = ( M /s ( M ~QG G ) )
9 qusvsval.m 
 |-  .xb = ( .s ` N )
10 qusvsval.x 
 |-  ( ph -> X e. B )
11 8 a1i 
 |-  ( ph -> N = ( M /s ( M ~QG G ) ) )
12 1 a1i 
 |-  ( ph -> B = ( Base ` M ) )
13 eqid 
 |-  ( x e. B |-> [ x ] ( M ~QG G ) ) = ( x e. B |-> [ x ] ( M ~QG G ) )
14 ovex 
 |-  ( M ~QG G ) e. _V
15 14 a1i 
 |-  ( ph -> ( M ~QG G ) e. _V )
16 11 12 13 15 5 qusval 
 |-  ( ph -> N = ( ( x e. B |-> [ x ] ( M ~QG G ) ) "s M ) )
17 11 12 13 15 5 quslem 
 |-  ( ph -> ( x e. B |-> [ x ] ( M ~QG G ) ) : B -onto-> ( B /. ( M ~QG G ) ) )
18 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
19 5 adantr 
 |-  ( ( ph /\ ( k e. S /\ u e. B /\ v e. B ) ) -> M e. LMod )
20 6 adantr 
 |-  ( ( ph /\ ( k e. S /\ u e. B /\ v e. B ) ) -> G e. ( LSubSp ` M ) )
21 simpr1 
 |-  ( ( ph /\ ( k e. S /\ u e. B /\ v e. B ) ) -> k e. S )
22 simpr2 
 |-  ( ( ph /\ ( k e. S /\ u e. B /\ v e. B ) ) -> u e. B )
23 simpr3 
 |-  ( ( ph /\ ( k e. S /\ u e. B /\ v e. B ) ) -> v e. B )
24 1 2 3 4 19 20 21 8 9 13 22 23 qusvscpbl 
 |-  ( ( ph /\ ( k e. S /\ u e. B /\ v e. B ) ) -> ( ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` u ) = ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` v ) -> ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` ( k .x. u ) ) = ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` ( k .x. v ) ) ) )
25 16 12 17 5 18 3 4 9 24 imasvscaval 
 |-  ( ( ph /\ K e. S /\ X e. B ) -> ( K .xb ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` X ) ) = ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` ( K .x. X ) ) )
26 7 10 25 mpd3an23 
 |-  ( ph -> ( K .xb ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` X ) ) = ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` ( K .x. X ) ) )
27 eceq1 
 |-  ( x = X -> [ x ] ( M ~QG G ) = [ X ] ( M ~QG G ) )
28 ecexg 
 |-  ( ( M ~QG G ) e. _V -> [ X ] ( M ~QG G ) e. _V )
29 14 28 ax-mp 
 |-  [ X ] ( M ~QG G ) e. _V
30 27 13 29 fvmpt 
 |-  ( X e. B -> ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` X ) = [ X ] ( M ~QG G ) )
31 10 30 syl 
 |-  ( ph -> ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` X ) = [ X ] ( M ~QG G ) )
32 31 oveq2d 
 |-  ( ph -> ( K .xb ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` X ) ) = ( K .xb [ X ] ( M ~QG G ) ) )
33 1 18 4 3 lmodvscl 
 |-  ( ( M e. LMod /\ K e. S /\ X e. B ) -> ( K .x. X ) e. B )
34 5 7 10 33 syl3anc 
 |-  ( ph -> ( K .x. X ) e. B )
35 eceq1 
 |-  ( x = ( K .x. X ) -> [ x ] ( M ~QG G ) = [ ( K .x. X ) ] ( M ~QG G ) )
36 ecexg 
 |-  ( ( M ~QG G ) e. _V -> [ ( K .x. X ) ] ( M ~QG G ) e. _V )
37 14 36 ax-mp 
 |-  [ ( K .x. X ) ] ( M ~QG G ) e. _V
38 35 13 37 fvmpt 
 |-  ( ( K .x. X ) e. B -> ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` ( K .x. X ) ) = [ ( K .x. X ) ] ( M ~QG G ) )
39 34 38 syl 
 |-  ( ph -> ( ( x e. B |-> [ x ] ( M ~QG G ) ) ` ( K .x. X ) ) = [ ( K .x. X ) ] ( M ~QG G ) )
40 26 32 39 3eqtr3d 
 |-  ( ph -> ( K .xb [ X ] ( M ~QG G ) ) = [ ( K .x. X ) ] ( M ~QG G ) )