Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . 5
⊢
(Scalar‘𝑀)
∈ V |
2 | | eqid 2610 |
. . . . . 6
⊢
({〈(Base‘ndx), (𝑀 LMHom 𝑀)〉, 〈(+g‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}) = ({〈(Base‘ndx), (𝑀 LMHom 𝑀)〉, 〈(+g‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}) |
3 | 2 | algsca 36770 |
. . . . 5
⊢
((Scalar‘𝑀)
∈ V → (Scalar‘𝑀) = (Scalar‘({〈(Base‘ndx),
(𝑀 LMHom 𝑀)〉, 〈(+g‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}))) |
4 | 1, 3 | mp1i 13 |
. . . 4
⊢ (𝑀 ∈ V →
(Scalar‘𝑀) =
(Scalar‘({〈(Base‘ndx), (𝑀 LMHom 𝑀)〉, 〈(+g‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}))) |
5 | | eqid 2610 |
. . . . . 6
⊢ (𝑀 LMHom 𝑀) = (𝑀 LMHom 𝑀) |
6 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦)) = (𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦)) |
7 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘ 𝑦)) |
8 | | eqid 2610 |
. . . . . 6
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
9 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈
(Base‘(Scalar‘𝑀)), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) = (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) |
10 | 5, 6, 7, 8, 9 | mendval 36772 |
. . . . 5
⊢ (𝑀 ∈ V →
(MEndo‘𝑀) =
({〈(Base‘ndx), (𝑀 LMHom 𝑀)〉, 〈(+g‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉})) |
11 | 10 | fveq2d 6107 |
. . . 4
⊢ (𝑀 ∈ V →
(Scalar‘(MEndo‘𝑀)) = (Scalar‘({〈(Base‘ndx),
(𝑀 LMHom 𝑀)〉, 〈(+g‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ (𝑀 LMHom 𝑀), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ (𝑀 LMHom 𝑀) ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}))) |
12 | 4, 11 | eqtr4d 2647 |
. . 3
⊢ (𝑀 ∈ V →
(Scalar‘𝑀) =
(Scalar‘(MEndo‘𝑀))) |
13 | | df-sca 15784 |
. . . . 5
⊢ Scalar =
Slot 5 |
14 | 13 | str0 15739 |
. . . 4
⊢ ∅ =
(Scalar‘∅) |
15 | | fvprc 6097 |
. . . 4
⊢ (¬
𝑀 ∈ V →
(Scalar‘𝑀) =
∅) |
16 | | fvprc 6097 |
. . . . 5
⊢ (¬
𝑀 ∈ V →
(MEndo‘𝑀) =
∅) |
17 | 16 | fveq2d 6107 |
. . . 4
⊢ (¬
𝑀 ∈ V →
(Scalar‘(MEndo‘𝑀)) =
(Scalar‘∅)) |
18 | 14, 15, 17 | 3eqtr4a 2670 |
. . 3
⊢ (¬
𝑀 ∈ V →
(Scalar‘𝑀) =
(Scalar‘(MEndo‘𝑀))) |
19 | 12, 18 | pm2.61i 175 |
. 2
⊢
(Scalar‘𝑀) =
(Scalar‘(MEndo‘𝑀)) |
20 | | mendsca.s |
. 2
⊢ 𝑆 = (Scalar‘𝑀) |
21 | | mendsca.a |
. . 3
⊢ 𝐴 = (MEndo‘𝑀) |
22 | 21 | fveq2i 6106 |
. 2
⊢
(Scalar‘𝐴) =
(Scalar‘(MEndo‘𝑀)) |
23 | 19, 20, 22 | 3eqtr4i 2642 |
1
⊢ 𝑆 = (Scalar‘𝐴) |