Metamath Proof Explorer

Theorem mendmulrfval

Description: Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-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 mulrid ⊢ .r = Slot ( .r ‘ ndx )
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 ‘ 𝐴 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) )