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

Metamath Proof Explorer

Theorem symgval

Description: The value of the symmetric group function at A . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 12-Jan-2015) (Revised by AV, 28-Mar-2024)

Ref Expression
Hypotheses symgval.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
symgval.2 ⊢ 𝐵 = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 }
Assertion symgval 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )

Proof

Step Hyp Ref Expression
1 symgval.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 symgval.2 ⊢ 𝐵 = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 }
3 df-symg ⊢ SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) )
4 3 a1i ⊢ ( 𝐴 ∈ V → SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) ) )
5 fveq2 ⊢ ( 𝑥 = 𝐴 → ( EndoFMnd ‘ 𝑥 ) = ( EndoFMnd ‘ 𝐴 ) )
6 eqidd ⊢ ( 𝑥 = 𝐴 → ℎ = ℎ )
7 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
8 6 7 7 f1oeq123d ⊢ ( 𝑥 = 𝐴 → ( ℎ : 𝑥 –1-1-onto→ 𝑥 ↔ ℎ : 𝐴 –1-1-onto→ 𝐴 ) )
9 8 abbidv ⊢ ( 𝑥 = 𝐴 → { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } = { ℎ ∣ ℎ : 𝐴 –1-1-onto→ 𝐴 } )
10 f1oeq1 ⊢ ( ℎ = 𝑥 → ( ℎ : 𝐴 –1-1-onto→ 𝐴 ↔ 𝑥 : 𝐴 –1-1-onto→ 𝐴 ) )
11 10 cbvabv ⊢ { ℎ ∣ ℎ : 𝐴 –1-1-onto→ 𝐴 } = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 }
12 9 11 eqtrdi ⊢ ( 𝑥 = 𝐴 → { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } )
13 12 2 eqtr4di ⊢ ( 𝑥 = 𝐴 → { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } = 𝐵 )
14 5 13 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ( EndoFMnd ‘ 𝑥 ) ↾s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) )
15 14 adantl ⊢ ( ( 𝐴 ∈ V ∧ 𝑥 = 𝐴 ) → ( ( EndoFMnd ‘ 𝑥 ) ↾s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) )
16 id ⊢ ( 𝐴 ∈ V → 𝐴 ∈ V )
17 ovexd ⊢ ( 𝐴 ∈ V → ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) ∈ V )
18 nfv ⊢ Ⅎ 𝑥 𝐴 ∈ V
19 nfcv ⊢ Ⅎ 𝑥 𝐴
20 nfcv ⊢ Ⅎ 𝑥 ( EndoFMnd ‘ 𝐴 )
21 nfcv ⊢ Ⅎ 𝑥 ↾s
22 nfab1 ⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 }
23 2 22 nfcxfr ⊢ Ⅎ 𝑥 𝐵
24 20 21 23 nfov ⊢ Ⅎ 𝑥 ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )
25 4 15 16 17 18 19 24 fvmptdf ⊢ ( 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) )
26 ress0 ⊢ ( ∅ ↾s 𝐵 ) = ∅
27 26 a1i ⊢ ( ¬ 𝐴 ∈ V → ( ∅ ↾s 𝐵 ) = ∅ )
28 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = ∅ )
29 28 oveq1d ⊢ ( ¬ 𝐴 ∈ V → ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) = ( ∅ ↾s 𝐵 ) )
30 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ∅ )
31 27 29 30 3eqtr4rd ⊢ ( ¬ 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) )
32 25 31 pm2.61i ⊢ ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )
33 1 32 eqtri ⊢ 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 )