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