# Metamath Proof Explorer

## Theorem symgov

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

Ref Expression
Hypotheses symgov.1 𝐺 = ( SymGrp ‘ 𝐴 )
symgov.2 𝐵 = ( Base ‘ 𝐺 )
symgov.3 + = ( +g𝐺 )
Assertion symgov ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋𝑌 ) )

### Proof

Step Hyp Ref Expression
1 symgov.1 𝐺 = ( SymGrp ‘ 𝐴 )
2 symgov.2 𝐵 = ( Base ‘ 𝐺 )
3 symgov.3 + = ( +g𝐺 )
4 eqid ( 𝐴m 𝐴 ) = ( 𝐴m 𝐴 )
5 1 4 3 symgplusg + = ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) )
6 5 a1i ( ( 𝑋𝐵𝑌𝐵 ) → + = ( 𝑓 ∈ ( 𝐴m 𝐴 ) , 𝑔 ∈ ( 𝐴m 𝐴 ) ↦ ( 𝑓𝑔 ) ) )
7 simpl ( ( 𝑓 = 𝑋𝑔 = 𝑌 ) → 𝑓 = 𝑋 )
8 simpr ( ( 𝑓 = 𝑋𝑔 = 𝑌 ) → 𝑔 = 𝑌 )
9 7 8 coeq12d ( ( 𝑓 = 𝑋𝑔 = 𝑌 ) → ( 𝑓𝑔 ) = ( 𝑋𝑌 ) )
10 9 adantl ( ( ( 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑓 = 𝑋𝑔 = 𝑌 ) ) → ( 𝑓𝑔 ) = ( 𝑋𝑌 ) )
11 1 2 symgbasmap ( 𝑋𝐵𝑋 ∈ ( 𝐴m 𝐴 ) )
12 11 adantr ( ( 𝑋𝐵𝑌𝐵 ) → 𝑋 ∈ ( 𝐴m 𝐴 ) )
13 1 2 symgbasmap ( 𝑌𝐵𝑌 ∈ ( 𝐴m 𝐴 ) )
14 13 adantl ( ( 𝑋𝐵𝑌𝐵 ) → 𝑌 ∈ ( 𝐴m 𝐴 ) )
15 coexg ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝑋𝑌 ) ∈ V )
16 6 10 12 14 15 ovmpod ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋𝑌 ) )