Metamath Proof Explorer


Theorem quss

Description: The scalar field of a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses qusbas.u ( 𝜑𝑈 = ( 𝑅 /s ) )
qusbas.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
qusbas.e ( 𝜑𝑊 )
qusbas.r ( 𝜑𝑅𝑍 )
quss.k 𝐾 = ( Scalar ‘ 𝑅 )
Assertion quss ( 𝜑𝐾 = ( Scalar ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 qusbas.u ( 𝜑𝑈 = ( 𝑅 /s ) )
2 qusbas.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
3 qusbas.e ( 𝜑𝑊 )
4 qusbas.r ( 𝜑𝑅𝑍 )
5 quss.k 𝐾 = ( Scalar ‘ 𝑅 )
6 eqid ( 𝑥𝑉 ↦ [ 𝑥 ] ) = ( 𝑥𝑉 ↦ [ 𝑥 ] )
7 1 2 6 3 4 qusval ( 𝜑𝑈 = ( ( 𝑥𝑉 ↦ [ 𝑥 ] ) “s 𝑅 ) )
8 1 2 6 3 4 quslem ( 𝜑 → ( 𝑥𝑉 ↦ [ 𝑥 ] ) : 𝑉onto→ ( 𝑉 / ) )
9 7 2 8 4 5 imassca ( 𝜑𝐾 = ( Scalar ‘ 𝑈 ) )