Metamath Proof Explorer


Theorem lkr0f

Description: The kernel of the zero functional is the set of all vectors. (Contributed by NM, 17-Apr-2014)

Ref Expression
Hypotheses lkr0f.d 𝐷 = ( Scalar ‘ 𝑊 )
lkr0f.o 0 = ( 0g𝐷 )
lkr0f.v 𝑉 = ( Base ‘ 𝑊 )
lkr0f.f 𝐹 = ( LFnl ‘ 𝑊 )
lkr0f.k 𝐾 = ( LKer ‘ 𝑊 )
Assertion lkr0f ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 𝐾𝐺 ) = 𝑉𝐺 = ( 𝑉 × { 0 } ) ) )

Proof

Step Hyp Ref Expression
1 lkr0f.d 𝐷 = ( Scalar ‘ 𝑊 )
2 lkr0f.o 0 = ( 0g𝐷 )
3 lkr0f.v 𝑉 = ( Base ‘ 𝑊 )
4 lkr0f.f 𝐹 = ( LFnl ‘ 𝑊 )
5 lkr0f.k 𝐾 = ( LKer ‘ 𝑊 )
6 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7 1 6 3 4 lflf ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝐷 ) )
8 7 ffnd ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → 𝐺 Fn 𝑉 )
9 8 adantr ( ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) ∧ ( 𝐾𝐺 ) = 𝑉 ) → 𝐺 Fn 𝑉 )
10 1 2 4 5 lkrval ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐾𝐺 ) = ( 𝐺 “ { 0 } ) )
11 10 eqeq1d ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 𝐾𝐺 ) = 𝑉 ↔ ( 𝐺 “ { 0 } ) = 𝑉 ) )
12 11 biimpa ( ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) ∧ ( 𝐾𝐺 ) = 𝑉 ) → ( 𝐺 “ { 0 } ) = 𝑉 )
13 2 fvexi 0 ∈ V
14 13 fconst2 ( 𝐺 : 𝑉 ⟶ { 0 } ↔ 𝐺 = ( 𝑉 × { 0 } ) )
15 fconst4 ( 𝐺 : 𝑉 ⟶ { 0 } ↔ ( 𝐺 Fn 𝑉 ∧ ( 𝐺 “ { 0 } ) = 𝑉 ) )
16 14 15 bitr3i ( 𝐺 = ( 𝑉 × { 0 } ) ↔ ( 𝐺 Fn 𝑉 ∧ ( 𝐺 “ { 0 } ) = 𝑉 ) )
17 9 12 16 sylanbrc ( ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) ∧ ( 𝐾𝐺 ) = 𝑉 ) → 𝐺 = ( 𝑉 × { 0 } ) )
18 17 ex ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 𝐾𝐺 ) = 𝑉𝐺 = ( 𝑉 × { 0 } ) ) )
19 16 biimpi ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐺 Fn 𝑉 ∧ ( 𝐺 “ { 0 } ) = 𝑉 ) )
20 19 adantl ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐺 Fn 𝑉 ∧ ( 𝐺 “ { 0 } ) = 𝑉 ) )
21 simpr ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 = ( 𝑉 × { 0 } ) )
22 eqid ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
23 1 2 3 22 lfl0f ( 𝑊 ∈ LMod → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) )
24 23 adantr ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) )
25 21 24 eqeltrd ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 ∈ ( LFnl ‘ 𝑊 ) )
26 1 2 22 5 lkrval ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ ( LFnl ‘ 𝑊 ) ) → ( 𝐾𝐺 ) = ( 𝐺 “ { 0 } ) )
27 25 26 syldan ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐾𝐺 ) = ( 𝐺 “ { 0 } ) )
28 27 eqeq1d ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐾𝐺 ) = 𝑉 ↔ ( 𝐺 “ { 0 } ) = 𝑉 ) )
29 ffn ( 𝐺 : 𝑉 ⟶ { 0 } → 𝐺 Fn 𝑉 )
30 14 29 sylbir ( 𝐺 = ( 𝑉 × { 0 } ) → 𝐺 Fn 𝑉 )
31 30 adantl ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 Fn 𝑉 )
32 31 biantrurd ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐺 “ { 0 } ) = 𝑉 ↔ ( 𝐺 Fn 𝑉 ∧ ( 𝐺 “ { 0 } ) = 𝑉 ) ) )
33 28 32 bitrd ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐾𝐺 ) = 𝑉 ↔ ( 𝐺 Fn 𝑉 ∧ ( 𝐺 “ { 0 } ) = 𝑉 ) ) )
34 20 33 mpbird ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐾𝐺 ) = 𝑉 )
35 34 ex ( 𝑊 ∈ LMod → ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐾𝐺 ) = 𝑉 ) )
36 35 adantr ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐾𝐺 ) = 𝑉 ) )
37 18 36 impbid ( ( 𝑊 ∈ LMod ∧ 𝐺𝐹 ) → ( ( 𝐾𝐺 ) = 𝑉𝐺 = ( 𝑉 × { 0 } ) ) )