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 syl6ib ( ( 𝑊 ∈ LVec ∧ 𝐺𝐹 ) → ( ∀ 𝑧𝑉 ( 𝐺𝑧 ) = 0𝐺 = ( 𝑉 × { 0 } ) ) )
17 7 16 syl5bi ( ( 𝑊 ∈ LVec ∧ 𝐺𝐹 ) → ( ∀ 𝑧𝑉 ¬ ( 𝐺𝑧 ) ≠ 0𝐺 = ( 𝑉 × { 0 } ) ) )
18 17 necon3ad ( ( 𝑊 ∈ LVec ∧ 𝐺𝐹 ) → ( 𝐺 ≠ ( 𝑉 × { 0 } ) → ¬ ∀ 𝑧𝑉 ¬ ( 𝐺𝑧 ) ≠ 0 ) )
19 dfrex2 ( ∃ 𝑧𝑉 ( 𝐺𝑧 ) ≠ 0 ↔ ¬ ∀ 𝑧𝑉 ¬ ( 𝐺𝑧 ) ≠ 0 )
20 18 19 syl6ibr ( ( 𝑊 ∈ 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 )