Metamath Proof Explorer

Theorem grpoidinvlem2

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

Ref Expression
Hypothesis grpfo.1 
|- X = ran G
Assertion grpoidinvlem2 
|- ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( U G Y ) = Y /\ ( Y G A ) = U ) ) -> ( ( A G Y ) G ( A G Y ) ) = ( A G Y ) )

Proof

Step Hyp Ref Expression
1 grpfo.1 
 |-  X = ran G
2 simprr 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) -> A e. X )
3 simprl 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) -> Y e. X )
4 1 grpocl 
 |-  ( ( G e. GrpOp /\ A e. X /\ Y e. X ) -> ( A G Y ) e. X )
5 4 3com23 
 |-  ( ( G e. GrpOp /\ Y e. X /\ A e. X ) -> ( A G Y ) e. X )
6 5 3expb 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) -> ( A G Y ) e. X )
7 2 3 6 3jca 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) -> ( A e. X /\ Y e. X /\ ( A G Y ) e. X ) )
8 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ Y e. X /\ ( A G Y ) e. X ) ) -> ( ( A G Y ) G ( A G Y ) ) = ( A G ( Y G ( A G Y ) ) ) )
9 7 8 syldan 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) -> ( ( A G Y ) G ( A G Y ) ) = ( A G ( Y G ( A G Y ) ) ) )
10 9 adantr 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( U G Y ) = Y /\ ( Y G A ) = U ) ) -> ( ( A G Y ) G ( A G Y ) ) = ( A G ( Y G ( A G Y ) ) ) )
11 oveq1 
 |-  ( ( Y G A ) = U -> ( ( Y G A ) G Y ) = ( U G Y ) )
12 11 adantl 
 |-  ( ( ( U G Y ) = Y /\ ( Y G A ) = U ) -> ( ( Y G A ) G Y ) = ( U G Y ) )
13 simpl 
 |-  ( ( ( U G Y ) = Y /\ ( Y G A ) = U ) -> ( U G Y ) = Y )
14 12 13 eqtr2d 
 |-  ( ( ( U G Y ) = Y /\ ( Y G A ) = U ) -> Y = ( ( Y G A ) G Y ) )
15 id 
 |-  ( ( Y e. X /\ A e. X /\ Y e. X ) -> ( Y e. X /\ A e. X /\ Y e. X ) )
16 15 3anidm13 
 |-  ( ( Y e. X /\ A e. X ) -> ( Y e. X /\ A e. X /\ Y e. X ) )
17 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X /\ Y e. X ) ) -> ( ( Y G A ) G Y ) = ( Y G ( A G Y ) ) )
18 16 17 sylan2 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) -> ( ( Y G A ) G Y ) = ( Y G ( A G Y ) ) )
19 14 18 sylan9eqr 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( U G Y ) = Y /\ ( Y G A ) = U ) ) -> Y = ( Y G ( A G Y ) ) )
20 19 eqcomd 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( U G Y ) = Y /\ ( Y G A ) = U ) ) -> ( Y G ( A G Y ) ) = Y )
21 20 oveq2d 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( U G Y ) = Y /\ ( Y G A ) = U ) ) -> ( A G ( Y G ( A G Y ) ) ) = ( A G Y ) )
22 10 21 eqtrd 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( U G Y ) = Y /\ ( Y G A ) = U ) ) -> ( ( A G Y ) G ( A G Y ) ) = ( A G Y ) )