Metamath Proof Explorer


Theorem lkreqN

Description: Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkreq.s 𝑆 = ( Scalar ‘ 𝑊 )
lkreq.r 𝑅 = ( Base ‘ 𝑆 )
lkreq.o 0 = ( 0g𝑆 )
lkreq.f 𝐹 = ( LFnl ‘ 𝑊 )
lkreq.k 𝐾 = ( LKer ‘ 𝑊 )
lkreq.d 𝐷 = ( LDual ‘ 𝑊 )
lkreq.t · = ( ·𝑠𝐷 )
lkreq.w ( 𝜑𝑊 ∈ LVec )
lkreq.a ( 𝜑𝐴 ∈ ( 𝑅 ∖ { 0 } ) )
lkreq.h ( 𝜑𝐻𝐹 )
lkreq.g ( 𝜑𝐺 = ( 𝐴 · 𝐻 ) )
Assertion lkreqN ( 𝜑 → ( 𝐾𝐺 ) = ( 𝐾𝐻 ) )

Proof

Step Hyp Ref Expression
1 lkreq.s 𝑆 = ( Scalar ‘ 𝑊 )
2 lkreq.r 𝑅 = ( Base ‘ 𝑆 )
3 lkreq.o 0 = ( 0g𝑆 )
4 lkreq.f 𝐹 = ( LFnl ‘ 𝑊 )
5 lkreq.k 𝐾 = ( LKer ‘ 𝑊 )
6 lkreq.d 𝐷 = ( LDual ‘ 𝑊 )
7 lkreq.t · = ( ·𝑠𝐷 )
8 lkreq.w ( 𝜑𝑊 ∈ LVec )
9 lkreq.a ( 𝜑𝐴 ∈ ( 𝑅 ∖ { 0 } ) )
10 lkreq.h ( 𝜑𝐻𝐹 )
11 lkreq.g ( 𝜑𝐺 = ( 𝐴 · 𝐻 ) )
12 11 eqeq1d ( 𝜑 → ( 𝐺 = ( 0g𝐷 ) ↔ ( 𝐴 · 𝐻 ) = ( 0g𝐷 ) ) )
13 eqid ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
14 eqid ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
15 eqid ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝐷 ) )
16 eqid ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝐷 ) )
17 eqid ( 0g𝐷 ) = ( 0g𝐷 )
18 6 8 lduallvec ( 𝜑𝐷 ∈ LVec )
19 9 eldifad ( 𝜑𝐴𝑅 )
20 1 2 6 14 15 8 ldualsbase ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = 𝑅 )
21 19 20 eleqtrrd ( 𝜑𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
22 4 6 13 8 10 ldualelvbase ( 𝜑𝐻 ∈ ( Base ‘ 𝐷 ) )
23 13 7 14 15 16 17 18 21 22 lvecvs0or ( 𝜑 → ( ( 𝐴 · 𝐻 ) = ( 0g𝐷 ) ↔ ( 𝐴 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = ( 0g𝐷 ) ) ) )
24 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
25 8 24 syl ( 𝜑𝑊 ∈ LMod )
26 1 3 6 14 16 25 ldual0 ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = 0 )
27 26 eqeq2d ( 𝜑 → ( 𝐴 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ↔ 𝐴 = 0 ) )
28 eldifsni ( 𝐴 ∈ ( 𝑅 ∖ { 0 } ) → 𝐴0 )
29 9 28 syl ( 𝜑𝐴0 )
30 29 a1d ( 𝜑 → ( 𝐻 ≠ ( 0g𝐷 ) → 𝐴0 ) )
31 30 necon4d ( 𝜑 → ( 𝐴 = 0𝐻 = ( 0g𝐷 ) ) )
32 27 31 sylbid ( 𝜑 → ( 𝐴 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) → 𝐻 = ( 0g𝐷 ) ) )
33 idd ( 𝜑 → ( 𝐻 = ( 0g𝐷 ) → 𝐻 = ( 0g𝐷 ) ) )
34 32 33 jaod ( 𝜑 → ( ( 𝐴 = ( 0g ‘ ( Scalar ‘ 𝐷 ) ) ∨ 𝐻 = ( 0g𝐷 ) ) → 𝐻 = ( 0g𝐷 ) ) )
35 23 34 sylbid ( 𝜑 → ( ( 𝐴 · 𝐻 ) = ( 0g𝐷 ) → 𝐻 = ( 0g𝐷 ) ) )
36 12 35 sylbid ( 𝜑 → ( 𝐺 = ( 0g𝐷 ) → 𝐻 = ( 0g𝐷 ) ) )
37 nne ( ¬ 𝐻 ≠ ( 0g𝐷 ) ↔ 𝐻 = ( 0g𝐷 ) )
38 36 37 syl6ibr ( 𝜑 → ( 𝐺 = ( 0g𝐷 ) → ¬ 𝐻 ≠ ( 0g𝐷 ) ) )
39 38 con3d ( 𝜑 → ( ¬ ¬ 𝐻 ≠ ( 0g𝐷 ) → ¬ 𝐺 = ( 0g𝐷 ) ) )
40 39 orrd ( 𝜑 → ( ¬ 𝐻 ≠ ( 0g𝐷 ) ∨ ¬ 𝐺 = ( 0g𝐷 ) ) )
41 ianor ( ¬ ( 𝐻 ≠ ( 0g𝐷 ) ∧ 𝐺 = ( 0g𝐷 ) ) ↔ ( ¬ 𝐻 ≠ ( 0g𝐷 ) ∨ ¬ 𝐺 = ( 0g𝐷 ) ) )
42 40 41 sylibr ( 𝜑 → ¬ ( 𝐻 ≠ ( 0g𝐷 ) ∧ 𝐺 = ( 0g𝐷 ) ) )
43 4 1 2 6 7 25 19 10 ldualvscl ( 𝜑 → ( 𝐴 · 𝐻 ) ∈ 𝐹 )
44 11 43 eqeltrd ( 𝜑𝐺𝐹 )
45 4 5 6 17 8 10 44 lkrpssN ( 𝜑 → ( ( 𝐾𝐻 ) ⊊ ( 𝐾𝐺 ) ↔ ( 𝐻 ≠ ( 0g𝐷 ) ∧ 𝐺 = ( 0g𝐷 ) ) ) )
46 df-pss ( ( 𝐾𝐻 ) ⊊ ( 𝐾𝐺 ) ↔ ( ( 𝐾𝐻 ) ⊆ ( 𝐾𝐺 ) ∧ ( 𝐾𝐻 ) ≠ ( 𝐾𝐺 ) ) )
47 45 46 bitr3di ( 𝜑 → ( ( 𝐻 ≠ ( 0g𝐷 ) ∧ 𝐺 = ( 0g𝐷 ) ) ↔ ( ( 𝐾𝐻 ) ⊆ ( 𝐾𝐺 ) ∧ ( 𝐾𝐻 ) ≠ ( 𝐾𝐺 ) ) ) )
48 1 2 4 5 6 7 8 10 19 lkrss ( 𝜑 → ( 𝐾𝐻 ) ⊆ ( 𝐾 ‘ ( 𝐴 · 𝐻 ) ) )
49 11 fveq2d ( 𝜑 → ( 𝐾𝐺 ) = ( 𝐾 ‘ ( 𝐴 · 𝐻 ) ) )
50 48 49 sseqtrrd ( 𝜑 → ( 𝐾𝐻 ) ⊆ ( 𝐾𝐺 ) )
51 50 biantrurd ( 𝜑 → ( ( 𝐾𝐻 ) ≠ ( 𝐾𝐺 ) ↔ ( ( 𝐾𝐻 ) ⊆ ( 𝐾𝐺 ) ∧ ( 𝐾𝐻 ) ≠ ( 𝐾𝐺 ) ) ) )
52 47 51 bitr4d ( 𝜑 → ( ( 𝐻 ≠ ( 0g𝐷 ) ∧ 𝐺 = ( 0g𝐷 ) ) ↔ ( 𝐾𝐻 ) ≠ ( 𝐾𝐺 ) ) )
53 52 necon2bbid ( 𝜑 → ( ( 𝐾𝐻 ) = ( 𝐾𝐺 ) ↔ ¬ ( 𝐻 ≠ ( 0g𝐷 ) ∧ 𝐺 = ( 0g𝐷 ) ) ) )
54 42 53 mpbird ( 𝜑 → ( 𝐾𝐻 ) = ( 𝐾𝐺 ) )
55 54 eqcomd ( 𝜑 → ( 𝐾𝐺 ) = ( 𝐾𝐻 ) )