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