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