Proof of Theorem mendmulrfval
Step | Hyp | Ref
| Expression |
1 | | mendmulrfval.a |
. . . . 5
⊢ 𝐴 = (MEndo‘𝑀) |
2 | | mendmulrfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
3 | 1 | mendbas 40603 |
. . . . . . 7
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
4 | 2, 3 | eqtr4i 2764 |
. . . . . 6
⊢ 𝐵 = (𝑀 LMHom 𝑀) |
5 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦)) |
6 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) |
7 | | eqid 2738 |
. . . . . 6
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
8 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈
(Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) = (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
9 | 4, 5, 6, 7, 8 | mendval 40602 |
. . . . 5
⊢ (𝑀 ∈ V →
(MEndo‘𝑀) =
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉})) |
10 | 1, 9 | syl5eq 2785 |
. . . 4
⊢ (𝑀 ∈ V → 𝐴 = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉})) |
11 | 10 | fveq2d 6680 |
. . 3
⊢ (𝑀 ∈ V →
(.r‘𝐴) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}))) |
12 | 2 | fvexi 6690 |
. . . . 5
⊢ 𝐵 ∈ V |
13 | 12, 12 | mpoex 7805 |
. . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) ∈ V |
14 | | eqid 2738 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}) |
15 | 14 | algmulr 40599 |
. . . 4
⊢ ((𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}))) |
16 | 13, 15 | mp1i 13 |
. . 3
⊢ (𝑀 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}))) |
17 | 11, 16 | eqtr4d 2776 |
. 2
⊢ (𝑀 ∈ V →
(.r‘𝐴) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))) |
18 | | fvprc 6668 |
. . . . . 6
⊢ (¬
𝑀 ∈ V →
(MEndo‘𝑀) =
∅) |
19 | 1, 18 | syl5eq 2785 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝐴 = ∅) |
20 | 19 | fveq2d 6680 |
. . . 4
⊢ (¬
𝑀 ∈ V →
(.r‘𝐴) =
(.r‘∅)) |
21 | | df-mulr 16684 |
. . . . 5
⊢
.r = Slot 3 |
22 | 21 | str0 16640 |
. . . 4
⊢ ∅ =
(.r‘∅) |
23 | 20, 22 | eqtr4di 2791 |
. . 3
⊢ (¬
𝑀 ∈ V →
(.r‘𝐴) =
∅) |
24 | 19 | fveq2d 6680 |
. . . . . . 7
⊢ (¬
𝑀 ∈ V →
(Base‘𝐴) =
(Base‘∅)) |
25 | 2, 24 | syl5eq 2785 |
. . . . . 6
⊢ (¬
𝑀 ∈ V → 𝐵 =
(Base‘∅)) |
26 | | base0 16641 |
. . . . . 6
⊢ ∅ =
(Base‘∅) |
27 | 25, 26 | eqtr4di 2791 |
. . . . 5
⊢ (¬
𝑀 ∈ V → 𝐵 = ∅) |
28 | 27 | olcd 873 |
. . . 4
⊢ (¬
𝑀 ∈ V → (𝐵 = ∅ ∨ 𝐵 = ∅)) |
29 | | 0mpo0 7253 |
. . . 4
⊢ ((𝐵 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = ∅) |
30 | 28, 29 | syl 17 |
. . 3
⊢ (¬
𝑀 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = ∅) |
31 | 23, 30 | eqtr4d 2776 |
. 2
⊢ (¬
𝑀 ∈ V →
(.r‘𝐴) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))) |
32 | 17, 31 | pm2.61i 185 |
1
⊢
(.r‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) |