Theorem mendbas

Description: Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015)

	Ref	Expression
Hypothesis	mendbas.a	⊢ 𝐴 = ( MEndo ‘ 𝑀 )
Assertion	mendbas	⊢ ( 𝑀 LMHom 𝑀 ) = ( Base ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mendbas.a	⊢ 𝐴 = ( MEndo ‘ 𝑀 )
2		ovex	⊢ ( 𝑀 LMHom 𝑀 ) ∈ V
3		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 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } )
4	3	algbase	⊢ ( ( 𝑀 LMHom 𝑀 ) ∈ V → ( 𝑀 LMHom 𝑀 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) ) )
5	2 4	mp1i	⊢ ( 𝑀 ∈ V → ( 𝑀 LMHom 𝑀 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) ) )
6		eqid	⊢ ( 𝑀 LMHom 𝑀 ) = ( 𝑀 LMHom 𝑀 )
7		eqid	⊢ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) )
8		eqid	⊢ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) )
9		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
10		eqid	⊢ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
11	6 7 8 9 10	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 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) )
12	1 11	syl5eq	⊢ ( 𝑀 ∈ V → 𝐴 = ( { ⟨ ( 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 → ( Base ‘ 𝐴 ) = ( Base ‘ ( { ⟨ ( Base ‘ ndx ) , ( 𝑀 LMHom 𝑀 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑀 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) , 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ⟩ } ) ) )
14	5 13	eqtr4d	⊢ ( 𝑀 ∈ V → ( 𝑀 LMHom 𝑀 ) = ( Base ‘ 𝐴 ) )
15		base0	⊢ ∅ = ( Base ‘ ∅ )
16		reldmlmhm	⊢ Rel dom LMHom
17	16	ovprc1	⊢ ( ¬ 𝑀 ∈ V → ( 𝑀 LMHom 𝑀 ) = ∅ )
18		fvprc	⊢ ( ¬ 𝑀 ∈ V → ( MEndo ‘ 𝑀 ) = ∅ )
19	1 18	syl5eq	⊢ ( ¬ 𝑀 ∈ V → 𝐴 = ∅ )
20	19	fveq2d	⊢ ( ¬ 𝑀 ∈ V → ( Base ‘ 𝐴 ) = ( Base ‘ ∅ ) )
21	15 17 20	3eqtr4a	⊢ ( ¬ 𝑀 ∈ V → ( 𝑀 LMHom 𝑀 ) = ( Base ‘ 𝐴 ) )
22	14 21	pm2.61i	⊢ ( 𝑀 LMHom 𝑀 ) = ( Base ‘ 𝐴 )