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