Theorem 0lno 8450

Description: The zero operator is linear.

Hypotheses

Ref	Expression
0lno.0	|- Z = (U 0op W)
0lno.7	|- L = (U LnOp W)

Assertion

Ref	Expression
0lno	|- ((U e. NrmCVec /\ W e. NrmCVec) -> Z e. L)

Proof of Theorem 0lno

Step	Hyp	Ref	Expression
1		eqid 1475	. . . 4 |- (Base` U) = (Base` U)
2		eqid 1475	. . . 4 |- (Base` W) = (Base` W)
3		0lno.0	. . . 4 |- Z = (U 0op W)
4	1, 2, 3	0oo 8449	. . 3 |- ((U e. NrmCVec /\ W e. NrmCVec) -> Z:(Base` U)-->(Base` W))
5		eqid 1475	. . . . . . . . . . 11 |- (0v` W) = (0v` W)
6	2, 5	nvzcl 8255	. . . . . . . . . 10 |- (W e. NrmCVec -> (0v` W) e. (Base` W))
7		eqid 1475	. . . . . . . . . . 11 |- (+v` W) = (+v` W)
8	2, 7, 5	nv0rid 8256	. . . . . . . . . 10 |- ((W e. NrmCVec /\ (0v` W) e. (Base` W)) -> ((0v` W)(+v` W)(0v` W)) = (0v` W))
9	6, 8	mpdan 704	. . . . . . . . 9 |- (W e. NrmCVec -> ((0v` W)(+v` W)(0v` W)) = (0v` W))
10	9	adantl 388	. . . . . . . 8 |- ((U e. NrmCVec /\ W e. NrmCVec) -> ((0v` W)(+v` W)(0v` W)) = (0v` W))
11	10	ad2antrr 404	. . . . . . 7 |- ((((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> ((0v` W)(+v` W)(0v` W)) = (0v` W))
12	1, 5, 3	0oval 8448	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. NrmCVec /\ x e. (Base` U)) -> (Z` x) = (0v` W))
13	12	3expa 833	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) -> (Z` x) = (0v` W))
14	13	adantr 389	. . . . . . . 8 |- ((((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> (Z` x) = (0v` W))
15	1, 5, 3	0oval 8448	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ W e. NrmCVec /\ z e. (Base` U)) -> (Z` z) = (0v` W))
16	15	3expa 833	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ z e. (Base` U)) -> (Z` z) = (0v` W))
17	16	adantrl 394	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (y e. CC /\ z e. (Base` U))) -> (Z` z) = (0v` W))
18	17	opreq2d 3976	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` W)(Z` z)) = (y(.s` W)(0v` W)))
19		eqid 1475	. . . . . . . . . . . 12 |- (.s` W) = (.s` W)
20	19, 5	nvsz 8259	. . . . . . . . . . 11 |- ((W e. NrmCVec /\ y e. CC) -> (y(.s` W)(0v` W)) = (0v` W))
21	20	ad2ant2lr 410	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` W)(0v` W)) = (0v` W))
22	18, 21	eqtrd 1507	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` W)(Z` z)) = (0v` W))
23	22	adantlr 393	. . . . . . . 8 |- ((((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` W)(Z` z)) = (0v` W))
24	14, 23	opreq12d 3978	. . . . . . 7 |- ((((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> ((Z` x)(+v` W)(y(.s` W)(Z` z))) = ((0v` W)(+v` W)(0v` W)))
25		eqid 1475	. . . . . . . . . . . . . . 15 |- (.s` U) = (.s` U)
26	1, 25	nvscl 8247	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ y e. CC /\ z e. (Base` U)) -> (y(.s` U)z) e. (Base` U))
27	26	3expb 834	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` U)z) e. (Base` U))
28	27	adantlr 393	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` U)z) e. (Base` U))
29		eqid 1475	. . . . . . . . . . . . . 14 |- (+v` U) = (+v` U)
30	1, 29	nvgcl 8239	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ x e. (Base` U) /\ (y(.s` U)z) e. (Base` U)) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
31	30	3expa 833	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ x e. (Base` U)) /\ (y(.s` U)z) e. (Base` U)) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
32	28, 31	syldan 467	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
33	32	anasss 440	. . . . . . . . . 10 |- ((U e. NrmCVec /\ (x e. (Base` U) /\ (y e. CC /\ z e. (Base` U)))) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
34	33	adantlr 393	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (x e. (Base` U) /\ (y e. CC /\ z e. (Base` U)))) -> (x(+v` U)(y(.s` U)z)) e. (Base` U))
35	1, 5, 3	0oval 8448	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. NrmCVec /\ (x(+v` U)(y(.s` U)z)) e. (Base` U)) -> (Z` (x(+v` U)(y(.s` U)z))) = (0v` W))
36	35	3expa 833	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (x(+v` U)(y(.s` U)z)) e. (Base` U)) -> (Z` (x(+v` U)(y(.s` U)z))) = (0v` W))
37	34, 36	syldan 467	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (x e. (Base` U) /\ (y e. CC /\ z e. (Base` U)))) -> (Z` (x(+v` U)(y(.s` U)z))) = (0v` W))
38	37	anassrs 441	. . . . . . 7 |- ((((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> (Z` (x(+v` U)(y(.s` U)z))) = (0v` W))
39	11, 24, 38	3eqtr4rd 1518	. . . . . 6 |- ((((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> (Z` (x(+v` U)(y(.s` U)z))) = ((Z` x)(+v` W)(y(.s` W)(Z` z))))
40	39	ex 373	. . . . 5 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) -> ((y e. CC /\ z e. (Base` U)) -> (Z` (x(+v` U)(y(.s` U)z))) = ((Z` x)(+v` W)(y(.s` W)(Z` z)))))
41	40	r19.21aivv 1720	. . . 4 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) -> A.y e. CC A.z e. (Base` U)(Z` (x(+v` U)(y(.s` U)z))) = ((Z` x)(+v` W)(y(.s` W)(Z` z))))
42	41	r19.21aiva 1714	. . 3 |- ((U e. NrmCVec /\ W e. NrmCVec) -> A.x e. (Base` U)A.y e. CC A.z e. (Base` U)(Z` (x(+v` U)(y(.s` U)z))) = ((Z` x)(+v` W)(y(.s` W)(Z` z))))
43	4, 42	jca 288	. 2 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (Z:(Base` U)-->(Base` W) /\ A.x e. (Base` U)A.y e. CC A.z e. (Base` U)(Z` (x(+v` U)(y(.s` U)z))) = ((Z` x)(+v` W)(y(.s` W)(Z` z)))))
44		0lno.7	. . 3 |- L = (U LnOp W)
45	1, 2, 29, 7, 25, 19, 44	islno 8414	. 2 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (Z e. L <-> (Z:(Base` U)-->(Base` W) /\ A.x e. (Base` U)A.y e. CC A.z e. (Base` U)(Z` (x(+v` U)(y(.s` U)z))) = ((Z` x)(+v` W)(y(.s` W)(Z` z))))))
46	43, 45	mpbird 196	1 |- ((U e. NrmCVec /\ W e. NrmCVec) -> Z e. L)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956   e. wcel 958  A.wral 1645  -->wf 3178  ` cfv 3182  (class class class)co 3963  CCcc 5232  NrmCVeccnv 8203  +vcpv 8204  Basecba 8205  .scns 8206  0vcn0v 8207   LnOp clno 8401   0op c0o 8404

This theorem is referenced by:  0blo 8452  nmlno0i 8454  blocn 8467

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693