This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpoidinvlem4

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

Ref Expression
Hypothesis grpfo.1 ⊢ 𝑋 = ran 𝐺
Assertion grpoidinvlem4 ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) → ( 𝐴 𝐺 𝑈 ) = ( 𝑈 𝐺 𝐴 ) )

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ 𝑋 = ran 𝐺
2 simpll ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝐺 ∈ GrpOp )
3 simplr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
4 simpr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
5 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝑦 ) 𝐺 𝐴 ) = ( 𝐴 𝐺 ( 𝑦 𝐺 𝐴 ) ) )
6 2 3 4 3 5 syl13anc ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝑦 ) 𝐺 𝐴 ) = ( 𝐴 𝐺 ( 𝑦 𝐺 𝐴 ) ) )
7 oveq2 ⊢ ( ( 𝑦 𝐺 𝐴 ) = 𝑈 → ( 𝐴 𝐺 ( 𝑦 𝐺 𝐴 ) ) = ( 𝐴 𝐺 𝑈 ) )
8 6 7 sylan9eq ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) → ( ( 𝐴 𝐺 𝑦 ) 𝐺 𝐴 ) = ( 𝐴 𝐺 𝑈 ) )
9 oveq1 ⊢ ( ( 𝐴 𝐺 𝑦 ) = 𝑈 → ( ( 𝐴 𝐺 𝑦 ) 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) )
10 8 9 sylan9req ⊢ ( ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) → ( 𝐴 𝐺 𝑈 ) = ( 𝑈 𝐺 𝐴 ) )
11 10 anasss ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) → ( 𝐴 𝐺 𝑈 ) = ( 𝑈 𝐺 𝐴 ) )
12 11 r19.29an ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) → ( 𝐴 𝐺 𝑈 ) = ( 𝑈 𝐺 𝐴 ) )