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=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
	grplact.2	$$⊢X={\mathrm{Base}}_G$$
Assertion	grplactfval	$$⊢A\in X\to F\left(A\right)=\left(a\in X⟼A\underset{\dot{}}{+}a\right)$$

Proof

Step	Hyp	Ref	Expression
1		grplact.1	$$⊢F=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
2		grplact.2	$$⊢X={\mathrm{Base}}_G$$
3		oveq1	$$⊢g=A\to g\underset{\dot{}}{+}a=A\underset{\dot{}}{+}a$$
4	3	mpteq2dv	$$⊢g=A\to \left(a\in X⟼g\underset{\dot{}}{+}a\right)=\left(a\in X⟼A\underset{\dot{}}{+}a\right)$$
5	4 1 2	mptfvmpt	$$⊢A\in X\to F\left(A\right)=\left(a\in X⟼A\underset{\dot{}}{+}a\right)$$