Metamath Proof Explorer


Theorem mendmulrfval

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

Ref Expression
Hypotheses mendmulrfval.a 𝐴 = ( MEndo ‘ 𝑀 )
mendmulrfval.b 𝐵 = ( Base ‘ 𝐴 )
Assertion mendmulrfval ( .r𝐴 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥𝑦 ) )

Proof

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