Metamath Proof Explorer


Theorem gaset

Description: The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion gaset ˙ G GrpAct Y Y V

Proof

Step Hyp Ref Expression
1 eqid Base G = Base G
2 eqid + G = + G
3 eqid 0 G = 0 G
4 1 2 3 isga ˙ G GrpAct Y G Grp Y V ˙ : Base G × Y Y x Y 0 G ˙ x = x y Base G z Base G y + G z ˙ x = y ˙ z ˙ x
5 4 simplbi ˙ G GrpAct Y G Grp Y V
6 5 simprd ˙ G GrpAct Y Y V