Proof of Theorem mendplusgfval
Step | Hyp | Ref
| Expression |
1 | | mendplusgfval.a |
. . . . 5
⊢ 𝐴 = (MEndo‘𝑀) |
2 | | mendplusgfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
3 | 1 | mendbas 40565 |
. . . . . . 7
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
4 | 2, 3 | eqtr4i 2764 |
. . . . . 6
⊢ 𝐵 = (𝑀 LMHom 𝑀) |
5 | | mendplusgfval.p |
. . . . . . . . . 10
⊢ + =
(+g‘𝑀) |
6 | | ofeq 7421 |
. . . . . . . . . 10
⊢ ( + =
(+g‘𝑀)
→ ∘f + = ∘f
(+g‘𝑀)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . 9
⊢
∘f + = ∘f
(+g‘𝑀) |
8 | 7 | oveqi 7177 |
. . . . . . . 8
⊢ (𝑥 ∘f + 𝑦) = (𝑥 ∘f
(+g‘𝑀)𝑦) |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∘f + 𝑦) = (𝑥 ∘f
(+g‘𝑀)𝑦)) |
10 | 9 | mpoeq3ia 7240 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦)) |
11 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) |
12 | | eqid 2738 |
. . . . . 6
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
13 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈
(Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) = (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
14 | 4, 10, 11, 12, 13 | mendval 40564 |
. . . . 5
⊢ (𝑀 ∈ V →
(MEndo‘𝑀) =
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉})) |
15 | 1, 14 | syl5eq 2785 |
. . . 4
⊢ (𝑀 ∈ V → 𝐴 = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉})) |
16 | 15 | fveq2d 6672 |
. . 3
⊢ (𝑀 ∈ V →
(+g‘𝐴) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}))) |
17 | 2 | fvexi 6682 |
. . . . 5
⊢ 𝐵 ∈ V |
18 | 17, 17 | mpoex 7796 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) ∈ V |
19 | | eqid 2738 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}) |
20 | 19 | algaddg 40560 |
. . . 4
⊢ ((𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}))) |
21 | 18, 20 | mp1i 13 |
. . 3
⊢ (𝑀 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}))) |
22 | 16, 21 | eqtr4d 2776 |
. 2
⊢ (𝑀 ∈ V →
(+g‘𝐴) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))) |
23 | | fvprc 6660 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(MEndo‘𝑀) =
∅) |
24 | 1, 23 | syl5eq 2785 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝐴 = ∅) |
25 | 24 | fveq2d 6672 |
. . . 4
⊢ (¬
𝑀 ∈ V →
(+g‘𝐴) =
(+g‘∅)) |
26 | | df-plusg 16674 |
. . . . 5
⊢
+g = Slot 2 |
27 | 26 | str0 16631 |
. . . 4
⊢ ∅ =
(+g‘∅) |
28 | 25, 27 | eqtr4di 2791 |
. . 3
⊢ (¬
𝑀 ∈ V →
(+g‘𝐴) =
∅) |
29 | 24 | fveq2d 6672 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(Base‘𝐴) =
(Base‘∅)) |
30 | | base0 16632 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
31 | 29, 2, 30 | 3eqtr4g 2798 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝐵 = ∅) |
32 | 31 | olcd 873 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝐵 = ∅ ∨ 𝐵 = ∅)) |
33 | | 0mpo0 7245 |
. . . 4
⊢ ((𝐵 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) = ∅) |
34 | 32, 33 | syl 17 |
. . 3
⊢ (¬
𝑀 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) = ∅) |
35 | 28, 34 | eqtr4d 2776 |
. 2
⊢ (¬
𝑀 ∈ V →
(+g‘𝐴) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦))) |
36 | 22, 35 | pm2.61i 185 |
1
⊢
(+g‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f + 𝑦)) |