grpoeqdivid

Description: Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011)

	Ref	Expression
Hypotheses	grpeqdivid.1	$⊢ X = ran G$
	grpeqdivid.2	$⊢ U = GId (G)$
	grpeqdivid.3	$⊢ D = /_{g} (G)$
Assertion	grpoeqdivid	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A = B \leftrightarrow A D B = U)$

Step	Hyp	Ref	Expression
1		grpeqdivid.1	$⊢ X = ran G$
2		grpeqdivid.2	$⊢ U = GId (G)$
3		grpeqdivid.3	$⊢ D = /_{g} (G)$
4	1 3 2	grpodivid	$⊢ (G \in GrpOp \land B \in X) \to B D B = U$
5	4	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to B D B = U$
6		oveq1	$⊢ A = B \to A D B = B D B$
7	6	eqeq1d	$⊢ A = B \to (A D B = U \leftrightarrow B D B = U)$
8	5 7	syl5ibrcom	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A = B \to A D B = U)$
9		oveq1	$⊢ A D B = U \to (A D B) G B = U G B$
10	1 3	grponpcan	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A D B) G B = A$
11	1 2	grpolid	$⊢ (G \in GrpOp \land B \in X) \to U G B = B$
12	11	3adant2	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to U G B = B$
13	10 12	eqeq12d	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to ((A D B) G B = U G B \leftrightarrow A = B)$
14	9 13	imbitrid	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A D B = U \to A = B)$
15	8 14	impbid	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to (A = B \leftrightarrow A D B = U)$

Metamath Proof Explorer