grpoidinvlem4

Description: Lemma for grpoidinv . (Contributed by NM, 14-Oct-2006) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	grpfo.1	$⊢ X = ran G$
	Assertion	grpoidinvlem4	$⊢ ((G \in GrpOp \land A \in X) \land \exists y \in X (y G A = U \land A G y = U)) \to A G U = U G A$

Step	Hyp	Ref	Expression
1		grpfo.1	$⊢ X = ran G$
2		simpll	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to G \in GrpOp$
3		simplr	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to A \in X$
4		simpr	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to y \in X$
5	1	grpoass	$⊢ (G \in GrpOp \land (A \in X \land y \in X \land A \in X)) \to (A G y) G A = A G (y G A)$
6	2 3 4 3 5	syl13anc	$⊢ ((G \in GrpOp \land A \in X) \land y \in X) \to (A G y) G A = A G (y G A)$
7		oveq2	$⊢ y G A = U \to A G (y G A) = A G U$
8	6 7	sylan9eq	$⊢ (((G \in GrpOp \land A \in X) \land y \in X) \land y G A = U) \to (A G y) G A = A G U$
9		oveq1	$⊢ A G y = U \to (A G y) G A = U G A$
10	8 9	sylan9req	$⊢ ((((G \in GrpOp \land A \in X) \land y \in X) \land y G A = U) \land A G y = U) \to A G U = U G A$
11	10	anasss	$⊢ (((G \in GrpOp \land A \in X) \land y \in X) \land (y G A = U \land A G y = U)) \to A G U = U G A$
12	11	r19.29an	$⊢ ((G \in GrpOp \land A \in X) \land \exists y \in X (y G A = U \land A G y = U)) \to A G U = U G A$

Metamath Proof Explorer