Metamath Proof Explorer

Theorem mendval

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

Ref Expression
Hypotheses mendval.b ⊢ 𝐵 = ( 𝑀 LMHom 𝑀 )
mendval.p ⊢ + = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) )
mendval.t ⊢ × = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) )
mendval.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
mendval.v ⊢ · = ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ 𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
Assertion mendval ( 𝑀 ∈ 𝑋 → ( MEndo ‘ 𝑀 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) )

Proof

Step Hyp Ref Expression
1 mendval.b ⊢ 𝐵 = ( 𝑀 LMHom 𝑀 )
2 mendval.p ⊢ + = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) )
3 mendval.t ⊢ × = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) )
4 mendval.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
5 mendval.v ⊢ · = ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ 𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
6 elex ⊢ ( 𝑀 ∈ 𝑋 → 𝑀 ∈ V )
7 oveq12 ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑚 = 𝑀 ) → ( 𝑚 LMHom 𝑚 ) = ( 𝑀 LMHom 𝑀 ) )
8 7 anidms ⊢ ( 𝑚 = 𝑀 → ( 𝑚 LMHom 𝑚 ) = ( 𝑀 LMHom 𝑀 ) )
9 8 1 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( 𝑚 LMHom 𝑚 ) = 𝐵 )
10 9 csbeq1d ⊢ ( 𝑚 = 𝑀 → ⦋ ( 𝑚 LMHom 𝑚 ) / 𝑏 ⦌ ( { ⟨ ( 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 ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } ) )
11 ovex ⊢ ( 𝑚 LMHom 𝑚 ) ∈ V
12 9 11 eqeltrrdi ⊢ ( 𝑚 = 𝑀 → 𝐵 ∈ V )
13 simpr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
14 13 opeq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ )
15 fveq2 ⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
16 ofeq ⊢ ( ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) → ∘f ( +g ‘ 𝑚 ) = ∘f ( +g ‘ 𝑀 ) )
17 15 16 syl ⊢ ( 𝑚 = 𝑀 → ∘f ( +g ‘ 𝑚 ) = ∘f ( +g ‘ 𝑀 ) )
18 17 oveqdr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) )
19 13 13 18 mpoeq123dv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) )
20 19 2 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) = + )
21 20 opeq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ = ⟨ ( +g ‘ ndx ) , + ⟩ )
22 eqidd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∘ 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
23 13 13 22 mpoeq123dv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) ) )
24 23 3 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) = × )
25 24 opeq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ = ⟨ ( .r ‘ ndx ) , × ⟩ )
26 14 21 25 tpeq123d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } )
27 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Scalar ‘ 𝑚 ) = ( Scalar ‘ 𝑀 ) )
28 27 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( Scalar ‘ 𝑚 ) = ( Scalar ‘ 𝑀 ) )
29 28 4 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( Scalar ‘ 𝑚 ) = 𝑆 )
30 29 opeq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ = ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ )
31 29 fveq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑚 ) ) = ( Base ‘ 𝑆 ) )
32 fveq2 ⊢ ( 𝑚 = 𝑀 → ( ·𝑠 ‘ 𝑚 ) = ( ·𝑠 ‘ 𝑀 ) )
33 32 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( ·𝑠 ‘ 𝑚 ) = ( ·𝑠 ‘ 𝑀 ) )
34 ofeq ⊢ ( ( ·𝑠 ‘ 𝑚 ) = ( ·𝑠 ‘ 𝑀 ) → ∘f ( ·𝑠 ‘ 𝑚 ) = ∘f ( ·𝑠 ‘ 𝑀 ) )
35 33 34 syl ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ∘f ( ·𝑠 ‘ 𝑚 ) = ∘f ( ·𝑠 ‘ 𝑀 ) )
36 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
37 36 adantr ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
38 37 xpeq1d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( ( Base ‘ 𝑚 ) × { 𝑥 } ) = ( ( Base ‘ 𝑀 ) × { 𝑥 } ) )
39 eqidd ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → 𝑦 = 𝑦 )
40 35 38 39 oveq123d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) = ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
41 31 13 40 mpoeq123dv ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ 𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) )
42 41 5 eqtr4di ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) = · )
43 42 opeq2d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ )
44 30 43 preq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } = { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } )
45 26 44 uneq12d ⊢ ( ( 𝑚 = 𝑀 ∧ 𝑏 = 𝐵 ) → ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) )
46 12 45 csbied ⊢ ( 𝑚 = 𝑀 → ⦋ 𝐵 / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) )
47 10 46 eqtrd ⊢ ( 𝑚 = 𝑀 → ⦋ ( 𝑚 LMHom 𝑚 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) )
48 df-mend ⊢ MEndo = ( 𝑚 ∈ V ↦ ⦋ ( 𝑚 LMHom 𝑚 ) / 𝑏 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘f ( +g ‘ 𝑚 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , ( Scalar ‘ 𝑚 ) ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑚 ) ) , 𝑦 ∈ 𝑏 ↦ ( ( ( Base ‘ 𝑚 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑚 ) 𝑦 ) ) ⟩ } ) )
49 tpex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∈ V
50 prex ⊢ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ∈ V
51 49 50 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) ∈ V
52 47 48 51 fvmpt ⊢ ( 𝑀 ∈ V → ( MEndo ‘ 𝑀 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) )
53 6 52 syl ⊢ ( 𝑀 ∈ 𝑋 → ( MEndo ‘ 𝑀 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , × ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ } ) )