Proof of Theorem mendvscafval
Step | Hyp | Ref
| Expression |
1 | | mendvscafval.a |
. . 3
⊢ 𝐴 = (MEndo‘𝑀) |
2 | 1 | fveq2i 6106 |
. 2
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘(MEndo‘𝑀)) |
3 | | mendvscafval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
4 | 1 | mendbas 36773 |
. . . . . . 7
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
5 | 3, 4 | eqtr4i 2635 |
. . . . . 6
⊢ 𝐵 = (𝑀 LMHom 𝑀) |
6 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦)) |
7 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) |
8 | | mendvscafval.s |
. . . . . 6
⊢ 𝑆 = (Scalar‘𝑀) |
9 | | mendvscafval.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝑆) |
10 | | eqid 2610 |
. . . . . . 7
⊢ 𝐵 = 𝐵 |
11 | | mendvscafval.e |
. . . . . . . . 9
⊢ 𝐸 = (Base‘𝑀) |
12 | 11 | xpeq1i 5059 |
. . . . . . . 8
⊢ (𝐸 × {𝑥}) = ((Base‘𝑀) × {𝑥}) |
13 | | eqid 2610 |
. . . . . . . 8
⊢ 𝑦 = 𝑦 |
14 | | mendvscafval.v |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑀) |
15 | | ofeq 6797 |
. . . . . . . . 9
⊢ ( · = (
·𝑠 ‘𝑀) → ∘𝑓 · =
∘𝑓 ( ·𝑠 ‘𝑀)) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . 8
⊢
∘𝑓 · =
∘𝑓 ( ·𝑠 ‘𝑀) |
17 | 12, 13, 16 | oveq123i 6563 |
. . . . . . 7
⊢ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦) |
18 | 9, 10, 17 | mpt2eq123i 6616 |
. . . . . 6
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) |
19 | 5, 6, 7, 8, 18 | mendval 36772 |
. . . . 5
⊢ (𝑀 ∈ V →
(MEndo‘𝑀) =
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))〉})) |
20 | 19 | fveq2d 6107 |
. . . 4
⊢ (𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = ( ·𝑠
‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))〉}))) |
21 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑆)
∈ V |
22 | 9, 21 | eqeltri 2684 |
. . . . . 6
⊢ 𝐾 ∈ V |
23 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐴)
∈ V |
24 | 3, 23 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
25 | 22, 24 | mpt2ex 7136 |
. . . . 5
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) ∈ V |
26 | | eqid 2610 |
. . . . . 6
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))〉}) =
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))〉}) |
27 | 26 | algvsca 36771 |
. . . . 5
⊢ ((𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) = (
·𝑠 ‘({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))〉}))) |
28 | 25, 27 | mp1i 13 |
. . . 4
⊢ (𝑀 ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) = (
·𝑠 ‘({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))〉}))) |
29 | 20, 28 | eqtr4d 2647 |
. . 3
⊢ (𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))) |
30 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(MEndo‘𝑀) =
∅) |
31 | 30 | fveq2d 6107 |
. . . . 5
⊢ (¬
𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = ( ·𝑠
‘∅)) |
32 | | df-vsca 15785 |
. . . . . 6
⊢
·𝑠 = Slot 6 |
33 | 32 | str0 15739 |
. . . . 5
⊢ ∅ =
( ·𝑠 ‘∅) |
34 | 31, 33 | syl6eqr 2662 |
. . . 4
⊢ (¬
𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = ∅) |
35 | | fvprc 6097 |
. . . . . . . . 9
⊢ (¬
𝑀 ∈ V →
(Scalar‘𝑀) =
∅) |
36 | 8, 35 | syl5eq 2656 |
. . . . . . . 8
⊢ (¬
𝑀 ∈ V → 𝑆 = ∅) |
37 | 36 | fveq2d 6107 |
. . . . . . 7
⊢ (¬
𝑀 ∈ V →
(Base‘𝑆) =
(Base‘∅)) |
38 | | base0 15740 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
39 | 37, 9, 38 | 3eqtr4g 2669 |
. . . . . 6
⊢ (¬
𝑀 ∈ V → 𝐾 = ∅) |
40 | | mpt2eq12 6613 |
. . . . . 6
⊢ ((𝐾 = ∅ ∧ 𝐵 = 𝐵) → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))) |
41 | 39, 10, 40 | sylancl 693 |
. . . . 5
⊢ (¬
𝑀 ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))) |
42 | | mpt20 6623 |
. . . . 5
⊢ (𝑥 ∈ ∅, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) = ∅ |
43 | 41, 42 | syl6eq 2660 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) = ∅) |
44 | 34, 43 | eqtr4d 2647 |
. . 3
⊢ (¬
𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦))) |
45 | 29, 44 | pm2.61i 175 |
. 2
⊢ (
·𝑠 ‘(MEndo‘𝑀)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) |
46 | 2, 45 | eqtri 2632 |
1
⊢ (
·𝑠 ‘𝐴) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘𝑓 · 𝑦)) |