This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( 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 imbitrdi ⊢ ( ( 𝑈 ∈ 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 biimtrid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 → 𝑇 = 𝑂 ) )
29 28 necon1ad ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → ( 𝑇 ≠ 𝑂 → ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 ) )
30 29 imp ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) ∧ 𝑇 ≠ 𝑂 ) → ∃ 𝑥 ∈ 𝑋 𝑥 ≠ 𝑍 )