Theorem mendval 40924

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 3440	. 2 ⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V)
2		oveq12 7264	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑚 = 𝑀) → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
3	2	anidms 566	. . . . . 6 ⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
4		mendval.b	. . . . . 6 ⊢ 𝐵 = (𝑀 LMHom 𝑀)
5	3, 4	eqtr4di 2797	. . . . 5 ⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = 𝐵)
6	5	csbeq1d 3832	. . . 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 7288	. . . . . 6 ⊢ (𝑚 LMHom 𝑚) ∈ V
8	5, 7	eqeltrrdi 2848	. . . . 5 ⊢ (𝑚 = 𝑀 → 𝐵 ∈ V)
9		simpr 484	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
10	9	opeq2d 4808	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
11		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀))
12	11	ofeqd 7513	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → ∘f (+g‘𝑚) = ∘f (+g‘𝑀))
13	12	oveqdr 7283	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘f (+g‘𝑚)𝑦) = (𝑥 ∘f (+g‘𝑀)𝑦))
14	9, 9, 13	mpoeq123dv 7328	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦)))
15		mendval.p	. . . . . . . . 9 ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦))
16	14, 15	eqtr4di 2797	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦)) = + )
17	16	opeq2d 4808	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩ = ⟨(+g‘ndx), + ⟩)
18		eqidd 2739	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘ 𝑦) = (𝑥 ∘ 𝑦))
19	9, 9, 18	mpoeq123dv 7328	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)))
20		mendval.t	. . . . . . . . 9 ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))
21	19, 20	eqtr4di 2797	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = × )
22	21	opeq2d 4808	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩ = ⟨(.r‘ndx), × ⟩)
23	10, 17, 22	tpeq123d 4681	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
24		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀))
25	24	adantr 480	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = (Scalar‘𝑀))
26		mendval.s	. . . . . . . . 9 ⊢ 𝑆 = (Scalar‘𝑀)
27	25, 26	eqtr4di 2797	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = 𝑆)
28	27	opeq2d 4808	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(Scalar‘ndx), (Scalar‘𝑚)⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
29	27	fveq2d 6760	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘(Scalar‘𝑚)) = (Base‘𝑆))
30		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → ( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀))
31	30	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀))
32	31	ofeqd 7513	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ∘f ( ·𝑠 ‘𝑚) = ∘f ( ·𝑠 ‘𝑀))
33		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
34	33	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘𝑚) = (Base‘𝑀))
35	34	xpeq1d 5609	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ((Base‘𝑚) × {𝑥}) = ((Base‘𝑀) × {𝑥}))
36		eqidd 2739	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑦 = 𝑦)
37	32, 35, 36	oveq123d 7276	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦))
38	29, 9, 37	mpoeq123dv 7328	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦)) = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦)))
39		mendval.v	. . . . . . . . 9 ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦))
40	38, 39	eqtr4di 2797	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦)) = · )
41	40	opeq2d 4808	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
42	28, 41	preq12d 4674	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})
43	23, 42	uneq12d 4094	. . . . 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 3866	. . . 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 2778	. . 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 40917	. . 3 ⊢ MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩}))
47		tpex 7575	. . . 4 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
48		prex 5350	. . . 4 ⊢ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩} ∈ V
49	47, 48	unex 7574	. . 3 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}) ∈ V
50	45, 46, 49	fvmpt 6857	. 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 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ⦋csb 3828   ∪ cun 3881  {csn 4558  {cpr 4560  {ctp 4562  ⟨cop 4564   × cxp 5578   ∘ ccom 5584  ‘cfv 6418  (class class class)co 7255   ∈ cmpo 7257   ∘_f cof 7509  ndxcnx 16822  Basecbs 16840  +_gcplusg 16888  ._rcmulr 16889  Scalarcsca 16891   ·_𝑠 cvsca 16892   LMHom clmhm 20196  MEndocmend 40916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-of 7511  df-mend 40917

This theorem is referenced by:  mendbas  40925  mendplusgfval  40926  mendmulrfval  40928  mendsca  40930  mendvscafval  40931