Metamath Proof Explorer

Theorem 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 ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X ∧ Y G A = U ∧ A G A = A → U G A = U

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ X = ran ⁡ G
2 id ⊢ Y ∈ X ∧ A ∈ X ∧ A ∈ X → Y ∈ X ∧ A ∈ X ∧ A ∈ X
3 2 3anidm23 ⊢ Y ∈ X ∧ A ∈ X → Y ∈ X ∧ A ∈ X ∧ A ∈ X
4 1 grpoass ⊢ G ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X ∧ A ∈ X → Y G A G A = Y G A G A
5 3 4 sylan2 ⊢ G ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X → Y G A G A = Y G A G A
6 5 adantr ⊢ G ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X ∧ Y G A = U ∧ A G A = A → Y G A G A = Y G A G A
7 oveq1 ⊢ Y G A = U → Y G A G A = U G A
8 7 ad2antrl ⊢ G ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X ∧ Y G A = U ∧ A G A = A → Y G A G A = U G A
9 oveq2 ⊢ A G A = A → Y G A G A = Y G A
10 9 ad2antll ⊢ G ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X ∧ Y G A = U ∧ A G A = A → Y G A G A = Y G A
11 simprl ⊢ G ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X ∧ Y G A = U ∧ A G A = A → Y G A = U
12 10 11 eqtrd ⊢ G ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X ∧ Y G A = U ∧ A G A = A → Y G A G A = U
13 6 8 12 3eqtr3d ⊢ G ∈ GrpOp ∧ Y ∈ X ∧ A ∈ X ∧ Y G A = U ∧ A G A = A → U G A = U