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

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 } ) ) )