Theorem mendval 41496

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 3463	. 2 ⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V)
2		oveq12 7366	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑚 = 𝑀) → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
3	2	anidms 567	. . . . . 6 ⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
4		mendval.b	. . . . . 6 ⊢ 𝐵 = (𝑀 LMHom 𝑀)
5	3, 4	eqtr4di 2794	. . . . 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 7390	. . . . . 6 ⊢ (𝑚 LMHom 𝑚) ∈ V
8	5, 7	eqeltrrdi 2847	. . . . 5 ⊢ (𝑚 = 𝑀 → 𝐵 ∈ V)
9		simpr 485	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
10	9	opeq2d 4837	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
11		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀))
12	11	ofeqd 7619	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → ∘f (+g‘𝑚) = ∘f (+g‘𝑀))
13	12	oveqdr 7385	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘f (+g‘𝑚)𝑦) = (𝑥 ∘f (+g‘𝑀)𝑦))
14	9, 9, 13	mpoeq123dv 7432	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦)))
15		mendval.p	. . . . . . . . 9 ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f (+g‘𝑀)𝑦))
16	14, 15	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦)) = + )
17	16	opeq2d 4837	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩ = ⟨(+g‘ndx), + ⟩)
18		eqidd 2737	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘ 𝑦) = (𝑥 ∘ 𝑦))
19	9, 9, 18	mpoeq123dv 7432	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)))
20		mendval.t	. . . . . . . . 9 ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))
21	19, 20	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = × )
22	21	opeq2d 4837	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩ = ⟨(.r‘ndx), × ⟩)
23	10, 17, 22	tpeq123d 4709	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
24		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀))
25	24	adantr 481	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = (Scalar‘𝑀))
26		mendval.s	. . . . . . . . 9 ⊢ 𝑆 = (Scalar‘𝑀)
27	25, 26	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = 𝑆)
28	27	opeq2d 4837	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(Scalar‘ndx), (Scalar‘𝑚)⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
29	27	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘(Scalar‘𝑚)) = (Base‘𝑆))
30		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → ( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀))
31	30	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀))
32	31	ofeqd 7619	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ∘f ( ·𝑠 ‘𝑚) = ∘f ( ·𝑠 ‘𝑀))
33		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
34	33	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘𝑚) = (Base‘𝑀))
35	34	xpeq1d 5662	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ((Base‘𝑚) × {𝑥}) = ((Base‘𝑀) × {𝑥}))
36		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑦 = 𝑦)
37	32, 35, 36	oveq123d 7378	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦))
38	29, 9, 37	mpoeq123dv 7432	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦)) = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦)))
39		mendval.v	. . . . . . . . 9 ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f ( ·𝑠 ‘𝑀)𝑦))
40	38, 39	eqtr4di 2794	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦)) = · )
41	40	opeq2d 4837	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
42	28, 41	preq12d 4702	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})
43	23, 42	uneq12d 4124	. . . . 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 3893	. . . 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 2776	. . 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 41489	. . 3 ⊢ MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f ( ·𝑠 ‘𝑚)𝑦))⟩}))
47		tpex 7681	. . . 4 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
48		prex 5389	. . . 4 ⊢ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩} ∈ V
49	47, 48	unex 7680	. . 3 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}) ∈ V
50	45, 46, 49	fvmpt 6948	. 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 396   = wceq 1541   ∈ wcel 2106  Vcvv 3445  ⦋csb 3855   ∪ cun 3908  {csn 4586  {cpr 4588  {ctp 4590  ⟨cop 4592   × cxp 5631   ∘ ccom 5637  ‘cfv 6496  (class class class)co 7357   ∈ cmpo 7359   ∘_f cof 7615  ndxcnx 17065  Basecbs 17083  +_gcplusg 17133  ._rcmulr 17134  Scalarcsca 17136   ·_𝑠 cvsca 17137   LMHom clmhm 20480  MEndocmend 41488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-iota 6448  df-fun 6498  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-mend 41489

This theorem is referenced by:  mendbas  41497  mendplusgfval  41498  mendmulrfval  41500  mendsca  41502  mendvscafval  41503