qusgrp2

Description: Prove that a quotient structure is a group. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	qusgrp2.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
	qusgrp2.v	$⊢ φ \to V = {Base}_{R}$
	qusgrp2.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
	qusgrp2.r	$⊢ φ \to \underset{˙}{\sim} Er V$
	qusgrp2.x	$⊢ φ \to R \in X$
	qusgrp2.e	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q))$
	qusgrp2.1	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
	qusgrp2.2	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to ((x \underset{˙}{+} y) \underset{˙}{+} z) \underset{˙}{\sim} (x \underset{˙}{+} (y \underset{˙}{+} z))$
	qusgrp2.3	$⊢ φ \to \underset{˙}{0} \in V$
	qusgrp2.4	$⊢ (φ \land x \in V) \to (\underset{˙}{0} \underset{˙}{+} x) \underset{˙}{\sim} x$
	qusgrp2.5	$⊢ (φ \land x \in V) \to N \in V$
	qusgrp2.6	$⊢ (φ \land x \in V) \to (N \underset{˙}{+} x) \underset{˙}{\sim} \underset{˙}{0}$
Assertion	qusgrp2	$⊢ φ \to (U \in Grp \land [\underset{˙}{0}] \underset{˙}{\sim} = 0_{U})$

Proof

Step	Hyp	Ref	Expression
1		qusgrp2.u	$⊢ φ \to U = R /_{𝑠} \underset{˙}{\sim}$
2		qusgrp2.v	$⊢ φ \to V = {Base}_{R}$
3		qusgrp2.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
4		qusgrp2.r	$⊢ φ \to \underset{˙}{\sim} Er V$
5		qusgrp2.x	$⊢ φ \to R \in X$
6		qusgrp2.e	$⊢ φ \to ((a \underset{˙}{\sim} p \land b \underset{˙}{\sim} q) \to (a \underset{˙}{+} b) \underset{˙}{\sim} (p \underset{˙}{+} q))$
7		qusgrp2.1	$⊢ (φ \land x \in V \land y \in V) \to x \underset{˙}{+} y \in V$
8		qusgrp2.2	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to ((x \underset{˙}{+} y) \underset{˙}{+} z) \underset{˙}{\sim} (x \underset{˙}{+} (y \underset{˙}{+} z))$
9		qusgrp2.3	$⊢ φ \to \underset{˙}{0} \in V$
10		qusgrp2.4	$⊢ (φ \land x \in V) \to (\underset{˙}{0} \underset{˙}{+} x) \underset{˙}{\sim} x$
11		qusgrp2.5	$⊢ (φ \land x \in V) \to N \in V$
12		qusgrp2.6	$⊢ (φ \land x \in V) \to (N \underset{˙}{+} x) \underset{˙}{\sim} \underset{˙}{0}$
13		eqid	$⊢ (u \in V ⟼ [u] \underset{˙}{\sim}) = (u \in V ⟼ [u] \underset{˙}{\sim})$
14		fvex	$⊢ {Base}_{R} \in V$
15	2 14	eqeltrdi	$⊢ φ \to V \in V$
16		erex	$⊢ \underset{˙}{\sim} Er V \to (V \in V \to \underset{˙}{\sim} \in V)$
17	4 15 16	sylc	$⊢ φ \to \underset{˙}{\sim} \in V$
18	1 2 13 17 5	qusval	$⊢ φ \to U = (u \in V ⟼ [u] \underset{˙}{\sim}) “_{𝑠} R$
19	1 2 13 17 5	quslem	$⊢ φ \to (u \in V ⟼ [u] \underset{˙}{\sim}) : V \underset{onto}{⟶} V / \underset{˙}{\sim}$
20	7	3expb	$⊢ (φ \land (x \in V \land y \in V)) \to x \underset{˙}{+} y \in V$
21	4 15 13 20 6	ercpbl	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (((u \in V ⟼ [u] \underset{˙}{\sim}) (a) = (u \in V ⟼ [u] \underset{˙}{\sim}) (p) \land (u \in V ⟼ [u] \underset{˙}{\sim}) (b) = (u \in V ⟼ [u] \underset{˙}{\sim}) (q)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (a \underset{˙}{+} b) = (u \in V ⟼ [u] \underset{˙}{\sim}) (p \underset{˙}{+} q))$
22	4	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to \underset{˙}{\sim} Er V$
23	22 8	erthi	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to [((x \underset{˙}{+} y) \underset{˙}{+} z)] \underset{˙}{\sim} = [(x \underset{˙}{+} (y \underset{˙}{+} z))] \underset{˙}{\sim}$
24	15	adantr	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to V \in V$
25	22 24 13	divsfval	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) ((x \underset{˙}{+} y) \underset{˙}{+} z) = [((x \underset{˙}{+} y) \underset{˙}{+} z)] \underset{˙}{\sim}$
26	22 24 13	divsfval	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (x \underset{˙}{+} (y \underset{˙}{+} z)) = [(x \underset{˙}{+} (y \underset{˙}{+} z))] \underset{˙}{\sim}$
27	23 25 26	3eqtr4d	$⊢ (φ \land (x \in V \land y \in V \land z \in V)) \to (u \in V ⟼ [u] \underset{˙}{\sim}) ((x \underset{˙}{+} y) \underset{˙}{+} z) = (u \in V ⟼ [u] \underset{˙}{\sim}) (x \underset{˙}{+} (y \underset{˙}{+} z))$
28	4	adantr	$⊢ (φ \land x \in V) \to \underset{˙}{\sim} Er V$
29	28 10	erthi	$⊢ (φ \land x \in V) \to [(\underset{˙}{0} \underset{˙}{+} x)] \underset{˙}{\sim} = [x] \underset{˙}{\sim}$
30	15	adantr	$⊢ (φ \land x \in V) \to V \in V$
31	28 30 13	divsfval	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0} \underset{˙}{+} x) = [(\underset{˙}{0} \underset{˙}{+} x)] \underset{˙}{\sim}$
32	28 30 13	divsfval	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (x) = [x] \underset{˙}{\sim}$
33	29 31 32	3eqtr4d	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0} \underset{˙}{+} x) = (u \in V ⟼ [u] \underset{˙}{\sim}) (x)$
34	28 12	ersym	$⊢ (φ \land x \in V) \to \underset{˙}{0} \underset{˙}{\sim} (N \underset{˙}{+} x)$
35	28 34	erthi	$⊢ (φ \land x \in V) \to [\underset{˙}{0}] \underset{˙}{\sim} = [(N \underset{˙}{+} x)] \underset{˙}{\sim}$
36	28 30 13	divsfval	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = [\underset{˙}{0}] \underset{˙}{\sim}$
37	28 30 13	divsfval	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (N \underset{˙}{+} x) = [(N \underset{˙}{+} x)] \underset{˙}{\sim}$
38	35 36 37	3eqtr4rd	$⊢ (φ \land x \in V) \to (u \in V ⟼ [u] \underset{˙}{\sim}) (N \underset{˙}{+} x) = (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0})$
39	18 2 3 19 21 5 7 27 9 33 11 38	imasgrp2	$⊢ φ \to (U \in Grp \land (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = 0_{U})$
40	4 15 13	divsfval	$⊢ φ \to (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = [\underset{˙}{0}] \underset{˙}{\sim}$
41	40	eqcomd	$⊢ φ \to [\underset{˙}{0}] \underset{˙}{\sim} = (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0})$
42	41	eqeq1d	$⊢ φ \to ([\underset{˙}{0}] \underset{˙}{\sim} = 0_{U} \leftrightarrow (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = 0_{U})$
43	42	anbi2d	$⊢ φ \to ((U \in Grp \land [\underset{˙}{0}] \underset{˙}{\sim} = 0_{U}) \leftrightarrow (U \in Grp \land (u \in V ⟼ [u] \underset{˙}{\sim}) (\underset{˙}{0}) = 0_{U}))$
44	39 43	mpbird	$⊢ φ \to (U \in Grp \land [\underset{˙}{0}] \underset{˙}{\sim} = 0_{U})$

Metamath Proof Explorer

Theorem qusgrp2

Proof