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 ˙ = 0 G
Assertion gagrpid ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → 0 ˙ ⊕ ˙ A = A

Proof

Step Hyp Ref Expression
1 gagrpid.1 ⊢ 0 ˙ = 0 G
2 eqid ⊢ Base G = Base G
3 eqid ⊢ + G = + G
4 2 3 1 isga ⊢ ⊕ ˙ ∈ G GrpAct Y ↔ G ∈ Grp ∧ Y ∈ V ∧ ⊕ ˙ : Base G × Y ⟶ Y ∧ ∀ x ∈ Y 0 ˙ ⊕ ˙ x = x ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ⊕ ˙ x = y ⊕ ˙ z ⊕ ˙ x
5 4 simprbi ⊢ ⊕ ˙ ∈ G GrpAct Y → ⊕ ˙ : Base G × Y ⟶ Y ∧ ∀ x ∈ Y 0 ˙ ⊕ ˙ x = x ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ⊕ ˙ x = y ⊕ ˙ z ⊕ ˙ x
6 simpl ⊢ 0 ˙ ⊕ ˙ x = x ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ⊕ ˙ x = y ⊕ ˙ z ⊕ ˙ x → 0 ˙ ⊕ ˙ x = x
7 6 ralimi ⊢ ∀ x ∈ Y 0 ˙ ⊕ ˙ x = x ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ⊕ ˙ x = y ⊕ ˙ z ⊕ ˙ x → ∀ x ∈ Y 0 ˙ ⊕ ˙ x = x
8 5 7 simpl2im ⊢ ⊕ ˙ ∈ G GrpAct Y → ∀ x ∈ 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 ⊢ ∀ x ∈ Y 0 ˙ ⊕ ˙ x = x ∧ A ∈ Y → 0 ˙ ⊕ ˙ A = A
13 8 12 sylan ⊢ ⊕ ˙ ∈ G GrpAct Y ∧ A ∈ Y → 0 ˙ ⊕ ˙ A = A