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 ∧ 𝐴 ∈ 𝑋 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) → ( 𝐴 𝐺 𝑈 ) = ( 𝑈 𝐺 𝐴 ) )