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 + 𝑌 ) )