qusaddvallem

Description: Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	qusaddf.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
	qusaddf.v	$⊢ φ \to V = {Base}_{R}$
	qusaddf.r	$⊢ φ \to \underset{˙}{\sim} Er V$
	qusaddf.z	$⊢ φ \to R \in Z$
	qusaddf.e	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{\cdot} b) \underset{˙}{\sim} (p \underset{˙}{\cdot} q))$
	qusaddf.c	$⊢ (φ \land (p \in V \land q \in V)) \to p \underset{˙}{\cdot} q \in V$
	qusaddflem.f	$⊢ F = (x \in V ⟼ [x] \underset{˙}{\sim})$
	qusaddflem.g	$⊢ φ \to \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
Assertion	qusaddvallem	$⊢ (φ \land X \in V \land Y \in V) \to [X] \underset{˙}{\sim} \underset{˙}{∙} [Y] \underset{˙}{\sim} = [(X \underset{˙}{\cdot} Y)] \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		qusaddf.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
2		qusaddf.v	$⊢ φ \to V = {Base}_{R}$
3		qusaddf.r	$⊢ φ \to \underset{˙}{\sim} Er V$
4		qusaddf.z	$⊢ φ \to R \in Z$
5		qusaddf.e	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{\cdot} b) \underset{˙}{\sim} (p \underset{˙}{\cdot} q))$
6		qusaddf.c	$⊢ (φ \land (p \in V \land q \in V)) \to p \underset{˙}{\cdot} q \in V$
7		qusaddflem.f	$⊢ F = (x \in V ⟼ [x] \underset{˙}{\sim})$
8		qusaddflem.g	$⊢ φ \to \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
9		fvex	$⊢ {Base}_{R} \in V$
10	2 9	eqeltrdi	$⊢ φ \to V \in V$
11		erex	$⊢ \underset{˙}{\sim} Er V \to (V \in V \to \underset{˙}{\sim} \in V)$
12	3 10 11	sylc	$⊢ φ \to \underset{˙}{\sim} \in V$
13	1 2 7 12 4	quslem	$⊢ φ \to F : V \underset{onto}{⟶} V / \underset{˙}{\sim}$
14	3 10 7 6 5	ercpbl	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
15	13 14 8	imasaddvallem	$⊢ (φ \land X \in V \land Y \in V) \to F (X) \underset{˙}{∙} F (Y) = F (X \underset{˙}{\cdot} Y)$
16	3	3ad2ant1	$⊢ (φ \land X \in V \land Y \in V) \to \underset{˙}{\sim} Er V$
17	10	3ad2ant1	$⊢ (φ \land X \in V \land Y \in V) \to V \in V$
18	16 17 7	divsfval	$⊢ (φ \land X \in V \land Y \in V) \to F (X) = [X] \underset{˙}{\sim}$
19	16 17 7	divsfval	$⊢ (φ \land X \in V \land Y \in V) \to F (Y) = [Y] \underset{˙}{\sim}$
20	18 19	oveq12d	$⊢ (φ \land X \in V \land Y \in V) \to F (X) \underset{˙}{∙} F (Y) = [X] \underset{˙}{\sim} \underset{˙}{∙} [Y] \underset{˙}{\sim}$
21	16 17 7	divsfval	$⊢ (φ \land X \in V \land Y \in V) \to F (X \underset{˙}{\cdot} Y) = [(X \underset{˙}{\cdot} Y)] \underset{˙}{\sim}$
22	15 20 21	3eqtr3d	$⊢ (φ \land X \in V \land Y \in V) \to [X] \underset{˙}{\sim} \underset{˙}{∙} [Y] \underset{˙}{\sim} = [(X \underset{˙}{\cdot} Y)] \underset{˙}{\sim}$

Metamath Proof Explorer

Theorem qusaddvallem

Proof