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