Metamath Proof Explorer


Theorem mendplusg

Description: A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015)

Ref Expression
Hypotheses mendplusgfval.a 𝐴 = ( MEndo ‘ 𝑀 )
mendplusgfval.b 𝐵 = ( Base ‘ 𝐴 )
mendplusgfval.p + = ( +g𝑀 )
mendplusg.q = ( +g𝐴 )
Assertion mendplusg ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) = ( 𝑋f + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mendplusgfval.a 𝐴 = ( MEndo ‘ 𝑀 )
2 mendplusgfval.b 𝐵 = ( Base ‘ 𝐴 )
3 mendplusgfval.p + = ( +g𝑀 )
4 mendplusg.q = ( +g𝐴 )
5 oveq12 ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( 𝑥f + 𝑦 ) = ( 𝑋f + 𝑌 ) )
6 1 2 3 mendplusgfval ( +g𝐴 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) )
7 4 6 eqtri = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) )
8 ovex ( 𝑋f + 𝑌 ) ∈ V
9 5 7 8 ovmpoa ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ) = ( 𝑋f + 𝑌 ) )