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

Metamath Proof Explorer

Theorem grplactfval

Description: The left group action of element A of group G . (Contributed by Paul Chapman, 18-Mar-2008)

Ref Expression
Hypotheses grplact.1 ⊢ F = g ∈ X ⟼ a ∈ X ⟼ g + ˙ a
grplact.2 ⊢ X = Base G
Assertion grplactfval ⊢ A ∈ X → F ⁡ A = a ∈ X ⟼ A + ˙ a

Proof

Step Hyp Ref Expression
1 grplact.1 ⊢ F = g ∈ X ⟼ a ∈ X ⟼ g + ˙ a
2 grplact.2 ⊢ X = Base G
3 oveq1 ⊢ g = A → g + ˙ a = A + ˙ a
4 3 mpteq2dv ⊢ g = A → a ∈ X ⟼ g + ˙ a = a ∈ X ⟼ A + ˙ a
5 4 1 2 mptfvmpt ⊢ A ∈ X → F ⁡ A = a ∈ X ⟼ A + ˙ a