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 lspsnel ⊢ ( ( 𝐷 ∈ 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 23 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) )
25 20 24 mpbid ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) )
26 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
27 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑊 ∈ LVec )
28 simp2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
29 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) )
30 eldifsni ⊢ ( 𝐺 ∈ ( ( 𝑁 ‘ { 𝐻 } ) ∖ { 0 } ) → 𝐺 ≠ 0 )
31 8 30 syl ⊢ ( 𝜑 → 𝐺 ≠ 0 )
32 31 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐺 ≠ 0 )
33 29 32 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ≠ 0 )
34 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝐷 ) )
35 21 26 3 15 34 11 ldual0 ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
36 35 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
37 36 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ↔ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
38 orc ⊢ ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = 0 ) )
39 37 38 syl6bir ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = 0 ) ) )
40 3 6 lduallvec ⊢ ( 𝜑 → 𝐷 ∈ LVec )
41 40 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐷 ∈ LVec )
42 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
43 28 42 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
44 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐻 ∈ ( Base ‘ 𝐷 ) )
45 13 17 15 16 34 4 41 43 44 lvecvs0or ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) = 0 ↔ ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = 0 ) ) )
46 39 45 sylibrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) = 0 ) )
47 46 necon3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ≠ 0 → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
48 33 47 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
49 eldifsn ⊢ ( 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ↔ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
50 28 48 49 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
51 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → 𝐻 ∈ 𝐹 )
52 21 22 26 1 2 3 17 27 50 51 29 lkreqN ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) )
53 52 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝐺 = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝐻 ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) ) )
54 25 53 mpd ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ 𝐻 ) )