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

Metamath Proof Explorer

Theorem gagrpid

Description: The identity of the group does not alter the base set. (Contributed by Jeff Hankins, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypothesis gagrpid.1 
|- .0. = ( 0g ` G )
Assertion gagrpid 
|- ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( .0. .(+) A ) = A )

Proof

Step Hyp Ref Expression
1 gagrpid.1 
 |-  .0. = ( 0g ` G )
2 eqid 
 |-  ( Base ` G ) = ( Base ` G )
3 eqid 
 |-  ( +g ` G ) = ( +g ` G )
4 2 3 1 isga 
 |-  ( .(+) e. ( G GrpAct Y ) <-> ( ( G e. Grp /\ Y e. _V ) /\ ( .(+) : ( ( Base ` G ) X. Y ) --> Y /\ A. x e. Y ( ( .0. .(+) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) ) ) )
5 4 simprbi 
 |-  ( .(+) e. ( G GrpAct Y ) -> ( .(+) : ( ( Base ` G ) X. Y ) --> Y /\ A. x e. Y ( ( .0. .(+) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) ) )
6 simpl 
 |-  ( ( ( .0. .(+) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) -> ( .0. .(+) x ) = x )
7 6 ralimi 
 |-  ( A. x e. Y ( ( .0. .(+) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) -> A. x e. Y ( .0. .(+) x ) = x )
8 5 7 simpl2im 
 |-  ( .(+) e. ( G GrpAct Y ) -> A. x e. Y ( .0. .(+) x ) = x )
9 oveq2 
 |-  ( x = A -> ( .0. .(+) x ) = ( .0. .(+) A ) )
10 id 
 |-  ( x = A -> x = A )
11 9 10 eqeq12d 
 |-  ( x = A -> ( ( .0. .(+) x ) = x <-> ( .0. .(+) A ) = A ) )
12 11 rspccva 
 |-  ( ( A. x e. Y ( .0. .(+) x ) = x /\ A e. Y ) -> ( .0. .(+) A ) = A )
13 8 12 sylan 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ A e. Y ) -> ( .0. .(+) A ) = A )