Metamath Proof Explorer

Theorem grpoidinvlem2

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

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

Proof

Step Hyp Ref Expression
1 grpfo.1 ⊢ 𝑋 = ran 𝐺
2 simprr ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
3 simprl ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → 𝑌 ∈ 𝑋 )
4 1 grpocl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑌 ) ∈ 𝑋 )
5 4 3com23 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 𝑌 ) ∈ 𝑋 )
6 5 3expb ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝑌 ) ∈ 𝑋 )
7 2 3 6 3jca ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑌 ) ∈ 𝑋 ) )
8 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ∧ ( 𝐴 𝐺 𝑌 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝑌 ) 𝐺 ( 𝐴 𝐺 𝑌 ) ) = ( 𝐴 𝐺 ( 𝑌 𝐺 ( 𝐴 𝐺 𝑌 ) ) ) )
9 7 8 syldan ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝑌 ) 𝐺 ( 𝐴 𝐺 𝑌 ) ) = ( 𝐴 𝐺 ( 𝑌 𝐺 ( 𝐴 𝐺 𝑌 ) ) ) )
10 9 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑈 𝐺 𝑌 ) = 𝑌 ∧ ( 𝑌 𝐺 𝐴 ) = 𝑈 ) ) → ( ( 𝐴 𝐺 𝑌 ) 𝐺 ( 𝐴 𝐺 𝑌 ) ) = ( 𝐴 𝐺 ( 𝑌 𝐺 ( 𝐴 𝐺 𝑌 ) ) ) )
11 oveq1 ⊢ ( ( 𝑌 𝐺 𝐴 ) = 𝑈 → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝑌 ) = ( 𝑈 𝐺 𝑌 ) )
12 11 adantl ⊢ ( ( ( 𝑈 𝐺 𝑌 ) = 𝑌 ∧ ( 𝑌 𝐺 𝐴 ) = 𝑈 ) → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝑌 ) = ( 𝑈 𝐺 𝑌 ) )
13 simpl ⊢ ( ( ( 𝑈 𝐺 𝑌 ) = 𝑌 ∧ ( 𝑌 𝐺 𝐴 ) = 𝑈 ) → ( 𝑈 𝐺 𝑌 ) = 𝑌 )
14 12 13 eqtr2d ⊢ ( ( ( 𝑈 𝐺 𝑌 ) = 𝑌 ∧ ( 𝑌 𝐺 𝐴 ) = 𝑈 ) → 𝑌 = ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝑌 ) )
15 id ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) → ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) )
16 15 3anidm13 ⊢ ( ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) )
17 1 grpoass ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑌 ∈ 𝑋 ) ) → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝑌 ) = ( 𝑌 𝐺 ( 𝐴 𝐺 𝑌 ) ) )
18 16 17 sylan2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑌 𝐺 𝐴 ) 𝐺 𝑌 ) = ( 𝑌 𝐺 ( 𝐴 𝐺 𝑌 ) ) )
19 14 18 sylan9eqr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑈 𝐺 𝑌 ) = 𝑌 ∧ ( 𝑌 𝐺 𝐴 ) = 𝑈 ) ) → 𝑌 = ( 𝑌 𝐺 ( 𝐴 𝐺 𝑌 ) ) )
20 19 eqcomd ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑈 𝐺 𝑌 ) = 𝑌 ∧ ( 𝑌 𝐺 𝐴 ) = 𝑈 ) ) → ( 𝑌 𝐺 ( 𝐴 𝐺 𝑌 ) ) = 𝑌 )
21 20 oveq2d ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑈 𝐺 𝑌 ) = 𝑌 ∧ ( 𝑌 𝐺 𝐴 ) = 𝑈 ) ) → ( 𝐴 𝐺 ( 𝑌 𝐺 ( 𝐴 𝐺 𝑌 ) ) ) = ( 𝐴 𝐺 𝑌 ) )
22 10 21 eqtrd ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ ( 𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) ∧ ( ( 𝑈 𝐺 𝑌 ) = 𝑌 ∧ ( 𝑌 𝐺 𝐴 ) = 𝑈 ) ) → ( ( 𝐴 𝐺 𝑌 ) 𝐺 ( 𝐴 𝐺 𝑌 ) ) = ( 𝐴 𝐺 𝑌 ) )