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 bilani ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) )
20 simpr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 = ( 𝑉 × { 0 } ) )
21 eqid ⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
22 1 2 3 21 lfl0f ⊢ ( 𝑊 ∈ LMod → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) )
23 22 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) )
24 20 23 eqeltrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 ∈ ( LFnl ‘ 𝑊 ) )
25 1 2 21 5 lkrval ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ ( LFnl ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) )
26 24 25 syldan ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) )
27 26 eqeq1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) )
28 ffn ⊢ ( 𝐺 : 𝑉 ⟶ { 0 } → 𝐺 Fn 𝑉 )
29 14 28 sylbir ⊢ ( 𝐺 = ( 𝑉 × { 0 } ) → 𝐺 Fn 𝑉 )
30 29 adantl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 Fn 𝑉 )
31 30 biantrurd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( ◡ 𝐺 “ { 0 } ) = 𝑉 ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) )
32 27 31 bitrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) )
33 19 32 mpbird ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 )
34 33 ex ⊢ ( 𝑊 ∈ LMod → ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
35 34 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
36 18 35 impbid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )