Theorem 0lno 8534

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 1522	. . . 4 |- (Base` U) = (Base` U)
2		eqid 1522	. . . 4 |- (Base` W) = (Base` W)
3		0lno.0	. . . 4 |- Z = (U 0op W)
4	1, 2, 3	0oo 8533	. . 3 |- ((U e. NrmCVec /\ W e. NrmCVec) -> Z:(Base` U)-->(Base` W))
5		eqid 1522	. . . . . . . . . . 11 |- (0v` W) = (0v` W)
6	2, 5	nvzcl 8339	. . . . . . . . . 10 |- (W e. NrmCVec -> (0v` W) e. (Base` W))
7		eqid 1522	. . . . . . . . . . 11 |- (+v` W) = (+v` W)
8	2, 7, 5	nv0rid 8340	. . . . . . . . . 10 |- ((W e. NrmCVec /\ (0v` W) e. (Base` W)) -> ((0v` W)(+v` W)(0v` W)) = (0v` W))
9	6, 8	mpdan 716	. . . . . . . . 9 |- (W e. NrmCVec -> ((0v` W)(+v` W)(0v` W)) = (0v` W))
10	9	adantl 397	. . . . . . . 8 |- ((U e. NrmCVec /\ W e. NrmCVec) -> ((0v` W)(+v` W)(0v` W)) = (0v` W))
11	10	ad2antrr 413	. . . . . . 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 8532	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. NrmCVec /\ x e. (Base` U)) -> (Z` x) = (0v` W))
13	12	3expa 845	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ x e. (Base` U)) -> (Z` x) = (0v` W))
14	13	adantr 398	. . . . . . . 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 8532	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ W e. NrmCVec /\ z e. (Base` U)) -> (Z` z) = (0v` W))
16	15	3expa 845	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ z e. (Base` U)) -> (Z` z) = (0v` W))
17	16	adantrl 403	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (y e. CC /\ z e. (Base` U))) -> (Z` z) = (0v` W))
18	17	opreq2d 4034	. . . . . . . . . 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 1522	. . . . . . . . . . . 12 |- (.s` W) = (.s` W)
20	19, 5	nvsz 8343	. . . . . . . . . . 11 |- ((W e. NrmCVec /\ y e. CC) -> (y(.s` W)(0v` W)) = (0v` W))
21	20	ad2ant2lr 419	. . . . . . . . . 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 1554	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. NrmCVec) /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` W)(Z` z)) = (0v` W))
23	22	adantlr 402	. . . . . . . 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 4036	. . . . . . 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 1522	. . . . . . . . . . . . . . 15 |- (.s` U) = (.s` U)
26	1, 25	nvscl 8331	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ y e. CC /\ z e. (Base` U)) -> (y(.s` U)z) e. (Base` U))
27	26	3expb 846	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` U)z) e. (Base` U))
28	27	adantlr 402	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ x e. (Base` U)) /\ (y e. CC /\ z e. (Base` U))) -> (y(.s` U)z) e. (Base` U))
29		eqid 1522	. . . . . . . . . . . . . 14 |- (+v` U) = (+v` U)
30	1, 29	nvgcl 8323	. . . . . . . . . . . . 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 845	. . . . . . . . . . . 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 478	. . . . . . . . . . 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 451	. . . . . . . . . 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 402	. . . . . . . . 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 8532	. . . . . . . . . 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 845	. . . . . . . . 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 478	. . . . . . . 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 452	. . . . . . 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 1565	. . . . . 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 380	. . . . 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 1767	. . . 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 1761	. . 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 295	. 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 8498	. 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 203	1 |- ((U e. NrmCVec /\ W e. NrmCVec) -> Z e. L)

Syntax hints:   -> wi 3   /\ wa 230   = wceq 997   e. wcel 999  A.wral 1692  -->wf 3235  ` cfv 3239  (class class class)co 4021  CCcc 5297  NrmCVeccnv 8287  +vcpv 8288  Basecba 8289  .scns 8290  0vcn0v 8291   LnOp clno 8485   0op c0o 8488

This theorem is referenced by:  0blo 8536  nmlno0i 8538  blocn 8551

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep