Theorem mendvscafval

Description: Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-2024)

	Ref	Expression
Hypotheses	mendvscafval.a	⊢ 𝐴 = ( MEndo ‘ 𝑀 )
	mendvscafval.v	⊢ · = ( ·𝑠 ‘ 𝑀 )
	mendvscafval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mendvscafval.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	mendvscafval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	mendvscafval.e	⊢ 𝐸 = ( Base ‘ 𝑀 )
Assertion	mendvscafval	⊢ ( ·𝑠 ‘ 𝐴 ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		mendvscafval.a	⊢ 𝐴 = ( MEndo ‘ 𝑀 )
2		mendvscafval.v	⊢ · = ( ·𝑠 ‘ 𝑀 )
3		mendvscafval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mendvscafval.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
5		mendvscafval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
6		mendvscafval.e	⊢ 𝐸 = ( Base ‘ 𝑀 )
7	1	fveq2i	⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ ( MEndo ‘ 𝑀 ) )
8	1	mendbas	⊢ ( 𝑀 LMHom 𝑀 ) = ( Base ‘ 𝐴 )
9	3 8	eqtr4i	⊢ 𝐵 = ( 𝑀 LMHom 𝑀 )
10		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) )
11		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) )
12		eqid	⊢ 𝐵 = 𝐵
13	6	xpeq1i	⊢ ( 𝐸 × { 𝑥 } ) = ( ( Base ‘ 𝑀 ) × { 𝑥 } )
14		eqid	⊢ 𝑦 = 𝑦
15		ofeq	⊢ ( · = ( ·𝑠 ‘ 𝑀 ) → ∘f · = ∘f ( ·𝑠 ‘ 𝑀 ) )
16	2 15	ax-mp	⊢ ∘f · = ∘f ( ·𝑠 ‘ 𝑀 )
17	13 14 16	oveq123i	⊢ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) = ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 )
18	5 12 17	mpoeq123i	⊢ ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑆 ) , 𝑦 ∈ 𝐵 ↦ ( ( ( Base ‘ 𝑀 ) × { 𝑥 } ) ∘f ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
19	9 10 11 4 18	mendval	⊢ ( 𝑀 ∈ V → ( MEndo ‘ 𝑀 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) ⟩ } ) )
20	19	fveq2d	⊢ ( 𝑀 ∈ V → ( ·𝑠 ‘ ( MEndo ‘ 𝑀 ) ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) ⟩ } ) ) )
21	5	fvexi	⊢ 𝐾 ∈ V
22	3	fvexi	⊢ 𝐵 ∈ V
23	21 22	mpoex	⊢ ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) ∈ V
24		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) ⟩ } )
25	24	algvsca	⊢ ( ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) ∈ V → ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) ⟩ } ) ) )
26	23 25	mp1i	⊢ ( 𝑀 ∈ V → ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) = ( ·𝑠 ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ∘ 𝑦 ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑆 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) ⟩ } ) ) )
27	20 26	eqtr4d	⊢ ( 𝑀 ∈ V → ( ·𝑠 ‘ ( MEndo ‘ 𝑀 ) ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) )
28		fvprc	⊢ ( ¬ 𝑀 ∈ V → ( MEndo ‘ 𝑀 ) = ∅ )
29	28	fveq2d	⊢ ( ¬ 𝑀 ∈ V → ( ·𝑠 ‘ ( MEndo ‘ 𝑀 ) ) = ( ·𝑠 ‘ ∅ ) )
30		vscaid	⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )
31	30	str0	⊢ ∅ = ( ·𝑠 ‘ ∅ )
32	29 31	eqtr4di	⊢ ( ¬ 𝑀 ∈ V → ( ·𝑠 ‘ ( MEndo ‘ 𝑀 ) ) = ∅ )
33		fvprc	⊢ ( ¬ 𝑀 ∈ V → ( Scalar ‘ 𝑀 ) = ∅ )
34	4 33	syl5eq	⊢ ( ¬ 𝑀 ∈ V → 𝑆 = ∅ )
35	34	fveq2d	⊢ ( ¬ 𝑀 ∈ V → ( Base ‘ 𝑆 ) = ( Base ‘ ∅ ) )
36		base0	⊢ ∅ = ( Base ‘ ∅ )
37	35 5 36	3eqtr4g	⊢ ( ¬ 𝑀 ∈ V → 𝐾 = ∅ )
38	37	orcd	⊢ ( ¬ 𝑀 ∈ V → ( 𝐾 = ∅ ∨ 𝐵 = ∅ ) )
39		0mpo0	⊢ ( ( 𝐾 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) = ∅ )
40	38 39	syl	⊢ ( ¬ 𝑀 ∈ V → ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) = ∅ )
41	32 40	eqtr4d	⊢ ( ¬ 𝑀 ∈ V → ( ·𝑠 ‘ ( MEndo ‘ 𝑀 ) ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) ) )
42	27 41	pm2.61i	⊢ ( ·𝑠 ‘ ( MEndo ‘ 𝑀 ) ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) )
43	7 42	eqtri	⊢ ( ·𝑠 ‘ 𝐴 ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( ( 𝐸 × { 𝑥 } ) ∘f · 𝑦 ) )