This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrdi ⊢ ( 𝜑 → ( 𝐺 = ( 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 ⊢ ( 𝜑 → ( 𝐾 ‘ 𝐺 ) = ( 𝐾 ‘ 𝐻 ) )