Metamath Proof Explorer

Theorem lnon0

Description: The domain of a nonzero linear operator contains a nonzero vector. (Contributed by NM, 15-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses lnon0.1 
|- X = ( BaseSet ` U )
lnon0.6 
|- Z = ( 0vec ` U )
lnon0.0 
|- O = ( U 0op W )
lnon0.7 
|- L = ( U LnOp W )
Assertion lnon0 
|- ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ T =/= O ) -> E. x e. X x =/= Z )

Proof

Step Hyp Ref Expression
1 lnon0.1 
 |-  X = ( BaseSet ` U )
2 lnon0.6 
 |-  Z = ( 0vec ` U )
3 lnon0.0 
 |-  O = ( U 0op W )
4 lnon0.7 
 |-  L = ( U LnOp W )
5 ralnex 
 |-  ( A. x e. X -. x =/= Z <-> -. E. x e. X x =/= Z )
6 nne 
 |-  ( -. x =/= Z <-> x = Z )
7 6 ralbii 
 |-  ( A. x e. X -. x =/= Z <-> A. x e. X x = Z )
8 5 7 bitr3i 
 |-  ( -. E. x e. X x =/= Z <-> A. x e. X x = Z )
9 fveq2 
 |-  ( x = Z -> ( T ` x ) = ( T ` Z ) )
10 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
11 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
12 1 10 2 11 4 lno0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T ` Z ) = ( 0vec ` W ) )
13 9 12 sylan9eqr 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ x = Z ) -> ( T ` x ) = ( 0vec ` W ) )
14 13 ex 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( x = Z -> ( T ` x ) = ( 0vec ` W ) ) )
15 14 ralimdv 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( A. x e. X x = Z -> A. x e. X ( T ` x ) = ( 0vec ` W ) ) )
16 1 10 4 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : X --> ( BaseSet ` W ) )
17 16 ffnd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T Fn X )
18 15 17 jctild 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( A. x e. X x = Z -> ( T Fn X /\ A. x e. X ( T ` x ) = ( 0vec ` W ) ) ) )
19 fconstfv 
 |-  ( T : X --> { ( 0vec ` W ) } <-> ( T Fn X /\ A. x e. X ( T ` x ) = ( 0vec ` W ) ) )
20 fvex 
 |-  ( 0vec ` W ) e. _V
21 20 fconst2 
 |-  ( T : X --> { ( 0vec ` W ) } <-> T = ( X X. { ( 0vec ` W ) } ) )
22 19 21 bitr3i 
 |-  ( ( T Fn X /\ A. x e. X ( T ` x ) = ( 0vec ` W ) ) <-> T = ( X X. { ( 0vec ` W ) } ) )
23 18 22 syl6ib 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( A. x e. X x = Z -> T = ( X X. { ( 0vec ` W ) } ) ) )
24 1 11 3 0ofval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> O = ( X X. { ( 0vec ` W ) } ) )
25 24 3adant3 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> O = ( X X. { ( 0vec ` W ) } ) )
26 25 eqeq2d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T = O <-> T = ( X X. { ( 0vec ` W ) } ) ) )
27 23 26 sylibrd 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( A. x e. X x = Z -> T = O ) )
28 8 27 syl5bi 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( -. E. x e. X x =/= Z -> T = O ) )
29 28 necon1ad 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T =/= O -> E. x e. X x =/= Z ) )
30 29 imp 
 |-  ( ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) /\ T =/= O ) -> E. x e. X x =/= Z )