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 ‘ 𝑈 ) )