This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝑌 )