Metamath Proof Explorer

Theorem qusscaval

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