Metamath Proof Explorer

Theorem lkrsc

Description: The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 9-Oct-2014)

Ref Expression
Hypotheses lkrsc.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lkrsc.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lkrsc.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lkrsc.t ⊢ · = ( .r ‘ 𝐷 )
lkrsc.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lkrsc.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
lkrsc.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lkrsc.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
lkrsc.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
lkrsc.o ⊢ 0 = ( 0g ‘ 𝐷 )
lkrsc.e ⊢ ( 𝜑 → 𝑅 ≠ 0 )
Assertion lkrsc ( 𝜑 → ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 lkrsc.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lkrsc.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lkrsc.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
4 lkrsc.t ⊢ · = ( .r ‘ 𝐷 )
5 lkrsc.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 lkrsc.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
7 lkrsc.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 lkrsc.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 lkrsc.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐾 )
10 lkrsc.o ⊢ 0 = ( 0g ‘ 𝐷 )
11 lkrsc.e ⊢ ( 𝜑 → 𝑅 ≠ 0 )
12 1 fvexi ⊢ 𝑉 ∈ V
13 12 a1i ⊢ ( 𝜑 → 𝑉 ∈ V )
14 2 3 1 5 lflf ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ 𝐾 )
15 7 8 14 syl2anc ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
16 15 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑉 )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ 𝑣 ) )
18 13 9 16 17 ofc2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = ( ( 𝐺 ‘ 𝑣 ) · 𝑅 ) )
19 18 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ↔ ( ( 𝐺 ‘ 𝑣 ) · 𝑅 ) = 0 ) )
20 2 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝐷 ∈ DivRing )
21 7 20 syl ⊢ ( 𝜑 → 𝐷 ∈ DivRing )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝐷 ∈ DivRing )
23 7 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑊 ∈ LVec )
24 8 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝐺 ∈ 𝐹 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
26 2 3 1 5 lflcl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑣 ) ∈ 𝐾 )
27 23 24 25 26 syl3anc ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑣 ) ∈ 𝐾 )
28 9 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑅 ∈ 𝐾 )
29 11 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑅 ≠ 0 )
30 3 10 4 22 27 28 29 drngmuleq0 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐺 ‘ 𝑣 ) · 𝑅 ) = 0 ↔ ( 𝐺 ‘ 𝑣 ) = 0 ) )
31 19 30 bitrd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ↔ ( 𝐺 ‘ 𝑣 ) = 0 ) )
32 31 pm5.32da ⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝑉 ∧ ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = 0 ) ) )
33 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
34 7 33 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
35 1 2 3 4 5 34 8 9 lflvscl ⊢ ( 𝜑 → ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ∈ 𝐹 )
36 1 2 10 5 6 ellkr ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ∈ 𝐹 ) → ( 𝑣 ∈ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ) ) )
37 7 35 36 syl2anc ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ‘ 𝑣 ) = 0 ) ) )
38 1 2 10 5 6 ellkr ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ) → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = 0 ) ) )
39 7 8 38 syl2anc ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = 0 ) ) )
40 32 37 39 3bitr4d ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) ↔ 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ) )
41 40 eqrdv ⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐺 ∘f · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿 ‘ 𝐺 ) )