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 = 0_{vec} (U)$
	lnon0.0	$⊢ O = U 0_{op} W$
	lnon0.7	$⊢ L = U LnOp W$
Assertion	lnon0	$⊢ ((U \in NrmCVec \land W \in NrmCVec \land T \in L) \land T \neq O) \to \exists x \in X x \neq Z$

Proof

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

Metamath Proof Explorer

Theorem lnon0

Proof