Theorem sylow2alem1

Description: Lemma for sylow2a . An equivalence class of fixed points is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015)

	Ref	Expression
Hypotheses	sylow2a.x	$$⊢X={\mathrm{Base}}_G$$
	sylow2a.m	$$⊢\phi \to \underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)$$
	sylow2a.p	$$⊢\phi \to P\mathrm{pGrp}G$$
	sylow2a.f	$$⊢\phi \to X\in \mathrm{Fin}$$
	sylow2a.y	$$⊢\phi \to Y\in \mathrm{Fin}$$
	sylow2a.z	$$⊢Z=\left\{u\in Y|\forall h\in Xh\underset{\dot{}}{\oplus }u=u\right\}$$
	sylow2a.r	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq Y\wedge \exists g\in Xg\underset{\dot{}}{\oplus }x=y\right)\right\}$$
Assertion	sylow2alem1	$$⊢\left(\phi \wedge A\in Z\right)\to \left[A\right]\underset{\dot{}}{\sim }=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		sylow2a.x	$$⊢X={\mathrm{Base}}_G$$
2		sylow2a.m	$$⊢\phi \to \underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)$$
3		sylow2a.p	$$⊢\phi \to P\mathrm{pGrp}G$$
4		sylow2a.f	$$⊢\phi \to X\in \mathrm{Fin}$$
5		sylow2a.y	$$⊢\phi \to Y\in \mathrm{Fin}$$
6		sylow2a.z	$$⊢Z=\left\{u\in Y|\forall h\in Xh\underset{\dot{}}{\oplus }u=u\right\}$$
7		sylow2a.r	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq Y\wedge \exists g\in Xg\underset{\dot{}}{\oplus }x=y\right)\right\}$$
8		vex	$$⊢w\in \mathrm{V}$$
9		simpr	$$⊢\left(\phi \wedge A\in Z\right)\to A\in Z$$
10		elecg	$$⊢\left(w\in \mathrm{V}\wedge A\in Z\right)\to \left(w\in \left[A\right]\underset{\dot{}}{\sim }\leftrightarrow A\underset{\dot{}}{\sim }w\right)$$
11	8 9 10	sylancr	$$⊢\left(\phi \wedge A\in Z\right)\to \left(w\in \left[A\right]\underset{\dot{}}{\sim }\leftrightarrow A\underset{\dot{}}{\sim }w\right)$$
12	7	gaorb	$$⊢A\underset{\dot{}}{\sim }w\leftrightarrow \left(A\in Y\wedge w\in Y\wedge \exists k\in Xk\underset{\dot{}}{\oplus }A=w\right)$$
13	12	simp3bi	$$⊢A\underset{\dot{}}{\sim }w\to \exists k\in Xk\underset{\dot{}}{\oplus }A=w$$
14		oveq2	$$⊢u=A\to h\underset{\dot{}}{\oplus }u=h\underset{\dot{}}{\oplus }A$$
15		id	$$⊢u=A\to u=A$$
16	14 15	eqeq12d	$$⊢u=A\to \left(h\underset{\dot{}}{\oplus }u=u\leftrightarrow h\underset{\dot{}}{\oplus }A=A\right)$$
17	16	ralbidv	$$⊢u=A\to \left(\forall h\in Xh\underset{\dot{}}{\oplus }u=u\leftrightarrow \forall h\in Xh\underset{\dot{}}{\oplus }A=A\right)$$
18	17 6	elrab2	$$⊢A\in Z\leftrightarrow \left(A\in Y\wedge \forall h\in Xh\underset{\dot{}}{\oplus }A=A\right)$$
19	9 18	sylib	$$⊢\left(\phi \wedge A\in Z\right)\to \left(A\in Y\wedge \forall h\in Xh\underset{\dot{}}{\oplus }A=A\right)$$
20	19	simprd	$$⊢\left(\phi \wedge A\in Z\right)\to \forall h\in Xh\underset{\dot{}}{\oplus }A=A$$
21		oveq1	$$⊢h=k\to h\underset{\dot{}}{\oplus }A=k\underset{\dot{}}{\oplus }A$$
22	21	eqeq1d	$$⊢h=k\to \left(h\underset{\dot{}}{\oplus }A=A\leftrightarrow k\underset{\dot{}}{\oplus }A=A\right)$$
23	22	rspccva	$$⊢\left(\forall h\in Xh\underset{\dot{}}{\oplus }A=A\wedge k\in X\right)\to k\underset{\dot{}}{\oplus }A=A$$
24	20 23	sylan	$$⊢\left(\left(\phi \wedge A\in Z\right)\wedge k\in X\right)\to k\underset{\dot{}}{\oplus }A=A$$
25		eqeq1	$$⊢k\underset{\dot{}}{\oplus }A=w\to \left(k\underset{\dot{}}{\oplus }A=A\leftrightarrow w=A\right)$$
26	24 25	syl5ibcom	$$⊢\left(\left(\phi \wedge A\in Z\right)\wedge k\in X\right)\to \left(k\underset{\dot{}}{\oplus }A=w\to w=A\right)$$
27	26	rexlimdva	$$⊢\left(\phi \wedge A\in Z\right)\to \left(\exists k\in Xk\underset{\dot{}}{\oplus }A=w\to w=A\right)$$
28	13 27	syl5	$$⊢\left(\phi \wedge A\in Z\right)\to \left(A\underset{\dot{}}{\sim }w\to w=A\right)$$
29	11 28	sylbid	$$⊢\left(\phi \wedge A\in Z\right)\to \left(w\in \left[A\right]\underset{\dot{}}{\sim }\to w=A\right)$$
30		velsn	$$⊢w\in \left\{A\right\}\leftrightarrow w=A$$
31	29 30	syl6ibr	$$⊢\left(\phi \wedge A\in Z\right)\to \left(w\in \left[A\right]\underset{\dot{}}{\sim }\to w\in \left\{A\right\}\right)$$
32	31	ssrdv	$$⊢\left(\phi \wedge A\in Z\right)\to \left[A\right]\underset{\dot{}}{\sim }\subseteq \left\{A\right\}$$
33	7 1	gaorber	$$⊢\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}Y\right)\to \underset{\dot{}}{\sim }\mathrm{Er}Y$$
34	2 33	syl	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}Y$$
35	34	adantr	$$⊢\left(\phi \wedge A\in Z\right)\to \underset{\dot{}}{\sim }\mathrm{Er}Y$$
36	19	simpld	$$⊢\left(\phi \wedge A\in Z\right)\to A\in Y$$
37	35 36	erref	$$⊢\left(\phi \wedge A\in Z\right)\to A\underset{\dot{}}{\sim }A$$
38		elecg	$$⊢\left(A\in Z\wedge A\in Z\right)\to \left(A\in \left[A\right]\underset{\dot{}}{\sim }\leftrightarrow A\underset{\dot{}}{\sim }A\right)$$
39	9 38	sylancom	$$⊢\left(\phi \wedge A\in Z\right)\to \left(A\in \left[A\right]\underset{\dot{}}{\sim }\leftrightarrow A\underset{\dot{}}{\sim }A\right)$$
40	37 39	mpbird	$$⊢\left(\phi \wedge A\in Z\right)\to A\in \left[A\right]\underset{\dot{}}{\sim }$$
41	40	snssd	$$⊢\left(\phi \wedge A\in Z\right)\to \left\{A\right\}\subseteq \left[A\right]\underset{\dot{}}{\sim }$$
42	32 41	eqssd	$$⊢\left(\phi \wedge A\in Z\right)\to \left[A\right]\underset{\dot{}}{\sim }=\left\{A\right\}$$