Theorem mendsca

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

	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		df-sca	⊢ Scalar = Slot 5
16	15	str0	⊢ ∅ = ( Scalar ‘ ∅ )
17		fvprc	⊢ ( ¬ 𝑀 ∈ V → ( Scalar ‘ 𝑀 ) = ∅ )
18		fvprc	⊢ ( ¬ 𝑀 ∈ V → ( MEndo ‘ 𝑀 ) = ∅ )
19	18	fveq2d	⊢ ( ¬ 𝑀 ∈ V → ( Scalar ‘ ( MEndo ‘ 𝑀 ) ) = ( Scalar ‘ ∅ ) )
20	16 17 19	3eqtr4a	⊢ ( ¬ 𝑀 ∈ V → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ ( MEndo ‘ 𝑀 ) ) )
21	14 20	pm2.61i	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ ( MEndo ‘ 𝑀 ) )
22	1	fveq2i	⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ( MEndo ‘ 𝑀 ) )
23	21 2 22	3eqtr4i	⊢ 𝑆 = ( Scalar ‘ 𝐴 )