# 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}=\mathrm{BaseSet}\left({U}\right)$
lnon0.6 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
lnon0.0 ${⊢}{O}={U}{0}_{\mathrm{op}}{W}$
lnon0.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
Assertion lnon0 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge {T}\ne {O}\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}\ne {Z}$

### Proof

Step Hyp Ref Expression
1 lnon0.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 lnon0.6 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
3 lnon0.0 ${⊢}{O}={U}{0}_{\mathrm{op}}{W}$
4 lnon0.7 ${⊢}{L}={U}\mathrm{LnOp}{W}$
5 ralnex ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}¬{x}\ne {Z}↔¬\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}\ne {Z}$
6 nne ${⊢}¬{x}\ne {Z}↔{x}={Z}$
7 6 ralbii ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}¬{x}\ne {Z}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}$
8 5 7 bitr3i ${⊢}¬\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}\ne {Z}↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}$
9 fveq2 ${⊢}{x}={Z}\to {T}\left({x}\right)={T}\left({Z}\right)$
10 eqid ${⊢}\mathrm{BaseSet}\left({W}\right)=\mathrm{BaseSet}\left({W}\right)$
11 eqid ${⊢}{0}_{\mathrm{vec}}\left({W}\right)={0}_{\mathrm{vec}}\left({W}\right)$
12 1 10 2 11 4 lno0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}\left({Z}\right)={0}_{\mathrm{vec}}\left({W}\right)$
13 9 12 sylan9eqr ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge {x}={Z}\right)\to {T}\left({x}\right)={0}_{\mathrm{vec}}\left({W}\right)$
14 13 ex ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left({x}={Z}\to {T}\left({x}\right)={0}_{\mathrm{vec}}\left({W}\right)\right)$
15 14 ralimdv ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={0}_{\mathrm{vec}}\left({W}\right)\right)$
16 1 10 4 lnof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}:{X}⟶\mathrm{BaseSet}\left({W}\right)$
17 16 ffnd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}Fn{X}$
18 15 17 jctild ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}\to \left({T}Fn{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={0}_{\mathrm{vec}}\left({W}\right)\right)\right)$
19 fconstfv ${⊢}{T}:{X}⟶\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}↔\left({T}Fn{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={0}_{\mathrm{vec}}\left({W}\right)\right)$
20 fvex ${⊢}{0}_{\mathrm{vec}}\left({W}\right)\in \mathrm{V}$
21 20 fconst2 ${⊢}{T}:{X}⟶\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}↔{T}={X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}$
22 19 21 bitr3i ${⊢}\left({T}Fn{X}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)={0}_{\mathrm{vec}}\left({W}\right)\right)↔{T}={X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}$
23 18 22 syl6ib ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}\to {T}={X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\right)$
24 1 11 3 0ofval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {O}={X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}$
25 24 3adant3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {O}={X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}$
26 25 eqeq2d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left({T}={O}↔{T}={X}×\left\{{0}_{\mathrm{vec}}\left({W}\right)\right\}\right)$
27 23 26 sylibrd ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}={Z}\to {T}={O}\right)$
28 8 27 syl5bi ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left(¬\exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}\ne {Z}\to {T}={O}\right)$
29 28 necon1ad ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left({T}\ne {O}\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}\ne {Z}\right)$
30 29 imp ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\wedge {T}\ne {O}\right)\to \exists {x}\in {X}\phantom{\rule{.4em}{0ex}}{x}\ne {Z}$