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

Metamath Proof Explorer

Theorem grpoidinvlem4

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

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

Proof

Step Hyp Ref Expression
1 grpfo.1 
 |-  X = ran G
2 simpll 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> G e. GrpOp )
3 simplr 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> A e. X )
4 simpr 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> y e. X )
5 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ y e. X /\ A e. X ) ) -> ( ( A G y ) G A ) = ( A G ( y G A ) ) )
6 2 3 4 3 5 syl13anc 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) -> ( ( A G y ) G A ) = ( A G ( y G A ) ) )
7 oveq2 
 |-  ( ( y G A ) = U -> ( A G ( y G A ) ) = ( A G U ) )
8 6 7 sylan9eq 
 |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) -> ( ( A G y ) G A ) = ( A G U ) )
9 oveq1 
 |-  ( ( A G y ) = U -> ( ( A G y ) G A ) = ( U G A ) )
10 8 9 sylan9req 
 |-  ( ( ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) /\ ( y G A ) = U ) /\ ( A G y ) = U ) -> ( A G U ) = ( U G A ) )
11 10 anasss 
 |-  ( ( ( ( G e. GrpOp /\ A e. X ) /\ y e. X ) /\ ( ( y G A ) = U /\ ( A G y ) = U ) ) -> ( A G U ) = ( U G A ) )
12 11 r19.29an 
 |-  ( ( ( G e. GrpOp /\ A e. X ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) -> ( A G U ) = ( U G A ) )