grpoidinvlem1

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

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

Step	Hyp	Ref	Expression
1		grpfo.1	$⊢ X = ran G$
2		id	$⊢ (Y \in X \land A \in X \land A \in X) \to (Y \in X \land A \in X \land A \in X)$
3	2	3anidm23	$⊢ (Y \in X \land A \in X) \to (Y \in X \land A \in X \land A \in X)$
4	1	grpoass	$⊢ (G \in GrpOp \land (Y \in X \land A \in X \land A \in X)) \to (Y G A) G A = Y G (A G A)$
5	3 4	sylan2	$⊢ (G \in GrpOp \land (Y \in X \land A \in X)) \to (Y G A) G A = Y G (A G A)$
6	5	adantr	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (Y G A = U \land A G A = A)) \to (Y G A) G A = Y G (A G A)$
7		oveq1	$⊢ Y G A = U \to (Y G A) G A = U G A$
8	7	ad2antrl	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (Y G A = U \land A G A = A)) \to (Y G A) G A = U G A$
9		oveq2	$⊢ A G A = A \to Y G (A G A) = Y G A$
10	9	ad2antll	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (Y G A = U \land A G A = A)) \to Y G (A G A) = Y G A$
11		simprl	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (Y G A = U \land A G A = A)) \to Y G A = U$
12	10 11	eqtrd	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (Y G A = U \land A G A = A)) \to Y G (A G A) = U$
13	6 8 12	3eqtr3d	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (Y G A = U \land A G A = A)) \to U G A = U$

Metamath Proof Explorer