Metamath Proof Explorer


Theorem symg1hash

Description: The symmetric group on a singleton has cardinality 1 . (Contributed by AV, 9-Dec-2018)

Ref Expression
Hypotheses symg1bas.1 𝐺 = ( SymGrp ‘ 𝐴 )
symg1bas.2 𝐵 = ( Base ‘ 𝐺 )
symg1bas.0 𝐴 = { 𝐼 }
Assertion symg1hash ( 𝐼𝑉 → ( ♯ ‘ 𝐵 ) = 1 )

Proof

Step Hyp Ref Expression
1 symg1bas.1 𝐺 = ( SymGrp ‘ 𝐴 )
2 symg1bas.2 𝐵 = ( Base ‘ 𝐺 )
3 symg1bas.0 𝐴 = { 𝐼 }
4 snfi { 𝐼 } ∈ Fin
5 3 4 eqeltri 𝐴 ∈ Fin
6 1 2 symghash ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐵 ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )
7 5 6 ax-mp ( ♯ ‘ 𝐵 ) = ( ! ‘ ( ♯ ‘ 𝐴 ) )
8 3 fveq2i ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝐼 } )
9 hashsng ( 𝐼𝑉 → ( ♯ ‘ { 𝐼 } ) = 1 )
10 8 9 eqtrid ( 𝐼𝑉 → ( ♯ ‘ 𝐴 ) = 1 )
11 10 fveq2d ( 𝐼𝑉 → ( ! ‘ ( ♯ ‘ 𝐴 ) ) = ( ! ‘ 1 ) )
12 fac1 ( ! ‘ 1 ) = 1
13 11 12 eqtrdi ( 𝐼𝑉 → ( ! ‘ ( ♯ ‘ 𝐴 ) ) = 1 )
14 7 13 eqtrid ( 𝐼𝑉 → ( ♯ ‘ 𝐵 ) = 1 )