grplactval

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

	Ref	Expression
Hypotheses	grplact.1	$⊢ F = (g \in X ⟼ (a \in X ⟼ g \underset{˙}{+} a))$
	grplact.2	$⊢ X = {Base}_{G}$
Assertion	grplactval	$⊢ (A \in X \land B \in X) \to F (A) (B) = A \underset{˙}{+} B$

Step	Hyp	Ref	Expression
1		grplact.1	$⊢ F = (g \in X ⟼ (a \in X ⟼ g \underset{˙}{+} a))$
2		grplact.2	$⊢ X = {Base}_{G}$
3	1 2	grplactfval	$⊢ A \in X \to F (A) = (a \in X ⟼ A \underset{˙}{+} a)$
4	3	fveq1d	$⊢ A \in X \to F (A) (B) = (a \in X ⟼ A \underset{˙}{+} a) (B)$
5		oveq2	$⊢ a = B \to A \underset{˙}{+} a = A \underset{˙}{+} B$
6		eqid	$⊢ (a \in X ⟼ A \underset{˙}{+} a) = (a \in X ⟼ A \underset{˙}{+} a)$
7		ovex	$⊢ A \underset{˙}{+} B \in V$
8	5 6 7	fvmpt	$⊢ B \in X \to (a \in X ⟼ A \underset{˙}{+} a) (B) = A \underset{˙}{+} B$
9	4 8	sylan9eq	$⊢ (A \in X \land B \in X) \to F (A) (B) = A \underset{˙}{+} B$

Metamath Proof Explorer