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	$⊢ Z = U 0_{op} W$
	0lno.7	$⊢ L = U LnOp W$
Assertion	0lno	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z \in L$

Proof

Step	Hyp	Ref	Expression
1		0lno.0	$⊢ Z = U 0_{op} W$
2		0lno.7	$⊢ L = U LnOp W$
3		eqid	$⊢ BaseSet (U) = BaseSet (U)$
4		eqid	$⊢ BaseSet (W) = BaseSet (W)$
5	3 4 1	0oo	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z : BaseSet (U) ⟶ BaseSet (W)$
6		simplll	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to U \in NrmCVec$
7		simpllr	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to W \in NrmCVec$
8		simplr	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to x \in ℂ$
9		simprl	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to y \in BaseSet (U)$
10		eqid	$⊢ \cdot_{𝑠OLD} (U) = \cdot_{𝑠OLD} (U)$
11	3 10	nvscl	$⊢ (U \in NrmCVec \land x \in ℂ \land y \in BaseSet (U)) \to x \cdot_{𝑠OLD} (U) y \in BaseSet (U)$
12	6 8 9 11	syl3anc	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to x \cdot_{𝑠OLD} (U) y \in BaseSet (U)$
13		simprr	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to z \in BaseSet (U)$
14		eqid	$⊢ +_{v} (U) = +_{v} (U)$
15	3 14	nvgcl	$⊢ (U \in NrmCVec \land x \cdot_{𝑠OLD} (U) y \in BaseSet (U) \land z \in BaseSet (U)) \to (x \cdot_{𝑠OLD} (U) y) +_{v} (U) z \in BaseSet (U)$
16	6 12 13 15	syl3anc	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to (x \cdot_{𝑠OLD} (U) y) +_{v} (U) z \in BaseSet (U)$
17		eqid	$⊢ 0_{vec} (W) = 0_{vec} (W)$
18	3 17 1	0oval	$⊢ (U \in NrmCVec \land W \in NrmCVec \land (x \cdot_{𝑠OLD} (U) y) +_{v} (U) z \in BaseSet (U)) \to Z ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = 0_{vec} (W)$
19	6 7 16 18	syl3anc	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to Z ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = 0_{vec} (W)$
20	3 17 1	0oval	$⊢ (U \in NrmCVec \land W \in NrmCVec \land y \in BaseSet (U)) \to Z (y) = 0_{vec} (W)$
21	6 7 9 20	syl3anc	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to Z (y) = 0_{vec} (W)$
22	21	oveq2d	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to x \cdot_{𝑠OLD} (W) Z (y) = x \cdot_{𝑠OLD} (W) 0_{vec} (W)$
23	3 17 1	0oval	$⊢ (U \in NrmCVec \land W \in NrmCVec \land z \in BaseSet (U)) \to Z (z) = 0_{vec} (W)$
24	6 7 13 23	syl3anc	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to Z (z) = 0_{vec} (W)$
25	22 24	oveq12d	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to (x \cdot_{𝑠OLD} (W) Z (y)) +_{v} (W) Z (z) = (x \cdot_{𝑠OLD} (W) 0_{vec} (W)) +_{v} (W) 0_{vec} (W)$
26		eqid	$⊢ \cdot_{𝑠OLD} (W) = \cdot_{𝑠OLD} (W)$
27	26 17	nvsz	$⊢ (W \in NrmCVec \land x \in ℂ) \to x \cdot_{𝑠OLD} (W) 0_{vec} (W) = 0_{vec} (W)$
28	7 8 27	syl2anc	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to x \cdot_{𝑠OLD} (W) 0_{vec} (W) = 0_{vec} (W)$
29	28	oveq1d	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to (x \cdot_{𝑠OLD} (W) 0_{vec} (W)) +_{v} (W) 0_{vec} (W) = 0_{vec} (W) +_{v} (W) 0_{vec} (W)$
30	4 17	nvzcl	$⊢ W \in NrmCVec \to 0_{vec} (W) \in BaseSet (W)$
31		eqid	$⊢ +_{v} (W) = +_{v} (W)$
32	4 31 17	nv0rid	$⊢ (W \in NrmCVec \land 0_{vec} (W) \in BaseSet (W)) \to 0_{vec} (W) +_{v} (W) 0_{vec} (W) = 0_{vec} (W)$
33	7 30 32	syl2anc2	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to 0_{vec} (W) +_{v} (W) 0_{vec} (W) = 0_{vec} (W)$
34	25 29 33	3eqtrd	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to (x \cdot_{𝑠OLD} (W) Z (y)) +_{v} (W) Z (z) = 0_{vec} (W)$
35	19 34	eqtr4d	$⊢ (((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \land (y \in BaseSet (U) \land z \in BaseSet (U))) \to Z ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (W) Z (y)) +_{v} (W) Z (z)$
36	35	ralrimivva	$⊢ ((U \in NrmCVec \land W \in NrmCVec) \land x \in ℂ) \to \forall y \in BaseSet (U) \forall z \in BaseSet (U) Z ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (W) Z (y)) +_{v} (W) Z (z)$
37	36	ralrimiva	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to \forall x \in ℂ \forall y \in BaseSet (U) \forall z \in BaseSet (U) Z ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (W) Z (y)) +_{v} (W) Z (z)$
38	3 4 14 31 10 26 2	islno	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to (Z \in L \leftrightarrow (Z : BaseSet (U) ⟶ BaseSet (W) \land \forall x \in ℂ \forall y \in BaseSet (U) \forall z \in BaseSet (U) Z ((x \cdot_{𝑠OLD} (U) y) +_{v} (U) z) = (x \cdot_{𝑠OLD} (W) Z (y)) +_{v} (W) Z (z)))$
39	5 37 38	mpbir2and	$⊢ (U \in NrmCVec \land W \in NrmCVec) \to Z \in L$

Metamath Proof Explorer

Theorem 0lno

Proof