Theorem mendval 43763

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

Hypotheses

Ref	Expression
mendval.b	⊢ 𝐵 = (𝑀 LMHom 𝑀)
mendval.p	⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦))
mendval.t	⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))
mendval.s	⊢ 𝑆 = (Scalar‘𝑀)
mendval.v	⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦))

Assertion

Ref	Expression
mendval	⊢ (𝑀 ∈ 𝑋 → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))

Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝑀,𝑦

Allowed substitution hints:   + (𝑥,𝑦)   𝑆(𝑥,𝑦)   · (𝑥,𝑦)   × (𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem mendval

Dummy variables 𝑚 𝑏 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  Vcvv 3457  ⦋csb 3855   ∪ cun 3905  {csn 4585  {cpr 4587  {ctp 4589  ⟨cop 4591   × cxp 5649   ∘ ccom 5655  ‘cfv 6525  (class class class)co 7400   ∈ cmpo 7402   ∘_f cof 7662  ndxcnx 17241  Basecbs 17257  +_gcplusg 17298  ._rcmulr 17299  Scalarcsca 17301   ·_𝑠 cvsca 17302   LMHom clmhm 21106  MEndocmend 43755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-of 7664  df-mend 43756

This theorem is referenced by:  mendbas  43764  mendplusgfval  43765  mendmulrfval  43767  mendsca  43769  mendvscafval  43770