Theorem quss

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

	Ref	Expression
Hypotheses	qusbas.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
	qusbas.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	qusbas.e	$$⊢\phi \to \underset{\dot{}}{\sim }\in W$$
	qusbas.r	$$⊢\phi \to R\in Z$$
	quss.k	$$⊢K=\mathrm{Scalar}\left(R\right)$$
Assertion	quss	$$⊢\phi \to K=\mathrm{Scalar}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		qusbas.u	$$⊢\phi \to U=R{/}_{𝑠}\underset{\dot{}}{\sim }$$
2		qusbas.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
3		qusbas.e	$$⊢\phi \to \underset{\dot{}}{\sim }\in W$$
4		qusbas.r	$$⊢\phi \to R\in Z$$
5		quss.k	$$⊢K=\mathrm{Scalar}\left(R\right)$$
6		eqid	$$⊢\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right)$$
7	1 2 6 3 4	qusval	$$⊢\phi \to U=\left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right){“}_{𝑠}R$$
8	1 2 6 3 4	quslem	$$⊢\phi \to \left(x\in V⟼\left[x\right]\underset{\dot{}}{\sim }\right):V\underset{onto}{⟶}V/\underset{\dot{}}{\sim }$$
9	7 2 8 4 5	imassca	$$⊢\phi \to K=\mathrm{Scalar}\left(U\right)$$