Metamath Proof Explorer

Theorem 0lno

Description: The zero operator is linear. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses 0lno.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
0lno.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion 0lno ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 ∈ 𝐿 )

Proof

Step Hyp Ref Expression
1 0lno.0 ⊢ 𝑍 = ( 𝑈 0op 𝑊 )
2 0lno.7 ⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
3 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
4 eqid ⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
5 3 4 1 0oo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) )
6 simplll ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑈 ∈ NrmCVec )
7 simpllr ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑊 ∈ NrmCVec )
8 simplr ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑥 ∈ ℂ )
9 simprl ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑦 ∈ ( BaseSet ‘ 𝑈 ) )
10 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
11 3 10 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) )
12 6 8 9 11 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) )
13 simprr ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → 𝑧 ∈ ( BaseSet ‘ 𝑈 ) )
14 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
15 3 14 nvgcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) )
16 6 12 13 15 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) )
17 eqid ⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
18 3 17 1 0oval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑍 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( 0vec ‘ 𝑊 ) )
19 6 7 16 18 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑍 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( 0vec ‘ 𝑊 ) )
20 3 17 1 0oval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑍 ‘ 𝑦 ) = ( 0vec ‘ 𝑊 ) )
21 6 7 9 20 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑍 ‘ 𝑦 ) = ( 0vec ‘ 𝑊 ) )
22 21 oveq2d ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑍 ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
23 3 17 1 0oval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) → ( 𝑍 ‘ 𝑧 ) = ( 0vec ‘ 𝑊 ) )
24 6 7 13 23 syl3anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑍 ‘ 𝑧 ) = ( 0vec ‘ 𝑊 ) )
25 22 24 oveq12d ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑍 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑍 ‘ 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
26 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
27 26 17 nvsz ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) = ( 0vec ‘ 𝑊 ) )
28 7 8 27 syl2anc ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) = ( 0vec ‘ 𝑊 ) )
29 28 oveq1d ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) = ( ( 0vec ‘ 𝑊 ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) )
30 4 17 nvzcl ⊢ ( 𝑊 ∈ NrmCVec → ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) )
31 eqid ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
32 4 31 17 nv0rid ⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) ) → ( ( 0vec ‘ 𝑊 ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) = ( 0vec ‘ 𝑊 ) )
33 7 30 32 syl2anc2 ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 0vec ‘ 𝑊 ) ( +𝑣 ‘ 𝑊 ) ( 0vec ‘ 𝑊 ) ) = ( 0vec ‘ 𝑊 ) )
34 25 29 33 3eqtrd ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑍 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑍 ‘ 𝑧 ) ) = ( 0vec ‘ 𝑊 ) )
35 19 34 eqtr4d ⊢ ( ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∧ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ) ) → ( 𝑍 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑍 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑍 ‘ 𝑧 ) ) )
36 35 ralrimivva ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑥 ∈ ℂ ) → ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( 𝑍 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑍 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑍 ‘ 𝑧 ) ) )
37 36 ralrimiva ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( 𝑍 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑍 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑍 ‘ 𝑧 ) ) )
38 3 4 14 31 10 26 2 islno ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑍 ∈ 𝐿 ↔ ( 𝑍 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑧 ∈ ( BaseSet ‘ 𝑈 ) ( 𝑍 ‘ ( ( 𝑥 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ( +𝑣 ‘ 𝑈 ) 𝑧 ) ) = ( ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) ( 𝑍 ‘ 𝑦 ) ) ( +𝑣 ‘ 𝑊 ) ( 𝑍 ‘ 𝑧 ) ) ) ) )
39 5 37 38 mpbir2and ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑍 ∈ 𝐿 )