Proof of Theorem mendmulrfval
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mendmulrfval.a | . . . . 5
⊢ 𝐴 = (MEndo‘𝑀) | 
| 2 |  | mendmulrfval.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝐴) | 
| 3 | 1 | mendbas 43192 | . . . . . . 7
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) | 
| 4 | 2, 3 | eqtr4i 2768 | . . . . . 6
⊢ 𝐵 = (𝑀 LMHom 𝑀) | 
| 5 |  | eqid 2737 | . . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦)) | 
| 6 |  | eqid 2737 | . . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) | 
| 7 |  | eqid 2737 | . . . . . 6
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) | 
| 8 |  | eqid 2737 | . . . . . 6
⊢ (𝑥 ∈
(Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) = (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) | 
| 9 | 4, 5, 6, 7, 8 | mendval 43191 | . . . . 5
⊢ (𝑀 ∈ V →
(MEndo‘𝑀) =
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉})) | 
| 10 | 1, 9 | eqtrid 2789 | . . . 4
⊢ (𝑀 ∈ V → 𝐴 = ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉})) | 
| 11 | 10 | fveq2d 6910 | . . 3
⊢ (𝑀 ∈ V →
(.r‘𝐴) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘f
(+g‘𝑀)𝑦))〉, 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑀)〉,
〈( ·𝑠 ‘ndx), (𝑥 ∈ (Base‘(Scalar‘𝑀)), 𝑦 ∈ 𝐵 ↦ (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦))〉}))) | 
| 12 | 2 | fvexi 6920 | . . . . 5
⊢ 𝐵 ∈ V | 
| 13 | 12, 12 | mpoex 8104 | . . . 4
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) ∈ V | 
| 14 |  | eqid 2737 | . . . . 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 43188 | . . . 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 2780 | . 2
⊢ (𝑀 ∈ V →
(.r‘𝐴) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))) | 
| 18 |  | fvprc 6898 | . . . . . 6
⊢ (¬
𝑀 ∈ V →
(MEndo‘𝑀) =
∅) | 
| 19 | 1, 18 | eqtrid 2789 | . . . . 5
⊢ (¬
𝑀 ∈ V → 𝐴 = ∅) | 
| 20 | 19 | fveq2d 6910 | . . . 4
⊢ (¬
𝑀 ∈ V →
(.r‘𝐴) =
(.r‘∅)) | 
| 21 |  | mulridx 17338 | . . . . 5
⊢
.r = Slot (.r‘ndx) | 
| 22 | 21 | str0 17226 | . . . 4
⊢ ∅ =
(.r‘∅) | 
| 23 | 20, 22 | eqtr4di 2795 | . . 3
⊢ (¬
𝑀 ∈ V →
(.r‘𝐴) =
∅) | 
| 24 | 19 | fveq2d 6910 | . . . . . . 7
⊢ (¬
𝑀 ∈ V →
(Base‘𝐴) =
(Base‘∅)) | 
| 25 | 2, 24 | eqtrid 2789 | . . . . . 6
⊢ (¬
𝑀 ∈ V → 𝐵 =
(Base‘∅)) | 
| 26 |  | base0 17252 | . . . . . 6
⊢ ∅ =
(Base‘∅) | 
| 27 | 25, 26 | eqtr4di 2795 | . . . . 5
⊢ (¬
𝑀 ∈ V → 𝐵 = ∅) | 
| 28 | 27 | olcd 875 | . . . 4
⊢ (¬
𝑀 ∈ V → (𝐵 = ∅ ∨ 𝐵 = ∅)) | 
| 29 |  | 0mpo0 7516 | . . . 4
⊢ ((𝐵 = ∅ ∨ 𝐵 = ∅) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = ∅) | 
| 30 | 28, 29 | syl 17 | . . 3
⊢ (¬
𝑀 ∈ V → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) = ∅) | 
| 31 | 23, 30 | eqtr4d 2780 | . 2
⊢ (¬
𝑀 ∈ V →
(.r‘𝐴) =
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦))) | 
| 32 | 17, 31 | pm2.61i 182 | 1
⊢
(.r‘𝐴) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 ∘ 𝑦)) |