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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow2a.m	⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
	sylow2a.p	⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
	sylow2a.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow2a.y	⊢ ( 𝜑 → 𝑌 ∈ Fin )
	sylow2a.z	⊢ 𝑍 = { 𝑢 ∈ 𝑌 ∣ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 }
	sylow2a.r	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
Assertion	sylow2alem1	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → [ 𝐴 ] ∼ = { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		sylow2a.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow2a.m	⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) )
3		sylow2a.p	⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
4		sylow2a.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
5		sylow2a.y	⊢ ( 𝜑 → 𝑌 ∈ Fin )
6		sylow2a.z	⊢ 𝑍 = { 𝑢 ∈ 𝑌 ∣ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 }
7		sylow2a.r	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑌 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
8		vex	⊢ 𝑤 ∈ V
9		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → 𝐴 ∈ 𝑍 )
10		elecg	⊢ ( ( 𝑤 ∈ V ∧ 𝐴 ∈ 𝑍 ) → ( 𝑤 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝑤 ) )
11	8 9 10	sylancr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ( 𝑤 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝑤 ) )
12	7	gaorb	⊢ ( 𝐴 ∼ 𝑤 ↔ ( 𝐴 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ∧ ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝐴 ) = 𝑤 ) )
13	12	simp3bi	⊢ ( 𝐴 ∼ 𝑤 → ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝐴 ) = 𝑤 )
14		oveq2	⊢ ( 𝑢 = 𝐴 → ( ℎ ⊕ 𝑢 ) = ( ℎ ⊕ 𝐴 ) )
15		id	⊢ ( 𝑢 = 𝐴 → 𝑢 = 𝐴 )
16	14 15	eqeq12d	⊢ ( 𝑢 = 𝐴 → ( ( ℎ ⊕ 𝑢 ) = 𝑢 ↔ ( ℎ ⊕ 𝐴 ) = 𝐴 ) )
17	16	ralbidv	⊢ ( 𝑢 = 𝐴 → ( ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝑢 ) = 𝑢 ↔ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐴 ) )
18	17 6	elrab2	⊢ ( 𝐴 ∈ 𝑍 ↔ ( 𝐴 ∈ 𝑌 ∧ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐴 ) )
19	9 18	sylib	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ( 𝐴 ∈ 𝑌 ∧ ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐴 ) )
20	19	simprd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐴 )
21		oveq1	⊢ ( ℎ = 𝑘 → ( ℎ ⊕ 𝐴 ) = ( 𝑘 ⊕ 𝐴 ) )
22	21	eqeq1d	⊢ ( ℎ = 𝑘 → ( ( ℎ ⊕ 𝐴 ) = 𝐴 ↔ ( 𝑘 ⊕ 𝐴 ) = 𝐴 ) )
23	22	rspccva	⊢ ( ( ∀ ℎ ∈ 𝑋 ( ℎ ⊕ 𝐴 ) = 𝐴 ∧ 𝑘 ∈ 𝑋 ) → ( 𝑘 ⊕ 𝐴 ) = 𝐴 )
24	20 23	sylan	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝑘 ⊕ 𝐴 ) = 𝐴 )
25		eqeq1	⊢ ( ( 𝑘 ⊕ 𝐴 ) = 𝑤 → ( ( 𝑘 ⊕ 𝐴 ) = 𝐴 ↔ 𝑤 = 𝐴 ) )
26	24 25	syl5ibcom	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝑘 ⊕ 𝐴 ) = 𝑤 → 𝑤 = 𝐴 ) )
27	26	rexlimdva	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ( ∃ 𝑘 ∈ 𝑋 ( 𝑘 ⊕ 𝐴 ) = 𝑤 → 𝑤 = 𝐴 ) )
28	13 27	syl5	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ( 𝐴 ∼ 𝑤 → 𝑤 = 𝐴 ) )
29	11 28	sylbid	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ( 𝑤 ∈ [ 𝐴 ] ∼ → 𝑤 = 𝐴 ) )
30		velsn	⊢ ( 𝑤 ∈ { 𝐴 } ↔ 𝑤 = 𝐴 )
31	29 30	imbitrrdi	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ( 𝑤 ∈ [ 𝐴 ] ∼ → 𝑤 ∈ { 𝐴 } ) )
32	31	ssrdv	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → [ 𝐴 ] ∼ ⊆ { 𝐴 } )
33	7 1	gaorber	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ∼ Er 𝑌 )
34	2 33	syl	⊢ ( 𝜑 → ∼ Er 𝑌 )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ∼ Er 𝑌 )
36	19	simpld	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → 𝐴 ∈ 𝑌 )
37	35 36	erref	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → 𝐴 ∼ 𝐴 )
38		elecg	⊢ ( ( 𝐴 ∈ 𝑍 ∧ 𝐴 ∈ 𝑍 ) → ( 𝐴 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝐴 ) )
39	9 38	sylancom	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → ( 𝐴 ∈ [ 𝐴 ] ∼ ↔ 𝐴 ∼ 𝐴 ) )
40	37 39	mpbird	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → 𝐴 ∈ [ 𝐴 ] ∼ )
41	40	snssd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → { 𝐴 } ⊆ [ 𝐴 ] ∼ )
42	32 41	eqssd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑍 ) → [ 𝐴 ] ∼ = { 𝐴 } )

Metamath Proof Explorer

Theorem sylow2alem1

Proof