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

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	1 2	grplactfval	$$⊢A\in X\to F\left(A\right)=\left(a\in X⟼A\underset{\dot{}}{+}a\right)$$
4	3	fveq1d	$$⊢A\in X\to F\left(A\right)\left(B\right)=\left(a\in X⟼A\underset{\dot{}}{+}a\right)\left(B\right)$$
5		oveq2	$$⊢a=B\to A\underset{\dot{}}{+}a=A\underset{\dot{}}{+}B$$
6		eqid	$$⊢\left(a\in X⟼A\underset{\dot{}}{+}a\right)=\left(a\in X⟼A\underset{\dot{}}{+}a\right)$$
7		ovex	$$⊢A\underset{\dot{}}{+}B\in \mathrm{V}$$
8	5 6 7	fvmpt	$$⊢B\in X\to \left(a\in X⟼A\underset{\dot{}}{+}a\right)\left(B\right)=A\underset{\dot{}}{+}B$$
9	4 8	sylan9eq	$$⊢\left(A\in X\wedge B\in X\right)\to F\left(A\right)\left(B\right)=A\underset{\dot{}}{+}B$$