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 · ( 𝑉 × { 𝑅 } ) ) ) = ( 𝐿𝐺 ) )