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

Metamath Proof Explorer

Theorem frmdadd

Description: Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses frmdbas.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
frmdbas.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
frmdplusg.p ⊢ + = ( +g ‘ 𝑀 )
Assertion frmdadd ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ++ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 frmdbas.m ⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2 frmdbas.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
3 frmdplusg.p ⊢ + = ( +g ‘ 𝑀 )
4 1 2 3 frmdplusg ⊢ + = ( ++ ↾ ( 𝐵 × 𝐵 ) )
5 4 oveqi ⊢ ( 𝑋 + 𝑌 ) = ( 𝑋 ( ++ ↾ ( 𝐵 × 𝐵 ) ) 𝑌 )
6 ovres ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ++ ↾ ( 𝐵 × 𝐵 ) ) 𝑌 ) = ( 𝑋 ++ 𝑌 ) )
7 5 6 eqtrid ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ++ 𝑌 ) )