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 ‘ 𝐴 )