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

Metamath Proof Explorer

Theorem lfl1

Description: A nonzero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lfl1.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lfl1.o ⊢ 0 = ( 0g ‘ 𝐷 )
lfl1.u ⊢ 1 = ( 1r ‘ 𝐷 )
lfl1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lfl1.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lfl1 ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 )

Proof

Step Hyp Ref Expression
1 lfl1.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2 lfl1.o ⊢ 0 = ( 0g ‘ 𝐷 )
3 lfl1.u ⊢ 1 = ( 1r ‘ 𝐷 )
4 lfl1.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
5 lfl1.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 nne ⊢ ( ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 ↔ ( 𝐺 ‘ 𝑧 ) = 0 )
7 6 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑉 ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 ↔ ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 )
8 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
9 1 8 4 5 lflf ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝐷 ) )
10 9 ffnd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → 𝐺 Fn 𝑉 )
11 fconstfv ⊢ ( 𝐺 : 𝑉 ⟶ { 0 } ↔ ( 𝐺 Fn 𝑉 ∧ ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 ) )
12 11 simplbi2 ⊢ ( 𝐺 Fn 𝑉 → ( ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 → 𝐺 : 𝑉 ⟶ { 0 } ) )
13 10 12 syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 → 𝐺 : 𝑉 ⟶ { 0 } ) )
14 2 fvexi ⊢ 0 ∈ V
15 14 fconst2 ⊢ ( 𝐺 : 𝑉 ⟶ { 0 } ↔ 𝐺 = ( 𝑉 × { 0 } ) )
16 13 15 imbitrdi ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( ∀ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) = 0 → 𝐺 = ( 𝑉 × { 0 } ) ) )
17 7 16 biimtrid ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( ∀ 𝑧 ∈ 𝑉 ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 → 𝐺 = ( 𝑉 × { 0 } ) ) )
18 17 necon3ad ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ≠ ( 𝑉 × { 0 } ) → ¬ ∀ 𝑧 ∈ 𝑉 ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
19 dfrex2 ⊢ ( ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 ↔ ¬ ∀ 𝑧 ∈ 𝑉 ¬ ( 𝐺 ‘ 𝑧 ) ≠ 0 )
20 18 19 imbitrrdi ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ≠ ( 𝑉 × { 0 } ) → ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
21 20 3impia ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 )
22 simp1l ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑊 ∈ LVec )
23 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
24 22 23 syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑊 ∈ LMod )
25 1 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝐷 ∈ DivRing )
26 22 25 syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝐷 ∈ DivRing )
27 simp1r ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝐺 ∈ 𝐹 )
28 simp2 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → 𝑧 ∈ 𝑉 )
29 1 8 4 5 lflcl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
30 22 27 28 29 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) )
31 simp3 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
32 eqid ⊢ ( invr ‘ 𝐷 ) = ( invr ‘ 𝐷 )
33 8 2 32 drnginvrcl ⊢ ( ( 𝐷 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐷 ) )
34 26 30 31 33 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐷 ) )
35 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
36 4 1 35 8 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ 𝑉 ) → ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
37 24 34 28 36 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 )
38 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
39 1 8 38 4 35 5 lflmul ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑧 ) ) )
40 24 27 34 28 39 syl112anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑧 ) ) )
41 8 2 38 3 32 drnginvrl ⊢ ( ( 𝐷 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑧 ) ) = 1 )
42 26 30 31 41 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑧 ) ) = 1 )
43 40 42 eqtrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = 1 )
44 fveqeq2 ⊢ ( 𝑥 = ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) → ( ( 𝐺 ‘ 𝑥 ) = 1 ↔ ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = 1 ) )
45 44 rspcev ⊢ ( ( ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ∈ 𝑉 ∧ ( 𝐺 ‘ ( ( ( invr ‘ 𝐷 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) = 1 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 )
46 37 43 45 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 )
47 46 rexlimdv3a ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 ) )
48 47 3adant3 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( ∃ 𝑧 ∈ 𝑉 ( 𝐺 ‘ 𝑧 ) ≠ 0 → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 ) )
49 21 48 mpd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ∃ 𝑥 ∈ 𝑉 ( 𝐺 ‘ 𝑥 ) = 1 )