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

Metamath Proof Explorer

Theorem symggrp

Description: The symmetric group on a set A is a group. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 13-Jan-2015) (Proof shortened by AV, 28-Jan-2024)

Ref Expression
Hypothesis symggrp.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion symggrp ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 symggrp.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 eqidd ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
3 eqidd ⊢ ( 𝐴 ∈ 𝑉 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) )
4 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6 1 4 5 symgcl ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
7 6 3adant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
8 1 4 5 symgcl ⊢ ( ( 𝑓 ∈ ( Base ‘ 𝐺 ) ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) ∈ ( Base ‘ 𝐺 ) )
9 1 4 5 symgov ⊢ ( ( 𝑓 ∈ ( Base ‘ 𝐺 ) ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) = ( 𝑓 ∘ 𝑔 ) )
10 8 9 symggrplem ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
12 1 idresperm ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) )
13 1 4 5 symgov ⊢ ( ( ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( ( I ↾ 𝐴 ) ∘ 𝑥 ) )
14 12 13 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( ( I ↾ 𝐴 ) ∘ 𝑥 ) )
15 1 4 elsymgbas ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↔ 𝑥 : 𝐴 –1-1-onto→ 𝐴 ) )
16 15 biimpa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 : 𝐴 –1-1-onto→ 𝐴 )
17 f1of ⊢ ( 𝑥 : 𝐴 –1-1-onto→ 𝐴 → 𝑥 : 𝐴 ⟶ 𝐴 )
18 fcoi2 ⊢ ( 𝑥 : 𝐴 ⟶ 𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝑥 ) = 𝑥 )
19 16 17 18 3syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( I ↾ 𝐴 ) ∘ 𝑥 ) = 𝑥 )
20 14 19 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( I ↾ 𝐴 ) ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
21 f1ocnv ⊢ ( 𝑥 : 𝐴 –1-1-onto→ 𝐴 → ◡ 𝑥 : 𝐴 –1-1-onto→ 𝐴 )
22 21 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 : 𝐴 –1-1-onto→ 𝐴 → ◡ 𝑥 : 𝐴 –1-1-onto→ 𝐴 ) )
23 1 4 elsymgbas ⊢ ( 𝐴 ∈ 𝑉 → ( ◡ 𝑥 ∈ ( Base ‘ 𝐺 ) ↔ ◡ 𝑥 : 𝐴 –1-1-onto→ 𝐴 ) )
24 22 15 23 3imtr4d ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ ( Base ‘ 𝐺 ) → ◡ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
25 24 imp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ◡ 𝑥 ∈ ( Base ‘ 𝐺 ) )
26 1 4 5 symgov ⊢ ( ( ◡ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ◡ 𝑥 ( +g ‘ 𝐺 ) 𝑥 ) = ( ◡ 𝑥 ∘ 𝑥 ) )
27 25 26 sylancom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ◡ 𝑥 ( +g ‘ 𝐺 ) 𝑥 ) = ( ◡ 𝑥 ∘ 𝑥 ) )
28 f1ococnv1 ⊢ ( 𝑥 : 𝐴 –1-1-onto→ 𝐴 → ( ◡ 𝑥 ∘ 𝑥 ) = ( I ↾ 𝐴 ) )
29 16 28 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ◡ 𝑥 ∘ 𝑥 ) = ( I ↾ 𝐴 ) )
30 27 29 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ◡ 𝑥 ( +g ‘ 𝐺 ) 𝑥 ) = ( I ↾ 𝐴 ) )
31 2 3 7 11 12 20 25 30 isgrpd ⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Grp )