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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	lnon0.6	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
	lnon0.0	⊢ 𝑂 = ( 𝑈 0op 𝑊 )
	lnon0.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
Assertion	lnon0	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ 𝑇 ≠ 𝑂 ) → ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		lnon0.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		lnon0.6	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3		lnon0.0	⊢ 𝑂 = ( 𝑈 0op 𝑊 )
4		lnon0.7	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
5		ralnex	⊢ ( ∀ 𝑥 ∈ 𝑋 ¬ 𝑥 ≠ 𝑍 ↔ ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 )
6		nne	⊢ ( ¬ 𝑥 ≠ 𝑍 ↔ 𝑥 = 𝑍 )
7	6	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑋 ¬ 𝑥 ≠ 𝑍 ↔ ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 )
8	5 7	bitr3i	⊢ ( ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 ↔ ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 )
9		fveq2	⊢ ( 𝑥 = 𝑍 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑍 ) )
10		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
11		eqid	⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
12	1 10 2 11 4	lno0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ‘ 𝑍 ) = ( 0vec ‘ 𝑊 ) )
13	9 12	sylan9eqr	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ 𝑥 = 𝑍 ) → ( 𝑇 ‘ 𝑥 ) = ( 0vec ‘ 𝑊 ) )
14	13	ex	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑥 = 𝑍 → ( 𝑇 ‘ 𝑥 ) = ( 0vec ‘ 𝑊 ) ) )
15	14	ralimdv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 → ∀ 𝑥 ∈ 𝑋 ( 𝑇 ‘ 𝑥 ) = ( 0vec ‘ 𝑊 ) ) )
16	1 10 4	lnof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
17	16	ffnd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 Fn 𝑋 )
18	15 17	jctild	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 → ( 𝑇 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑇 ‘ 𝑥 ) = ( 0vec ‘ 𝑊 ) ) ) )
19		fconstfv	⊢ ( 𝑇 : 𝑋 ⟶ { ( 0vec ‘ 𝑊 ) } ↔ ( 𝑇 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑇 ‘ 𝑥 ) = ( 0vec ‘ 𝑊 ) ) )
20		fvex	⊢ ( 0vec ‘ 𝑊 ) ∈ V
21	20	fconst2	⊢ ( 𝑇 : 𝑋 ⟶ { ( 0vec ‘ 𝑊 ) } ↔ 𝑇 = ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) )
22	19 21	bitr3i	⊢ ( ( 𝑇 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑇 ‘ 𝑥 ) = ( 0vec ‘ 𝑊 ) ) ↔ 𝑇 = ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) )
23	18 22	syl6ib	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 → 𝑇 = ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) ) )
24	1 11 3	0ofval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝑂 = ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) )
25	24	3adant3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑂 = ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) )
26	25	eqeq2d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 = 𝑂 ↔ 𝑇 = ( 𝑋 × { ( 0vec ‘ 𝑊 ) } ) ) )
27	23 26	sylibrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ∀ 𝑥 ∈ 𝑋 𝑥 = 𝑍 → 𝑇 = 𝑂 ) )
28	8 27	syl5bi	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 → 𝑇 = 𝑂 ) )
29	28	necon1ad	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ≠ 𝑂 → ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 ) )
30	29	imp	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ 𝑇 ≠ 𝑂 ) → ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 )