# 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}={\mathrm{Base}}_{{M}}$
eqgvscpbl.e
eqgvscpbl.s ${⊢}{S}={\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
eqgvscpbl.p
eqgvscpbl.m ${⊢}{\phi }\to {M}\in \mathrm{LMod}$
eqgvscpbl.g ${⊢}{\phi }\to {G}\in \mathrm{LSubSp}\left({M}\right)$
eqgvscpbl.k ${⊢}{\phi }\to {K}\in {S}$
qusscaval.n ${⊢}{N}={M}{/}_{𝑠}\left({M}{~}_{\mathit{QG}}{G}\right)$
qusscaval.m
Assertion qusscaval

### Proof

Step Hyp Ref Expression
1 eqgvscpbl.v ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 eqgvscpbl.e
3 eqgvscpbl.s ${⊢}{S}={\mathrm{Base}}_{\mathrm{Scalar}\left({M}\right)}$
4 eqgvscpbl.p
5 eqgvscpbl.m ${⊢}{\phi }\to {M}\in \mathrm{LMod}$
6 eqgvscpbl.g ${⊢}{\phi }\to {G}\in \mathrm{LSubSp}\left({M}\right)$
7 eqgvscpbl.k ${⊢}{\phi }\to {K}\in {S}$
8 qusscaval.n ${⊢}{N}={M}{/}_{𝑠}\left({M}{~}_{\mathit{QG}}{G}\right)$
9 qusscaval.m
10 8 a1i ${⊢}{\phi }\to {N}={M}{/}_{𝑠}\left({M}{~}_{\mathit{QG}}{G}\right)$
11 1 a1i ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{M}}$
12 eqid ${⊢}\left({x}\in {B}⟼\left[{x}\right]\left({M}{~}_{\mathit{QG}}{G}\right)\right)=\left({x}\in {B}⟼\left[{x}\right]\left({M}{~}_{\mathit{QG}}{G}\right)\right)$
13 ovex ${⊢}{M}{~}_{\mathit{QG}}{G}\in \mathrm{V}$
14 13 a1i ${⊢}{\phi }\to {M}{~}_{\mathit{QG}}{G}\in \mathrm{V}$
15 10 11 12 14 5 qusval ${⊢}{\phi }\to {N}=\left({x}\in {B}⟼\left[{x}\right]\left({M}{~}_{\mathit{QG}}{G}\right)\right){“}_{𝑠}{M}$
16 10 11 12 14 5 quslem ${⊢}{\phi }\to \left({x}\in {B}⟼\left[{x}\right]\left({M}{~}_{\mathit{QG}}{G}\right)\right):{B}\underset{onto}{⟶}{B}/\left({M}{~}_{\mathit{QG}}{G}\right)$
17 eqid ${⊢}\mathrm{Scalar}\left({M}\right)=\mathrm{Scalar}\left({M}\right)$
18 5 adantr ${⊢}\left({\phi }\wedge \left({k}\in {S}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\to {M}\in \mathrm{LMod}$
19 6 adantr ${⊢}\left({\phi }\wedge \left({k}\in {S}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\to {G}\in \mathrm{LSubSp}\left({M}\right)$
20 simpr1 ${⊢}\left({\phi }\wedge \left({k}\in {S}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\to {k}\in {S}$
21 simpr2 ${⊢}\left({\phi }\wedge \left({k}\in {S}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\to {u}\in {B}$
22 simpr3 ${⊢}\left({\phi }\wedge \left({k}\in {S}\wedge {u}\in {B}\wedge {v}\in {B}\right)\right)\to {v}\in {B}$
23 1 2 3 4 18 19 20 8 9 12 21 22 qusvscpbl
24 15 11 16 5 17 3 4 9 23 imasvscaval
25 eceq1 ${⊢}{x}={X}\to \left[{x}\right]\left({M}{~}_{\mathit{QG}}{G}\right)=\left[{X}\right]\left({M}{~}_{\mathit{QG}}{G}\right)$
26 ecexg ${⊢}{M}{~}_{\mathit{QG}}{G}\in \mathrm{V}\to \left[{X}\right]\left({M}{~}_{\mathit{QG}}{G}\right)\in \mathrm{V}$
27 13 26 ax-mp ${⊢}\left[{X}\right]\left({M}{~}_{\mathit{QG}}{G}\right)\in \mathrm{V}$
28 25 12 27 fvmpt ${⊢}{X}\in {B}\to \left({x}\in {B}⟼\left[{x}\right]\left({M}{~}_{\mathit{QG}}{G}\right)\right)\left({X}\right)=\left[{X}\right]\left({M}{~}_{\mathit{QG}}{G}\right)$
29 28 3ad2ant3 ${⊢}\left({\phi }\wedge {K}\in {S}\wedge {X}\in {B}\right)\to \left({x}\in {B}⟼\left[{x}\right]\left({M}{~}_{\mathit{QG}}{G}\right)\right)\left({X}\right)=\left[{X}\right]\left({M}{~}_{\mathit{QG}}{G}\right)$
30 29 oveq2d
31 1 17 4 3 lmodvscl
32 5 31 syl3an1
33 eceq1
34 ecexg
35 13 34 ax-mp
36 33 12 35 fvmpt
37 32 36 syl
38 24 30 37 3eqtr3d