Metamath Proof Explorer


Theorem mendplusgfval

Description: Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-2024)

Ref Expression
Hypotheses mendplusgfval.a 𝐴 = ( MEndo ‘ 𝑀 )
mendplusgfval.b 𝐵 = ( Base ‘ 𝐴 )
mendplusgfval.p + = ( +g𝑀 )
Assertion mendplusgfval ( +g𝐴 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) )

Proof

Step Hyp Ref Expression
1 mendplusgfval.a 𝐴 = ( MEndo ‘ 𝑀 )
2 mendplusgfval.b 𝐵 = ( Base ‘ 𝐴 )
3 mendplusgfval.p + = ( +g𝑀 )
4 1 mendbas ( 𝑀 LMHom 𝑀 ) = ( Base ‘ 𝐴 )
5 2 4 eqtr4i 𝐵 = ( 𝑀 LMHom 𝑀 )
6 ofeq ( + = ( +g𝑀 ) → ∘f + = ∘f ( +g𝑀 ) )
7 3 6 ax-mp f + = ∘f ( +g𝑀 )
8 7 oveqi ( 𝑥f + 𝑦 ) = ( 𝑥f ( +g𝑀 ) 𝑦 )
9 8 a1i ( ( 𝑥𝐵𝑦𝐵 ) → ( 𝑥f + 𝑦 ) = ( 𝑥f ( +g𝑀 ) 𝑦 ) )
10 9 mpoeq3ia ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f ( +g𝑀 ) 𝑦 ) )
11 eqid ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) )
12 eqid ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
13 eqid ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) )
14 5 10 11 12 13 mendval ( 𝑀 ∈ V → ( MEndo ‘ 𝑀 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) ) ⟩ } ) )
15 1 14 syl5eq ( 𝑀 ∈ V → 𝐴 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) ) ⟩ } ) )
16 15 fveq2d ( 𝑀 ∈ V → ( +g𝐴 ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) ) ⟩ } ) ) )
17 2 fvexi 𝐵 ∈ V
18 17 17 mpoex ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ∈ V
19 eqid ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) ) ⟩ } )
20 19 algaddg ( ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ∈ V → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) ) ⟩ } ) ) )
21 18 20 mp1i ( 𝑀 ∈ V → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠𝑀 ) 𝑦 ) ) ⟩ } ) ) )
22 16 21 eqtr4d ( 𝑀 ∈ V → ( +g𝐴 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) )
23 fvprc ( ¬ 𝑀 ∈ V → ( MEndo ‘ 𝑀 ) = ∅ )
24 1 23 syl5eq ( ¬ 𝑀 ∈ V → 𝐴 = ∅ )
25 24 fveq2d ( ¬ 𝑀 ∈ V → ( +g𝐴 ) = ( +g ‘ ∅ ) )
26 plusgid +g = Slot ( +g ‘ ndx )
27 26 str0 ∅ = ( +g ‘ ∅ )
28 25 27 eqtr4di ( ¬ 𝑀 ∈ V → ( +g𝐴 ) = ∅ )
29 24 fveq2d ( ¬ 𝑀 ∈ V → ( Base ‘ 𝐴 ) = ( Base ‘ ∅ ) )
30 base0 ∅ = ( Base ‘ ∅ )
31 29 2 30 3eqtr4g ( ¬ 𝑀 ∈ V → 𝐵 = ∅ )
32 31 olcd ( ¬ 𝑀 ∈ V → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
33 0mpo0 ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) = ∅ )
34 32 33 syl ( ¬ 𝑀 ∈ V → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) = ∅ )
35 28 34 eqtr4d ( ¬ 𝑀 ∈ V → ( +g𝐴 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) ) )
36 22 35 pm2.61i ( +g𝐴 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥f + 𝑦 ) )