Theorem quss

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

	Ref	Expression
Hypotheses	qusbas.u	|- ( ph -> U = ( R /s .~ ) )
	qusbas.v	|- ( ph -> V = ( Base ` R ) )
	qusbas.e	|- ( ph -> .~ e. W )
	qusbas.r	|- ( ph -> R e. Z )
	quss.k	|- K = ( Scalar ` R )
Assertion	quss	|- ( ph -> K = ( Scalar ` U ) )

Proof

Step	Hyp	Ref	Expression
1		qusbas.u	|- ( ph -> U = ( R /s .~ ) )
2		qusbas.v	|- ( ph -> V = ( Base ` R ) )
3		qusbas.e	|- ( ph -> .~ e. W )
4		qusbas.r	|- ( ph -> R e. Z )
5		quss.k	|- K = ( Scalar ` R )
6		eqid	|- ( x e. V |-> [ x ] .~ ) = ( x e. V |-> [ x ] .~ )
7	1 2 6 3 4	qusval	|- ( ph -> U = ( ( x e. V |-> [ x ] .~ ) "s R ) )
8	1 2 6 3 4	quslem	|- ( ph -> ( x e. V |-> [ x ] .~ ) : V -onto-> ( V /. .~ ) )
9	7 2 8 4 5	imassca	|- ( ph -> K = ( Scalar ` U ) )