Theorem gafo

Description: A group action is onto its base set. (Contributed by Jeff Hankins, 10-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypothesis	gaf.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
Assertion	gafo	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) –onto→ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		gaf.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2	1	gaf	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 )
3		gagrp	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝐺 ∈ Grp )
4	3	adantr	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → 𝐺 ∈ Grp )
5		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6	1 5	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
7	4 6	syl	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
8		simpr	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑌 )
9	5	gagrpid	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝑥 ) = 𝑥 )
10	9	eqcomd	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 = ( ( 0g ‘ 𝐺 ) ⊕ 𝑥 ) )
11		rspceov	⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑋 ∧ 𝑥 ∈ 𝑌 ∧ 𝑥 = ( ( 0g ‘ 𝐺 ) ⊕ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑌 𝑥 = ( 𝑦 ⊕ 𝑧 ) )
12	7 8 10 11	syl3anc	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑌 𝑥 = ( 𝑦 ⊕ 𝑧 ) )
13	12	ralrimiva	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ∀ 𝑥 ∈ 𝑌 ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑌 𝑥 = ( 𝑦 ⊕ 𝑧 ) )
14		foov	⊢ ( ⊕ : ( 𝑋 × 𝑌 ) –onto→ 𝑌 ↔ ( ⊕ : ( 𝑋 × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑌 ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑌 𝑥 = ( 𝑦 ⊕ 𝑧 ) ) )
15	2 13 14	sylanbrc	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( 𝑋 × 𝑌 ) –onto→ 𝑌 )