qusval

Description: Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	qusval.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
	qusval.v	$⊢ φ \to V = {Base}_{R}$
	qusval.f	$⊢ F = (x \in V ⟼ [x] \underset{˙}{\sim})$
	qusval.e	$⊢ φ \to \underset{˙}{\sim} \in W$
	qusval.r	$⊢ φ \to R \in Z$
Assertion	qusval	$⊢ φ \to U = F “_{𝑠} R$

Proof

Step	Hyp	Ref	Expression
1		qusval.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
2		qusval.v	$⊢ φ \to V = {Base}_{R}$
3		qusval.f	$⊢ F = (x \in V ⟼ [x] \underset{˙}{\sim})$
4		qusval.e	$⊢ φ \to \underset{˙}{\sim} \in W$
5		qusval.r	$⊢ φ \to R \in Z$
6		df-qus	$⊢ /_{𝑠} = (r \in V, e \in V ⟼ (x \in {Base}_{r} ⟼ [x] e) “_{𝑠} r)$
7	6	a1i	$⊢ φ \to /_{𝑠} = (r \in V, e \in V ⟼ (x \in {Base}_{r} ⟼ [x] e) “_{𝑠} r)$
8		simprl	$⊢ (φ \land (r = R \land e = \underset{˙}{\sim})) \to r = R$
9	8	fveq2d	$⊢ (φ \land (r = R \land e = \underset{˙}{\sim})) \to {Base}_{r} = {Base}_{R}$
10	2	adantr	$⊢ (φ \land (r = R \land e = \underset{˙}{\sim})) \to V = {Base}_{R}$
11	9 10	eqtr4d	$⊢ (φ \land (r = R \land e = \underset{˙}{\sim})) \to {Base}_{r} = V$
12		eceq2	$⊢ e = \underset{˙}{\sim} \to [x] e = [x] \underset{˙}{\sim}$
13	12	ad2antll	$⊢ (φ \land (r = R \land e = \underset{˙}{\sim})) \to [x] e = [x] \underset{˙}{\sim}$
14	11 13	mpteq12dv	$⊢ (φ \land (r = R \land e = \underset{˙}{\sim})) \to (x \in {Base}_{r} ⟼ [x] e) = (x \in V ⟼ [x] \underset{˙}{\sim})$
15	14 3	eqtr4di	$⊢ (φ \land (r = R \land e = \underset{˙}{\sim})) \to (x \in {Base}_{r} ⟼ [x] e) = F$
16	15 8	oveq12d	$⊢ (φ \land (r = R \land e = \underset{˙}{\sim})) \to (x \in {Base}_{r} ⟼ [x] e) “_{𝑠} r = F “_{𝑠} R$
17	5	elexd	$⊢ φ \to R \in V$
18	4	elexd	$⊢ φ \to \underset{˙}{\sim} \in V$
19		ovexd	$⊢ φ \to F “_{𝑠} R \in V$
20	7 16 17 18 19	ovmpod	$⊢ φ \to R /_{𝑠} \underset{˙}{\sim} = F “_{𝑠} R$
21	1 20	eqtrd	$⊢ φ \to U = F “_{𝑠} R$

Metamath Proof Explorer

Theorem qusval

Proof