Theorem gaass

Description: An "associative" property for group actions. (Contributed by Jeff Hankins, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	gaass.1	$$⊢X={\mathrm{Base}}_G$$
	gaass.2	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	gaass	$$⊢\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge \left(A\in X\wedge B\in X\wedge C\in Y\right)\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{\oplus }C=A\underset{\dot{}}{\oplus }\left(B\underset{\dot{}}{\oplus }C\right)$$

Proof

Step	Hyp	Ref	Expression
1		gaass.1	$$⊢X={\mathrm{Base}}_G$$
2		gaass.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		eqid	$$⊢0_G=0_G$$
4	1 2 3	isga	$$⊢\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\leftrightarrow \left(\left(G\in \mathrm{Grp}\wedge Y\in \mathrm{V}\right)\wedge \left(\underset{\dot{}}{\oplus }:X\times Y⟶Y\wedge \forall x\in Y\left(0_G\underset{\dot{}}{\oplus }x=x\wedge \forall y\in X\forall z\in X\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)\right)\right)\right)$$
5	4	simprbi	$$⊢\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\to \left(\underset{\dot{}}{\oplus }:X\times Y⟶Y\wedge \forall x\in Y\left(0_G\underset{\dot{}}{\oplus }x=x\wedge \forall y\in X\forall z\in X\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)\right)\right)$$
6		simpr	$$⊢\left(0_G\underset{\dot{}}{\oplus }x=x\wedge \forall y\in X\forall z\in X\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)\right)\to \forall y\in X\forall z\in X\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)$$
7	6	ralimi	$$⊢\forall x\in Y\left(0_G\underset{\dot{}}{\oplus }x=x\wedge \forall y\in X\forall z\in X\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)\right)\to \forall x\in Y\forall y\in X\forall z\in X\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)$$
8	5 7	simpl2im	$$⊢\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\to \forall x\in Y\forall y\in X\forall z\in X\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)$$
9		oveq2	$$⊢x=C\to \left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }C$$
10		oveq2	$$⊢x=C\to z\underset{\dot{}}{\oplus }x=z\underset{\dot{}}{\oplus }C$$
11	10	oveq2d	$$⊢x=C\to y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }C\right)$$
12	9 11	eqeq12d	$$⊢x=C\to \left(\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)\leftrightarrow \left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }C=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }C\right)\right)$$
13		oveq1	$$⊢y=A\to y\underset{\dot{}}{+}z=A\underset{\dot{}}{+}z$$
14	13	oveq1d	$$⊢y=A\to \left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }C=\left(A\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }C$$
15		oveq1	$$⊢y=A\to y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }C\right)=A\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }C\right)$$
16	14 15	eqeq12d	$$⊢y=A\to \left(\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }C=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }C\right)\leftrightarrow \left(A\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }C=A\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }C\right)\right)$$
17		oveq2	$$⊢z=B\to A\underset{\dot{}}{+}z=A\underset{\dot{}}{+}B$$
18	17	oveq1d	$$⊢z=B\to \left(A\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }C=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{\oplus }C$$
19		oveq1	$$⊢z=B\to z\underset{\dot{}}{\oplus }C=B\underset{\dot{}}{\oplus }C$$
20	19	oveq2d	$$⊢z=B\to A\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }C\right)=A\underset{\dot{}}{\oplus }\left(B\underset{\dot{}}{\oplus }C\right)$$
21	18 20	eqeq12d	$$⊢z=B\to \left(\left(A\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }C=A\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }C\right)\leftrightarrow \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{\oplus }C=A\underset{\dot{}}{\oplus }\left(B\underset{\dot{}}{\oplus }C\right)\right)$$
22	12 16 21	rspc3v	$$⊢\left(C\in Y\wedge A\in X\wedge B\in X\right)\to \left(\forall x\in Y\forall y\in X\forall z\in X\left(y\underset{\dot{}}{+}z\right)\underset{\dot{}}{\oplus }x=y\underset{\dot{}}{\oplus }\left(z\underset{\dot{}}{\oplus }x\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{\oplus }C=A\underset{\dot{}}{\oplus }\left(B\underset{\dot{}}{\oplus }C\right)\right)$$
23	8 22	syl5	$$⊢\left(C\in Y\wedge A\in X\wedge B\in X\right)\to \left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{\oplus }C=A\underset{\dot{}}{\oplus }\left(B\underset{\dot{}}{\oplus }C\right)\right)$$
24	23	3coml	$$⊢\left(A\in X\wedge B\in X\wedge C\in Y\right)\to \left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{\oplus }C=A\underset{\dot{}}{\oplus }\left(B\underset{\dot{}}{\oplus }C\right)\right)$$
25	24	impcom	$$⊢\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\wedge \left(A\in X\wedge B\in X\wedge C\in Y\right)\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{\oplus }C=A\underset{\dot{}}{\oplus }\left(B\underset{\dot{}}{\oplus }C\right)$$