Metamath Proof Explorer

Theorem grpoidinvlem1

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

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

Proof

Step Hyp Ref Expression
1 grpfo.1 
 |-  X = ran G
2 id 
 |-  ( ( Y e. X /\ A e. X /\ A e. X ) -> ( Y e. X /\ A e. X /\ A e. X ) )
3 2 3anidm23 
 |-  ( ( Y e. X /\ A e. X ) -> ( Y e. X /\ A e. X /\ A e. X ) )
4 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X /\ A e. X ) ) -> ( ( Y G A ) G A ) = ( Y G ( A G A ) ) )
5 3 4 sylan2 
 |-  ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) -> ( ( Y G A ) G A ) = ( Y G ( A G A ) ) )
6 5 adantr 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( Y G A ) = U /\ ( A G A ) = A ) ) -> ( ( Y G A ) G A ) = ( Y G ( A G A ) ) )
7 oveq1 
 |-  ( ( Y G A ) = U -> ( ( Y G A ) G A ) = ( U G A ) )
8 7 ad2antrl 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( Y G A ) = U /\ ( A G A ) = A ) ) -> ( ( Y G A ) G A ) = ( U G A ) )
9 oveq2 
 |-  ( ( A G A ) = A -> ( Y G ( A G A ) ) = ( Y G A ) )
10 9 ad2antll 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( Y G A ) = U /\ ( A G A ) = A ) ) -> ( Y G ( A G A ) ) = ( Y G A ) )
11 simprl 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( Y G A ) = U /\ ( A G A ) = A ) ) -> ( Y G A ) = U )
12 10 11 eqtrd 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( Y G A ) = U /\ ( A G A ) = A ) ) -> ( Y G ( A G A ) ) = U )
13 6 8 12 3eqtr3d 
 |-  ( ( ( G e. GrpOp /\ ( Y e. X /\ A e. X ) ) /\ ( ( Y G A ) = U /\ ( A G A ) = A ) ) -> ( U G A ) = U )