Proof of Theorem mendplusgfval
Step | Hyp | Ref
| Expression |
1 | | mendplusgfval.a |
. . . . 5
⊢ 𝐴 = (MEndo‘𝑀) |
2 | | mendplusgfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
3 | 1 | mendbas 37754 |
. . . . . . 7
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
4 | 2, 3 | eqtr4i 2647 |
. . . . . 6
⊢ 𝐵 = (𝑀 LMHom 𝑀) |
5 | | mendplusgfval.p |
. . . . . . . . . 10
⊢ + =
(+g‘𝑀) |
6 | | ofeq 6899 |
. . . . . . . . . 10
⊢ ( + =
(+g‘𝑀)
→ ∘𝑓 + =
∘𝑓 (+g‘𝑀)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . 9
⊢
∘𝑓 + =
∘𝑓 (+g‘𝑀) |
8 | 7 | oveqi 6663 |
. . . . . . . 8
⊢ (𝑥 ∘𝑓
+ 𝑦) = (𝑥 ∘𝑓
(+g‘𝑀)𝑦) |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∘𝑓 + 𝑦) = (𝑥 ∘𝑓
(+g‘𝑀)𝑦)) |
10 | 9 | mpt2eq3ia 6720 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓
(+g‘𝑀)𝑦)) |
11 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) |
12 | | eqid 2622 |
. . . . . 6
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
13 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈
(Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) = (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) |
14 | 4, 10, 11, 12, 13 | mendval 37753 |
. . . . 5
⊢ (𝑀 ∈ V →
(MEndo‘𝑀) =
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))〉,
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉})) |
15 | 1, 14 | syl5eq 2668 |
. . . 4
⊢ (𝑀 ∈ V → 𝐴 = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))〉,
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉})) |
16 | 15 | fveq2d 6195 |
. . 3
⊢ (𝑀 ∈ V →
(+g‘𝐴) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))〉,
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}))) |
17 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝐴)
∈ V |
18 | 2, 17 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
19 | 18, 18 | mpt2ex 7247 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) ∈ V |
20 | | eqid 2622 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))〉,
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))〉,
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}) |
21 | 20 | algaddg 37749 |
. . . 4
⊢ ((𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))〉,
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}))) |
22 | 19, 21 | mp1i 13 |
. . 3
⊢ (𝑀 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) =
(+g‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))〉,
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦))〉}))) |
23 | 16, 22 | eqtr4d 2659 |
. 2
⊢ (𝑀 ∈ V →
(+g‘𝐴) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))) |
24 | | fvprc 6185 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(MEndo‘𝑀) =
∅) |
25 | 1, 24 | syl5eq 2668 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝐴 = ∅) |
26 | 25 | fveq2d 6195 |
. . . 4
⊢ (¬
𝑀 ∈ V →
(+g‘𝐴) =
(+g‘∅)) |
27 | | df-plusg 15954 |
. . . . 5
⊢
+g = Slot 2 |
28 | 27 | str0 15911 |
. . . 4
⊢ ∅ =
(+g‘∅) |
29 | 26, 28 | syl6eqr 2674 |
. . 3
⊢ (¬
𝑀 ∈ V →
(+g‘𝐴) =
∅) |
30 | 25 | fveq2d 6195 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(Base‘𝐴) =
(Base‘∅)) |
31 | | base0 15912 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
32 | 30, 2, 31 | 3eqtr4g 2681 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝐵 = ∅) |
33 | | mpt2eq12 6715 |
. . . . . 6
⊢ ((𝐵 = ∅ ∧ 𝐵 = ∅) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 ∘𝑓 + 𝑦))) |
34 | 33 | anidms 677 |
. . . . 5
⊢ (𝐵 = ∅ → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 ∘𝑓 + 𝑦))) |
35 | 32, 34 | syl 17 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) = (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 ∘𝑓 + 𝑦))) |
36 | | mpt20 6725 |
. . . 4
⊢ (𝑥 ∈ ∅, 𝑦 ∈ ∅ ↦ (𝑥 ∘𝑓
+ 𝑦)) = ∅ |
37 | 35, 36 | syl6eq 2672 |
. . 3
⊢ (¬
𝑀 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) = ∅) |
38 | 29, 37 | eqtr4d 2659 |
. 2
⊢ (¬
𝑀 ∈ V →
(+g‘𝐴) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦))) |
39 | 23, 38 | pm2.61i 176 |
1
⊢
(+g‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘𝑓 + 𝑦)) |