Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lnon0 Structured version   Unicode version

Theorem lnon0 26284
 Description: The domain of a nonzero linear operator contains a nonzero vector. (Contributed by NM, 15-Dec-2007.) (New usage is discouraged.)
Hypotheses
Ref Expression
lnon0.1
lnon0.6
lnon0.0
lnon0.7
Assertion
Ref Expression
lnon0
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem lnon0
StepHypRef Expression
1 ralnex 2878 . . . . 5
2 nne 2631 . . . . . 6
32ralbii 2863 . . . . 5
41, 3bitr3i 254 . . . 4
5 fveq2 5881 . . . . . . . . . 10
6 lnon0.1 . . . . . . . . . . 11
7 eqid 2429 . . . . . . . . . . 11
8 lnon0.6 . . . . . . . . . . 11
9 eqid 2429 . . . . . . . . . . 11
10 lnon0.7 . . . . . . . . . . 11
116, 7, 8, 9, 10lno0 26242 . . . . . . . . . 10
125, 11sylan9eqr 2492 . . . . . . . . 9
1312ex 435 . . . . . . . 8
1413ralimdv 2842 . . . . . . 7
156, 7, 10lnof 26241 . . . . . . . 8
16 ffn 5746 . . . . . . . 8
1715, 16syl 17 . . . . . . 7
1814, 17jctild 545 . . . . . 6
19 fconstfv 6141 . . . . . . 7
20 fvex 5891 . . . . . . . 8
2120fconst2 6136 . . . . . . 7
2219, 21bitr3i 254 . . . . . 6
2318, 22syl6ib 229 . . . . 5
24 lnon0.0 . . . . . . . 8
256, 9, 240ofval 26273 . . . . . . 7
26253adant3 1025 . . . . . 6
2726eqeq2d 2443 . . . . 5
2823, 27sylibrd 237 . . . 4
294, 28syl5bi 220 . . 3