Theorem mendval 41925

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 3493	. 2 ⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V)
2		oveq12 7418	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑚 = 𝑀) → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
3	2	anidms 568	. . . . . 6 ⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
4		mendval.b	. . . . . 6 ⊢ 𝐵 = (𝑀 LMHom 𝑀)
5	3, 4	eqtr4di 2791	. . . . 5 ⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = 𝐵)
6	5	csbeq1d 3898	. . . 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 7442	. . . . . 6 ⊢ (𝑚 LMHom 𝑚) ∈ V
8	5, 7	eqeltrrdi 2843	. . . . 5 ⊢ (𝑚 = 𝑀 → 𝐵 ∈ V)
9		simpr 486	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
10	9	opeq2d 4881	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
11		fveq2 6892	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀))
12	11	ofeqd 7672	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → ∘f (+g‘𝑚) = ∘f (+g‘𝑀))
13	12	oveqdr 7437	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘f (+g‘𝑚)𝑦) = (𝑥 ∘f (+g‘𝑀)𝑦))
14	9, 9, 13	mpoeq123dv 7484	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦)))
15		mendval.p	. . . . . . . . 9 ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦))
16	14, 15	eqtr4di 2791	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦)) = + )
17	16	opeq2d 4881	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩ = ⟨(+g‘ndx), + ⟩)
18		eqidd 2734	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘ 𝑦) = (𝑥 ∘ 𝑦))
19	9, 9, 18	mpoeq123dv 7484	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)))
20		mendval.t	. . . . . . . . 9 ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))
21	19, 20	eqtr4di 2791	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = × )
22	21	opeq2d 4881	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩ = ⟨(.r‘ndx), × ⟩)
23	10, 17, 22	tpeq123d 4753	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
24		fveq2 6892	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀))
25	24	adantr 482	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = (Scalar‘𝑀))
26		mendval.s	. . . . . . . . 9 ⊢ 𝑆 = (Scalar‘𝑀)
27	25, 26	eqtr4di 2791	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = 𝑆)
28	27	opeq2d 4881	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(Scalar‘ndx), (Scalar‘𝑚)⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
29	27	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘(Scalar‘𝑚)) = (Base‘𝑆))
30		fveq2 6892	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → ( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀))
31	30	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀))
32	31	ofeqd 7672	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ∘f ( ·𝑠 ‘𝑚) = ∘f ( ·𝑠 ‘𝑀))
33		fveq2 6892	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
34	33	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘𝑚) = (Base‘𝑀))
35	34	xpeq1d 5706	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ((Base‘𝑚) × {𝑥}) = ((Base‘𝑀) × {𝑥}))
36		eqidd 2734	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑦 = 𝑦)
37	32, 35, 36	oveq123d 7430	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦))
38	29, 9, 37	mpoeq123dv 7484	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦)) = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦)))
39		mendval.v	. . . . . . . . 9 ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦))
40	38, 39	eqtr4di 2791	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦)) = · )
41	40	opeq2d 4881	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
42	28, 41	preq12d 4746	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})
43	23, 42	uneq12d 4165	. . . . 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 3932	. . . 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 2773	. . 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 41918	. . 3 ⊢ MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩}))
47		tpex 7734	. . . 4 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
48		prex 5433	. . . 4 ⊢ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩} ∈ V
49	47, 48	unex 7733	. . 3 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}) ∈ V
50	45, 46, 49	fvmpt 6999	. 2 ⊢ (𝑀 ∈ V → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
51	1, 50	syl 17	1 ⊢ (𝑀 ∈ 𝑋 → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ⦋csb 3894   ∪ cun 3947  {csn 4629  {cpr 4631  {ctp 4633  ⟨cop 4635   × cxp 5675   ∘ ccom 5681  ‘cfv 6544  (class class class)co 7409   ∈ cmpo 7411   ∘_f cof 7668  ndxcnx 17126  Basecbs 17144  +_gcplusg 17197  ._rcmulr 17198  Scalarcsca 17200   ·_𝑠 cvsca 17201   LMHom clmhm 20630  MEndocmend 41917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-mend 41918

This theorem is referenced by:  mendbas  41926  mendplusgfval  41927  mendmulrfval  41929  mendsca  41931  mendvscafval  41932