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 𝐵 )