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 ( 𝜑 → ( 𝐿𝐺 ) = ( 𝐿𝐻 ) )