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 
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ∘ 𝑌 ) ) 