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

Metamath Proof Explorer

Theorem grpoidinvlem1

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

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

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ 𝑋 = ran 𝐺
2 id ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
3 2 3anidm23 ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
4 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝐴 ) = ( 𝑌 𝐺 ( 𝐴 𝐺 𝐴 ) ) )
5 3 4 sylan2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝐴 ) = ( 𝑌 𝐺 ( 𝐴 𝐺 𝐴 ) ) )
6 5 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑌 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) ) → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝐴 ) = ( 𝑌 𝐺 ( 𝐴 𝐺 𝐴 ) ) )
7 oveq1 ⊢ ( ( 𝑌 𝐺 𝐴 ) = 𝑈 → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) )
8 7 ad2antrl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑌 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) ) → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝐴 ) = ( 𝑈 𝐺 𝐴 ) )
9 oveq2 ⊢ ( ( 𝐴 𝐺 𝐴 ) = 𝐴 → ( 𝑌 𝐺 ( 𝐴 𝐺 𝐴 ) ) = ( 𝑌 𝐺 𝐴 ) )
10 9 ad2antll ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑌 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) ) → ( 𝑌 𝐺 ( 𝐴 𝐺 𝐴 ) ) = ( 𝑌 𝐺 𝐴 ) )
11 simprl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑌 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) ) → ( 𝑌 𝐺 𝐴 ) = 𝑈 )
12 10 11 eqtrd ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑌 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) ) → ( 𝑌 𝐺 ( 𝐴 𝐺 𝐴 ) ) = 𝑈 )
13 6 8 12 3eqtr3d ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑌 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝐴 ) = 𝐴 ) ) → ( 𝑈 𝐺 𝐴 ) = 𝑈 )