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 
|- Z = ( U 0op W )
0lno.7 
|- L = ( U LnOp W )
Assertion 0lno 
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z e. L )

Proof

Step Hyp Ref Expression
1 0lno.0 
 |-  Z = ( U 0op 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 e. NrmCVec /\ W e. NrmCVec ) -> Z : ( BaseSet ` U ) --> ( BaseSet ` W ) )
6 simplll 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> U e. NrmCVec )
7 simpllr 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> W e. NrmCVec )
8 simplr 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> x e. CC )
9 simprl 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> y e. ( BaseSet ` U ) )
10 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
11 3 10 nvscl 
 |-  ( ( U e. NrmCVec /\ x e. CC /\ y e. ( BaseSet ` U ) ) -> ( x ( .sOLD ` U ) y ) e. ( BaseSet ` U ) )
12 6 8 9 11 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( x ( .sOLD ` U ) y ) e. ( BaseSet ` U ) )
13 simprr 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> z e. ( BaseSet ` U ) )
14 eqid 
 |-  ( +v ` U ) = ( +v ` U )
15 3 14 nvgcl 
 |-  ( ( U e. NrmCVec /\ ( x ( .sOLD ` U ) y ) e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) -> ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) e. ( BaseSet ` U ) )
16 6 12 13 15 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) e. ( BaseSet ` U ) )
17 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
18 3 17 1 0oval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) e. ( BaseSet ` U ) ) -> ( Z ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( 0vec ` W ) )
19 6 7 16 18 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( Z ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( 0vec ` W ) )
20 3 17 1 0oval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ y e. ( BaseSet ` U ) ) -> ( Z ` y ) = ( 0vec ` W ) )
21 6 7 9 20 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( Z ` y ) = ( 0vec ` W ) )
22 21 oveq2d 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( x ( .sOLD ` W ) ( Z ` y ) ) = ( x ( .sOLD ` W ) ( 0vec ` W ) ) )
23 3 17 1 0oval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ z e. ( BaseSet ` U ) ) -> ( Z ` z ) = ( 0vec ` W ) )
24 6 7 13 23 syl3anc 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( Z ` z ) = ( 0vec ` W ) )
25 22 24 oveq12d 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( ( x ( .sOLD ` W ) ( Z ` y ) ) ( +v ` W ) ( Z ` z ) ) = ( ( x ( .sOLD ` W ) ( 0vec ` W ) ) ( +v ` W ) ( 0vec ` W ) ) )
26 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
27 26 17 nvsz 
 |-  ( ( W e. NrmCVec /\ x e. CC ) -> ( x ( .sOLD ` W ) ( 0vec ` W ) ) = ( 0vec ` W ) )
28 7 8 27 syl2anc 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( x ( .sOLD ` W ) ( 0vec ` W ) ) = ( 0vec ` W ) )
29 28 oveq1d 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( ( x ( .sOLD ` W ) ( 0vec ` W ) ) ( +v ` W ) ( 0vec ` W ) ) = ( ( 0vec ` W ) ( +v ` W ) ( 0vec ` W ) ) )
30 4 17 nvzcl 
 |-  ( W e. NrmCVec -> ( 0vec ` W ) e. ( BaseSet ` W ) )
31 eqid 
 |-  ( +v ` W ) = ( +v ` W )
32 4 31 17 nv0rid 
 |-  ( ( W e. NrmCVec /\ ( 0vec ` W ) e. ( BaseSet ` W ) ) -> ( ( 0vec ` W ) ( +v ` W ) ( 0vec ` W ) ) = ( 0vec ` W ) )
33 7 30 32 syl2anc2 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( ( 0vec ` W ) ( +v ` W ) ( 0vec ` W ) ) = ( 0vec ` W ) )
34 25 29 33 3eqtrd 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( ( x ( .sOLD ` W ) ( Z ` y ) ) ( +v ` W ) ( Z ` z ) ) = ( 0vec ` W ) )
35 19 34 eqtr4d 
 |-  ( ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) /\ ( y e. ( BaseSet ` U ) /\ z e. ( BaseSet ` U ) ) ) -> ( Z ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` W ) ( Z ` y ) ) ( +v ` W ) ( Z ` z ) ) )
36 35 ralrimivva 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec ) /\ x e. CC ) -> A. y e. ( BaseSet ` U ) A. z e. ( BaseSet ` U ) ( Z ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` W ) ( Z ` y ) ) ( +v ` W ) ( Z ` z ) ) )
37 36 ralrimiva 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> A. x e. CC A. y e. ( BaseSet ` U ) A. z e. ( BaseSet ` U ) ( Z ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` W ) ( Z ` y ) ) ( +v ` W ) ( Z ` z ) ) )
38 3 4 14 31 10 26 2 islno 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( Z e. L <-> ( Z : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ A. x e. CC A. y e. ( BaseSet ` U ) A. z e. ( BaseSet ` U ) ( Z ` ( ( x ( .sOLD ` U ) y ) ( +v ` U ) z ) ) = ( ( x ( .sOLD ` W ) ( Z ` y ) ) ( +v ` W ) ( Z ` z ) ) ) ) )
39 5 37 38 mpbir2and 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z e. L )