Metamath Proof Explorer

Theorem mendsca

Description: The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-2024)

Ref Expression
Hypotheses mendsca.a ⊢ 𝐴 = ( MEndo ‘ 𝑀 )
mendsca.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
Assertion mendsca 𝑆 = ( Scalar ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 mendsca.a ⊢ 𝐴 = ( MEndo ‘ 𝑀 )
2 mendsca.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3 fvex ⊢ ( Scalar ‘ 𝑀 ) ∈ V
4 eqid ⊢ ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } )
5 4 algsca ⊢ ( ( Scalar ‘ 𝑀 ) ∈ V → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) ) )
6 3 5 mp1i ⊢ ( 𝑀 ∈ V → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) ) )
7 eqid ⊢ ( 𝑀 LMHom 𝑀 ) = ( 𝑀 LMHom 𝑀 )
8 eqid ⊢ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) )
9 eqid ⊢ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) )
10 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
11 eqid ⊢ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
12 7 8 9 10 11 mendval ⊢ ( 𝑀 ∈ V → ( MEndo ‘ 𝑀 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) )
13 12 fveq2d ⊢ ( 𝑀 ∈ V → ( Scalar ‘ ( MEndo ‘ 𝑀 ) ) = ( Scalar ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) ) )
14 6 13 eqtr4d ⊢ ( 𝑀 ∈ V → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ ( MEndo ‘ 𝑀 ) ) )
15 scaid ⊢ Scalar = Slot ( Scalar ‘ ndx )
16 15 str0 ⊢ ∅ = ( Scalar ‘ ∅ )
17 16 eqcomi ⊢ ( Scalar ‘ ∅ ) = ∅
18 eqid ⊢ ( MEndo ‘ 𝑀 ) = ( MEndo ‘ 𝑀 )
19 17 18 fveqprc ⊢ ( ¬ 𝑀 ∈ V → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ ( MEndo ‘ 𝑀 ) ) )
20 14 19 pm2.61i ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ ( MEndo ‘ 𝑀 ) )
21 1 fveq2i ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ( MEndo ‘ 𝑀 ) )
22 20 2 21 3eqtr4i ⊢ 𝑆 = ( Scalar ‘ 𝐴 )