Theorem mendval 38589

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

Hypotheses

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

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 3429	. 2 ⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V)
2		oveq12 6914	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑚 = 𝑀) → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
3	2	anidms 562	. . . . . 6 ⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀))
4		mendval.b	. . . . . 6 ⊢ 𝐵 = (𝑀 LMHom 𝑀)
5	3, 4	syl6eqr 2879	. . . . 5 ⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = 𝐵)
6	5	csbeq1d 3764	. . . 4 ⊢ (𝑚 = 𝑀 → ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))⟩}) = ⦋𝐵 / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))⟩}))
7		ovex 6937	. . . . . 6 ⊢ (𝑚 LMHom 𝑚) ∈ V
8	5, 7	syl6eqelr 2915	. . . . 5 ⊢ (𝑚 = 𝑀 → 𝐵 ∈ V)
9		simpr 479	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
10	9	opeq2d 4630	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
11		fveq2 6433	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀))
12		ofeq 7159	. . . . . . . . . . . 12 ⊢ ((+g‘𝑚) = (+g‘𝑀) → ∘𝑓 (+g‘𝑚) = ∘𝑓 (+g‘𝑀))
13	11, 12	syl 17	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → ∘𝑓 (+g‘𝑚) = ∘𝑓 (+g‘𝑀))
14	13	oveqdr 6933	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘𝑓 (+g‘𝑚)𝑦) = (𝑥 ∘𝑓 (+g‘𝑀)𝑦))
15	9, 9, 14	mpt2eq123dv 6977	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 (+g‘𝑀)𝑦)))
16		mendval.p	. . . . . . . . 9 ⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 (+g‘𝑀)𝑦))
17	15, 16	syl6eqr 2879	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦)) = + )
18	17	opeq2d 4630	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))⟩ = ⟨(+g‘ndx), + ⟩)
19		eqidd 2826	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘ 𝑦) = (𝑥 ∘ 𝑦))
20	9, 9, 19	mpt2eq123dv 6977	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)))
21		mendval.t	. . . . . . . . 9 ⊢ × = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))
22	20, 21	syl6eqr 2879	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = × )
23	22	opeq2d 4630	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩ = ⟨(.r‘ndx), × ⟩)
24	10, 18, 23	tpeq123d 4501	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩})
25		fveq2 6433	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀))
26	25	adantr 474	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = (Scalar‘𝑀))
27		mendval.s	. . . . . . . . 9 ⊢ 𝑆 = (Scalar‘𝑀)
28	26, 27	syl6eqr 2879	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = 𝑆)
29	28	opeq2d 4630	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨(Scalar‘ndx), (Scalar‘𝑚)⟩ = ⟨(Scalar‘ndx), 𝑆⟩)
30	28	fveq2d 6437	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘(Scalar‘𝑚)) = (Base‘𝑆))
31		fveq2 6433	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → ( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀))
32	31	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀))
33		ofeq 7159	. . . . . . . . . . . 12 ⊢ (( ·𝑠 ‘𝑚) = ( ·𝑠 ‘𝑀) → ∘𝑓 ( ·𝑠 ‘𝑚) = ∘𝑓 ( ·𝑠 ‘𝑀))
34	32, 33	syl 17	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ∘𝑓 ( ·𝑠 ‘𝑚) = ∘𝑓 ( ·𝑠 ‘𝑀))
35		fveq2 6433	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀))
36	35	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘𝑚) = (Base‘𝑀))
37	36	xpeq1d 5371	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ((Base‘𝑚) × {𝑥}) = ((Base‘𝑀) × {𝑥}))
38		eqidd 2826	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑦 = 𝑦)
39	34, 37, 38	oveq123d 6926	. . . . . . . . . 10 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦) = (((Base‘𝑀) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑀)𝑦))
40	30, 9, 39	mpt2eq123dv 6977	. . . . . . . . 9 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦)) = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑀)𝑦)))
41		mendval.v	. . . . . . . . 9 ⊢ · = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑀)𝑦))
42	40, 41	syl6eqr 2879	. . . . . . . 8 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦)) = · )
43	42	opeq2d 4630	. . . . . . 7 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
44	29, 43	preq12d 4494	. . . . . 6 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))⟩} = {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩})
45	24, 44	uneq12d 3995	. . . . 5 ⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
46	8, 45	csbied 3784	. . . 4 ⊢ (𝑚 = 𝑀 → ⦋𝐵 / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
47	6, 46	eqtrd 2861	. . 3 ⊢ (𝑚 = 𝑀 → ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))⟩}) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
48		df-mend 38582	. . 3 ⊢ MEndo = (𝑚 ∈ V ↦ ⦋(𝑚 LMHom 𝑚) / 𝑏⦌({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘𝑓 (+g‘𝑚)𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑚)⟩, ⟨( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘𝑓 ( ·𝑠 ‘𝑚)𝑦))⟩}))
49		tpex 7217	. . . 4 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∈ V
50		prex 5130	. . . 4 ⊢ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩} ∈ V
51	49, 50	unex 7216	. . 3 ⊢ ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}) ∈ V
52	47, 48, 51	fvmpt 6529	. 2 ⊢ (𝑀 ∈ V → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))
53	1, 52	syl 17	1 ⊢ (𝑀 ∈ 𝑋 → (MEndo‘𝑀) = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩}))

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1656   ∈ wcel 2164  Vcvv 3414  ⦋csb 3757   ∪ cun 3796  {csn 4397  {cpr 4399  {ctp 4401  ⟨cop 4403   × cxp 5340   ∘ ccom 5346  ‘cfv 6123  (class class class)co 6905   ↦ cmpt2 6907   ∘_𝑓 cof 7155  ndxcnx 16219  Basecbs 16222  +_gcplusg 16305  ._rcmulr 16306  Scalarcsca 16308   ·_𝑠 cvsca 16309   LMHom clmhm 19378  MEndocmend 38581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-iota 6086  df-fun 6125  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-of 7157  df-mend 38582

This theorem is referenced by:  mendbas  38590  mendplusgfval  38591  mendmulrfval  38593  mendsca  38595  mendvscafval  38596