Proof of Theorem mendvscafval
| Step | Hyp | Ref
| Expression |
| 1 | | mendvscafval.a |
. . 3
⊢ 𝐴 = (MEndo‘𝑀) |
| 2 | 1 | fveq2i 6909 |
. 2
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘(MEndo‘𝑀)) |
| 3 | | mendvscafval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
| 4 | 1 | mendbas 43192 |
. . . . . . 7
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
| 5 | 3, 4 | eqtr4i 2768 |
. . . . . 6
⊢ 𝐵 = (𝑀 LMHom 𝑀) |
| 6 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦)) |
| 7 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) |
| 8 | | mendvscafval.s |
. . . . . 6
⊢ 𝑆 = (Scalar‘𝑀) |
| 9 | | mendvscafval.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝑆) |
| 10 | | eqid 2737 |
. . . . . . 7
⊢ 𝐵 = 𝐵 |
| 11 | | mendvscafval.e |
. . . . . . . . 9
⊢ 𝐸 = (Base‘𝑀) |
| 12 | 11 | xpeq1i 5711 |
. . . . . . . 8
⊢ (𝐸 × {𝑥}) = ((Base‘𝑀) × {𝑥}) |
| 13 | | eqid 2737 |
. . . . . . . 8
⊢ 𝑦 = 𝑦 |
| 14 | | mendvscafval.v |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑀) |
| 15 | | ofeq 7700 |
. . . . . . . . 9
⊢ ( · = (
·𝑠 ‘𝑀) → ∘f · =
∘f ( ·𝑠 ‘𝑀)) |
| 16 | 14, 15 | ax-mp 5 |
. . . . . . . 8
⊢
∘f · =
∘f ( ·𝑠 ‘𝑀) |
| 17 | 12, 13, 16 | oveq123i 7445 |
. . . . . . 7
⊢ ((𝐸 × {𝑥}) ∘f · 𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦) |
| 18 | 9, 10, 17 | mpoeq123i 7509 |
. . . . . 6
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) = (𝑥 ∈ (Base‘𝑆), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
| 19 | 5, 6, 7, 8, 18 | mendval 43191 |
. . . . 5
⊢ (𝑀 ∈ V →
(MEndo‘𝑀) =
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))〉})) |
| 20 | 19 | fveq2d 6910 |
. . . 4
⊢ (𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = ( ·𝑠
‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))〉}))) |
| 21 | 9 | fvexi 6920 |
. . . . . 6
⊢ 𝐾 ∈ V |
| 22 | 3 | fvexi 6920 |
. . . . . 6
⊢ 𝐵 ∈ V |
| 23 | 21, 22 | mpoex 8104 |
. . . . 5
⊢ (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) ∈ V |
| 24 | | eqid 2737 |
. . . . . 6
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))〉}) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))〉}) |
| 25 | 24 | algvsca 43190 |
. . . . 5
⊢ ((𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) = ( ·𝑠
‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))〉}))) |
| 26 | 23, 25 | mp1i 13 |
. . . 4
⊢ (𝑀 ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) = ( ·𝑠
‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
𝑆〉, 〈(
·𝑠 ‘ndx), (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))〉}))) |
| 27 | 20, 26 | eqtr4d 2780 |
. . 3
⊢ (𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))) |
| 28 | | fvprc 6898 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(MEndo‘𝑀) =
∅) |
| 29 | 28 | fveq2d 6910 |
. . . . 5
⊢ (¬
𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = ( ·𝑠
‘∅)) |
| 30 | | vscaid 17364 |
. . . . . 6
⊢
·𝑠 = Slot (
·𝑠 ‘ndx) |
| 31 | 30 | str0 17226 |
. . . . 5
⊢ ∅ =
( ·𝑠 ‘∅) |
| 32 | 29, 31 | eqtr4di 2795 |
. . . 4
⊢ (¬
𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = ∅) |
| 33 | | fvprc 6898 |
. . . . . . . . 9
⊢ (¬
𝑀 ∈ V →
(Scalar‘𝑀) =
∅) |
| 34 | 8, 33 | eqtrid 2789 |
. . . . . . . 8
⊢ (¬
𝑀 ∈ V → 𝑆 = ∅) |
| 35 | 34 | fveq2d 6910 |
. . . . . . 7
⊢ (¬
𝑀 ∈ V →
(Base‘𝑆) =
(Base‘∅)) |
| 36 | | base0 17252 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
| 37 | 35, 9, 36 | 3eqtr4g 2802 |
. . . . . 6
⊢ (¬
𝑀 ∈ V → 𝐾 = ∅) |
| 38 | 37 | orcd 874 |
. . . . 5
⊢ (¬
𝑀 ∈ V → (𝐾 = ∅ ∨ 𝐵 = ∅)) |
| 39 | | 0mpo0 7516 |
. . . . 5
⊢ ((𝐾 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) = ∅) |
| 40 | 38, 39 | syl 17 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) = ∅) |
| 41 | 32, 40 | eqtr4d 2780 |
. . 3
⊢ (¬
𝑀 ∈ V → (
·𝑠 ‘(MEndo‘𝑀)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦))) |
| 42 | 27, 41 | pm2.61i 182 |
. 2
⊢ (
·𝑠 ‘(MEndo‘𝑀)) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) |
| 43 | 2, 42 | eqtri 2765 |
1
⊢ (
·𝑠 ‘𝐴) = (𝑥 ∈ 𝐾, 𝑦 ∈ 𝐵 ↦ ((𝐸 × {𝑥}) ∘f · 𝑦)) |