| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
| 2 | | eqid 2737 |
. . 3
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
| 3 | | 0lno.0 |
. . 3
⊢ 𝑍 = (𝑈 0op 𝑊) |
| 4 | 1, 2, 3 | 0oo 30808 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:(BaseSet‘𝑈)⟶(BaseSet‘𝑊)) |
| 5 | | simplll 775 |
. . . . . 6
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → 𝑈 ∈ NrmCVec) |
| 6 | | simpllr 776 |
. . . . . 6
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → 𝑊 ∈ NrmCVec) |
| 7 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → 𝑥 ∈ ℂ) |
| 8 | | simprl 771 |
. . . . . . . 8
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → 𝑦 ∈ (BaseSet‘𝑈)) |
| 9 | | eqid 2737 |
. . . . . . . . 9
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
| 10 | 1, 9 | nvscl 30645 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ (BaseSet‘𝑈)) → (𝑥( ·𝑠OLD
‘𝑈)𝑦) ∈ (BaseSet‘𝑈)) |
| 11 | 5, 7, 8, 10 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → (𝑥( ·𝑠OLD
‘𝑈)𝑦) ∈ (BaseSet‘𝑈)) |
| 12 | | simprr 773 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → 𝑧 ∈ (BaseSet‘𝑈)) |
| 13 | | eqid 2737 |
. . . . . . . 8
⊢ (
+𝑣 ‘𝑈) = ( +𝑣 ‘𝑈) |
| 14 | 1, 13 | nvgcl 30639 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥(
·𝑠OLD ‘𝑈)𝑦) ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈)) → ((𝑥( ·𝑠OLD
‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧) ∈ (BaseSet‘𝑈)) |
| 15 | 5, 11, 12, 14 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → ((𝑥( ·𝑠OLD
‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧) ∈ (BaseSet‘𝑈)) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
| 17 | 1, 16, 3 | 0oval 30807 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ ((𝑥(
·𝑠OLD ‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧) ∈ (BaseSet‘𝑈)) → (𝑍‘((𝑥( ·𝑠OLD
‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧)) = (0vec‘𝑊)) |
| 18 | 5, 6, 15, 17 | syl3anc 1373 |
. . . . 5
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → (𝑍‘((𝑥( ·𝑠OLD
‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧)) = (0vec‘𝑊)) |
| 19 | 1, 16, 3 | 0oval 30807 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑈)) → (𝑍‘𝑦) = (0vec‘𝑊)) |
| 20 | 5, 6, 8, 19 | syl3anc 1373 |
. . . . . . . 8
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → (𝑍‘𝑦) = (0vec‘𝑊)) |
| 21 | 20 | oveq2d 7447 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → (𝑥( ·𝑠OLD
‘𝑊)(𝑍‘𝑦)) = (𝑥( ·𝑠OLD
‘𝑊)(0vec‘𝑊))) |
| 22 | 1, 16, 3 | 0oval 30807 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑧 ∈ (BaseSet‘𝑈)) → (𝑍‘𝑧) = (0vec‘𝑊)) |
| 23 | 5, 6, 12, 22 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → (𝑍‘𝑧) = (0vec‘𝑊)) |
| 24 | 21, 23 | oveq12d 7449 |
. . . . . 6
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → ((𝑥( ·𝑠OLD
‘𝑊)(𝑍‘𝑦))( +𝑣 ‘𝑊)(𝑍‘𝑧)) = ((𝑥( ·𝑠OLD
‘𝑊)(0vec‘𝑊))( +𝑣 ‘𝑊)(0vec‘𝑊))) |
| 25 | | eqid 2737 |
. . . . . . . . 9
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
| 26 | 25, 16 | nvsz 30657 |
. . . . . . . 8
⊢ ((𝑊 ∈ NrmCVec ∧ 𝑥 ∈ ℂ) → (𝑥(
·𝑠OLD ‘𝑊)(0vec‘𝑊)) = (0vec‘𝑊)) |
| 27 | 6, 7, 26 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → (𝑥( ·𝑠OLD
‘𝑊)(0vec‘𝑊)) = (0vec‘𝑊)) |
| 28 | 27 | oveq1d 7446 |
. . . . . 6
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → ((𝑥( ·𝑠OLD
‘𝑊)(0vec‘𝑊))( +𝑣 ‘𝑊)(0vec‘𝑊)) =
((0vec‘𝑊)(
+𝑣 ‘𝑊)(0vec‘𝑊))) |
| 29 | 2, 16 | nvzcl 30653 |
. . . . . . 7
⊢ (𝑊 ∈ NrmCVec →
(0vec‘𝑊)
∈ (BaseSet‘𝑊)) |
| 30 | | eqid 2737 |
. . . . . . . 8
⊢ (
+𝑣 ‘𝑊) = ( +𝑣 ‘𝑊) |
| 31 | 2, 30, 16 | nv0rid 30654 |
. . . . . . 7
⊢ ((𝑊 ∈ NrmCVec ∧
(0vec‘𝑊)
∈ (BaseSet‘𝑊))
→ ((0vec‘𝑊)( +𝑣 ‘𝑊)(0vec‘𝑊)) =
(0vec‘𝑊)) |
| 32 | 6, 29, 31 | syl2anc2 585 |
. . . . . 6
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → ((0vec‘𝑊)( +𝑣
‘𝑊)(0vec‘𝑊)) = (0vec‘𝑊)) |
| 33 | 24, 28, 32 | 3eqtrd 2781 |
. . . . 5
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → ((𝑥( ·𝑠OLD
‘𝑊)(𝑍‘𝑦))( +𝑣 ‘𝑊)(𝑍‘𝑧)) = (0vec‘𝑊)) |
| 34 | 18, 33 | eqtr4d 2780 |
. . . 4
⊢ ((((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) ∧ (𝑦 ∈ (BaseSet‘𝑈) ∧ 𝑧 ∈ (BaseSet‘𝑈))) → (𝑍‘((𝑥( ·𝑠OLD
‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑊)(𝑍‘𝑦))( +𝑣 ‘𝑊)(𝑍‘𝑧))) |
| 35 | 34 | ralrimivva 3202 |
. . 3
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) ∧ 𝑥 ∈ ℂ) →
∀𝑦 ∈
(BaseSet‘𝑈)∀𝑧 ∈ (BaseSet‘𝑈)(𝑍‘((𝑥( ·𝑠OLD
‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑊)(𝑍‘𝑦))( +𝑣 ‘𝑊)(𝑍‘𝑧))) |
| 36 | 35 | ralrimiva 3146 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) →
∀𝑥 ∈ ℂ
∀𝑦 ∈
(BaseSet‘𝑈)∀𝑧 ∈ (BaseSet‘𝑈)(𝑍‘((𝑥( ·𝑠OLD
‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑊)(𝑍‘𝑦))( +𝑣 ‘𝑊)(𝑍‘𝑧))) |
| 37 | | 0lno.7 |
. . 3
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
| 38 | 1, 2, 13, 30, 9, 25, 37 | islno 30772 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑍 ∈ 𝐿 ↔ (𝑍:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑈)∀𝑧 ∈ (BaseSet‘𝑈)(𝑍‘((𝑥( ·𝑠OLD
‘𝑈)𝑦)( +𝑣 ‘𝑈)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑊)(𝑍‘𝑦))( +𝑣 ‘𝑊)(𝑍‘𝑧))))) |
| 39 | 4, 36, 38 | mpbir2and 713 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐿) |