Metamath Proof Explorer

Theorem lkrlspeqN

Description: Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkrlspeq.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lkrlspeq.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
lkrlspeq.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
lkrlspeq.o ⊢ 0 = ( 0g ‘ 𝐷 )
lkrlspeq.j ⊢ 𝑁 = ( LSpan ‘ 𝐷 )
lkrlspeq.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lkrlspeq.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
lkrlspeq.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝑁 ‘ { 𝐻 } ) ∖ { 0 } ) )
Assertion lkrlspeqN ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 lkrlspeq.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2 lkrlspeq.l ⊢ 𝐿 = ( LKer ‘ 𝑊 )
3 lkrlspeq.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
4 lkrlspeq.o ⊢ 0 = ( 0g ‘ 𝐷 )
5 lkrlspeq.j ⊢ 𝑁 = ( LSpan ‘ 𝐷 )
6 lkrlspeq.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lkrlspeq.h ⊢ ( 𝜑 → 𝐻 ∈ 𝐹 )
8 lkrlspeq.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝑁 ‘ { 𝐻 } ) ∖ { 0 } ) )
9 8 eldifad ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 ‘ { 𝐻 } ) )
10 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
11 6 10 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
12 3 11 lduallmod ⊢ ( 𝜑 → 𝐷 ∈ LMod )
13 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
14 1 3 13 6 7 ldualelvbase ⊢ ( 𝜑 → 𝐻 ∈ ( Base ‘ 𝐷 ) )
15 eqid ⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
16 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝐷 ) )
17 eqid ⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
18 15 16 13 17 5 ellspsn ⊢ ( ( 𝐷 ∈ LMod ∧ 𝐻 ∈ ( Base ‘ 𝐷 ) ) → ( 𝐺 ∈ ( 𝑁 ‘ { 𝐻 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) )
19 12 14 18 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑁 ‘ { 𝐻 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) )
20 9 19 mpbid ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) )
21 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
22 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
23 21 22 3 15 16 6 ldualsbase ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
24 20 23 rexeqtrdv ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) )
25 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
26 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑊 ∈ LVec )
27 simp2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
28 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) )
29 eldifsni ⊢ ( 𝐺 ∈ ( ( 𝑁 ‘ { 𝐻 } ) ∖ { 0 } ) → 𝐺 ≠ 0 )
30 8 29 syl ⊢ ( 𝜑 → 𝐺 ≠ 0 )
31 30 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐺 ≠ 0 )
32 28 31 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ≠ 0 )
33 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝐷 ) )
34 21 25 3 15 33 11 ldual0 ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
35 34 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
36 35 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ↔ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
37 orc ⊢ ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = 0 ) )
38 36 37 biimtrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = 0 ) ) )
39 3 6 lduallvec ⊢ ( 𝜑 → 𝐷 ∈ LVec )
40 39 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐷 ∈ LVec )
41 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
42 27 41 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
43 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐻 ∈ ( Base ‘ 𝐷 ) )
44 13 17 15 16 33 4 40 42 43 lvecvs0or ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) = 0 ↔ ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = 0 ) ) )
45 38 44 sylibrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) = 0 ) )
46 45 necon3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ≠ 0 → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
47 32 46 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
48 eldifsn ⊢ ( 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↔ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
49 27 47 48 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
50 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐻 ∈ 𝐹 )
51 21 22 25 1 2 3 17 26 49 50 28 lkreqN ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) )
52 51 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) )
53 24 52 mpd ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) )