Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ X = ran ⁡ G
2 simpll ⊢ G ∈ GrpOp ∧ A ∈ X ∧ y ∈ X → G ∈ GrpOp
3 simplr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ y ∈ X → A ∈ X
4 simpr ⊢ G ∈ GrpOp ∧ A ∈ X ∧ y ∈ X → y ∈ X
5 1 grpoass ⊢ G ∈ GrpOp ∧ A ∈ X ∧ y ∈ X ∧ A ∈ X → A G y G A = A G y G A
6 2 3 4 3 5 syl13anc ⊢ G ∈ GrpOp ∧ A ∈ X ∧ y ∈ X → A G y G A = A G y G A
7 oveq2 ⊢ y G A = U → A G y G A = A G U
8 6 7 sylan9eq ⊢ G ∈ GrpOp ∧ A ∈ X ∧ y ∈ X ∧ y G A = U → A G y G A = A G U
9 oveq1 ⊢ A G y = U → A G y G A = U G A
10 8 9 sylan9req ⊢ G ∈ GrpOp ∧ A ∈ X ∧ y ∈ X ∧ y G A = U ∧ A G y = U → A G U = U G A
11 10 anasss ⊢ G ∈ GrpOp ∧ A ∈ X ∧ y ∈ X ∧ y G A = U ∧ A G y = U → A G U = U G A
12 11 r19.29an ⊢ G ∈ GrpOp ∧ A ∈ X ∧ ∃ y ∈ X y G A = U ∧ A G y = U → A G U = U G A