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 ) → 𝑍 ∈ 𝐿 )