grpoidinvlem2

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

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

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	$⊢ X = ran G$
2		simprr	$⊢ (G \in GrpOp \land (Y \in X \land A \in X)) \to A \in X$
3		simprl	$⊢ (G \in GrpOp \land (Y \in X \land A \in X)) \to Y \in X$
4	1	grpocl	$⊢ (G \in GrpOp \land A \in X \land Y \in X) \to A G Y \in X$
5	4	3com23	$⊢ (G \in GrpOp \land Y \in X \land A \in X) \to A G Y \in X$
6	5	3expb	$⊢ (G \in GrpOp \land (Y \in X \land A \in X)) \to A G Y \in X$
7	2 3 6	3jca	$⊢ (G \in GrpOp \land (Y \in X \land A \in X)) \to (A \in X \land Y \in X \land A G Y \in X)$
8	1	grpoass	$⊢ (G \in GrpOp \land (A \in X \land Y \in X \land A G Y \in X)) \to (A G Y) G (A G Y) = A G (Y G (A G Y))$
9	7 8	syldan	$⊢ (G \in GrpOp \land (Y \in X \land A \in X)) \to (A G Y) G (A G Y) = A G (Y G (A G Y))$
10	9	adantr	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (U G Y = Y \land Y G A = U)) \to (A G Y) G (A G Y) = A G (Y G (A G Y))$
11		oveq1	$⊢ Y G A = U \to (Y G A) G Y = U G Y$
12	11	adantl	$⊢ (U G Y = Y \land Y G A = U) \to (Y G A) G Y = U G Y$
13		simpl	$⊢ (U G Y = Y \land Y G A = U) \to U G Y = Y$
14	12 13	eqtr2d	$⊢ (U G Y = Y \land Y G A = U) \to Y = (Y G A) G Y$
15		id	$⊢ (Y \in X \land A \in X \land Y \in X) \to (Y \in X \land A \in X \land Y \in X)$
16	15	3anidm13	$⊢ (Y \in X \land A \in X) \to (Y \in X \land A \in X \land Y \in X)$
17	1	grpoass	$⊢ (G \in GrpOp \land (Y \in X \land A \in X \land Y \in X)) \to (Y G A) G Y = Y G (A G Y)$
18	16 17	sylan2	$⊢ (G \in GrpOp \land (Y \in X \land A \in X)) \to (Y G A) G Y = Y G (A G Y)$
19	14 18	sylan9eqr	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (U G Y = Y \land Y G A = U)) \to Y = Y G (A G Y)$
20	19	eqcomd	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (U G Y = Y \land Y G A = U)) \to Y G (A G Y) = Y$
21	20	oveq2d	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (U G Y = Y \land Y G A = U)) \to A G (Y G (A G Y)) = A G Y$
22	10 21	eqtrd	$⊢ ((G \in GrpOp \land (Y \in X \land A \in X)) \land (U G Y = Y \land Y G A = U)) \to (A G Y) G (A G Y) = A G Y$

Metamath Proof Explorer

Theorem grpoidinvlem2

Proof