Step | Hyp | Ref
| Expression |
1 | | elex 3439 |
. 2
⊢ (𝑀 ∈ 𝑋 → 𝑀 ∈ V) |
2 | | oveq12 7241 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑚 = 𝑀) → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀)) |
3 | 2 | anidms 570 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = (𝑀 LMHom 𝑀)) |
4 | | mendval.b |
. . . . . 6
⊢ 𝐵 = (𝑀 LMHom 𝑀) |
5 | 3, 4 | eqtr4di 2797 |
. . . . 5
⊢ (𝑚 = 𝑀 → (𝑚 LMHom 𝑚) = 𝐵) |
6 | 5 | csbeq1d 3830 |
. . . 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 7265 |
. . . . . 6
⊢ (𝑚 LMHom 𝑚) ∈ V |
8 | 5, 7 | eqeltrrdi 2848 |
. . . . 5
⊢ (𝑚 = 𝑀 → 𝐵 ∈ V) |
9 | | simpr 488 |
. . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
10 | 9 | opeq2d 4806 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐵〉) |
11 | | fveq2 6736 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀)) |
12 | | ofeq 7490 |
. . . . . . . . . . . 12
⊢
((+g‘𝑚) = (+g‘𝑀) → ∘f
(+g‘𝑚) =
∘f (+g‘𝑀)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → ∘f
(+g‘𝑚) =
∘f (+g‘𝑀)) |
14 | 13 | oveqdr 7260 |
. . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘f
(+g‘𝑚)𝑦) = (𝑥 ∘f
(+g‘𝑀)𝑦)) |
15 | 9, 9, 14 | mpoeq123dv 7305 |
. . . . . . . . 9
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))) |
16 | | mendval.p |
. . . . . . . . 9
⊢ + = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦)) |
17 | 15, 16 | eqtr4di 2797 |
. . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦)) = + ) |
18 | 17 | opeq2d 4806 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 〈(+g‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉 = 〈(+g‘ndx),
+
〉) |
19 | | eqidd 2739 |
. . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∘ 𝑦) = (𝑥 ∘ 𝑦)) |
20 | 9, 9, 19 | mpoeq123dv 7305 |
. . . . . . . . 9
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))) |
21 | | mendval.t |
. . . . . . . . 9
⊢ × =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) |
22 | 20, 21 | eqtr4di 2797 |
. . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦)) = × ) |
23 | 22 | opeq2d 4806 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 〈(.r‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉 = 〈(.r‘ndx),
×
〉) |
24 | 10, 18, 23 | tpeq123d 4679 |
. . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} = {〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), + 〉,
〈(.r‘ndx), ×
〉}) |
25 | | fveq2 6736 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (Scalar‘𝑚) = (Scalar‘𝑀)) |
26 | 25 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = (Scalar‘𝑀)) |
27 | | mendval.s |
. . . . . . . . 9
⊢ 𝑆 = (Scalar‘𝑀) |
28 | 26, 27 | eqtr4di 2797 |
. . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Scalar‘𝑚) = 𝑆) |
29 | 28 | opeq2d 4806 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 〈(Scalar‘ndx),
(Scalar‘𝑚)〉 =
〈(Scalar‘ndx), 𝑆〉) |
30 | 28 | fveq2d 6740 |
. . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘(Scalar‘𝑚)) = (Base‘𝑆)) |
31 | | fveq2 6736 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑀 → (
·𝑠 ‘𝑚) = ( ·𝑠
‘𝑀)) |
32 | 31 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (
·𝑠 ‘𝑚) = ( ·𝑠
‘𝑀)) |
33 | | ofeq 7490 |
. . . . . . . . . . . 12
⊢ ((
·𝑠 ‘𝑚) = ( ·𝑠
‘𝑀) →
∘f ( ·𝑠 ‘𝑚) = ∘f (
·𝑠 ‘𝑀)) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ∘f (
·𝑠 ‘𝑚) = ∘f (
·𝑠 ‘𝑀)) |
35 | | fveq2 6736 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
36 | 35 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (Base‘𝑚) = (Base‘𝑀)) |
37 | 36 | xpeq1d 5595 |
. . . . . . . . . . 11
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → ((Base‘𝑚) × {𝑥}) = ((Base‘𝑀) × {𝑥})) |
38 | | eqidd 2739 |
. . . . . . . . . . 11
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 𝑦 = 𝑦) |
39 | 34, 37, 38 | oveq123d 7253 |
. . . . . . . . . 10
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
40 | 30, 9, 39 | mpoeq123dv 7305 |
. . . . . . . . 9
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦)) = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))) |
41 | | mendval.v |
. . . . . . . . 9
⊢ · =
(𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
42 | 40, 41 | eqtr4di 2797 |
. . . . . . . 8
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦)) = · ) |
43 | 42 | opeq2d 4806 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → 〈(
·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉 = 〈(
·𝑠 ‘ndx), ·
〉) |
44 | 29, 43 | preq12d 4672 |
. . . . . 6
⊢ ((𝑚 = 𝑀 ∧ 𝑏 = 𝐵) → {〈(Scalar‘ndx),
(Scalar‘𝑚)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉} = {〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), ·
〉}) |
45 | 24, 44 | uneq12d 4093 |
. . . . 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), ·
〉})) |
46 | 8, 45 | csbied 3864 |
. . . 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), ·
〉})) |
47 | 6, 46 | 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), ·
〉})) |
48 | | df-mend 40733 |
. . 3
⊢ MEndo =
(𝑚 ∈ V ↦
⦋(𝑚 LMHom
𝑚) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘f
(+g‘𝑚)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑚)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑚)), 𝑦 ∈ 𝑏 ↦ (((Base‘𝑚) × {𝑥}) ∘f (
·𝑠 ‘𝑚)𝑦))〉})) |
49 | | tpex 7551 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
+ 〉,
〈(.r‘ndx), × 〉} ∈
V |
50 | | prex 5340 |
. . . 4
⊢
{〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), · 〉} ∈
V |
51 | 49, 50 | unex 7550 |
. . 3
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
+ 〉,
〈(.r‘ndx), × 〉} ∪
{〈(Scalar‘ndx), 𝑆〉, 〈(
·𝑠 ‘ndx), · 〉}) ∈
V |
52 | 47, 48, 51 | fvmpt 6837 |
. 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), ·
〉})) |