Proof of Theorem lclkrlem1
Step | Hyp | Ref
| Expression |
1 | | lclkrlem1.f |
. . 3
⊢ 𝐹 = (LFnl‘𝑈) |
2 | | lclkrlem1.r |
. . 3
⊢ 𝑅 = (Scalar‘𝑈) |
3 | | lclkrlem1.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
4 | | lclkrlem1.d |
. . 3
⊢ 𝐷 = (LDual‘𝑈) |
5 | | lclkrlem1.t |
. . 3
⊢ · = (
·𝑠 ‘𝐷) |
6 | | lclkrlem1.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
7 | | lclkrlem1.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
8 | | lclkrlem1.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
9 | 6, 7, 8 | dvhlmod 36399 |
. . 3
⊢ (𝜑 → 𝑈 ∈ LMod) |
10 | | lclkrlem1.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
11 | | lclkrlem1.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝐶) |
12 | | lclkrlem1.c |
. . . . . 6
⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥
‘(𝐿‘𝑓))) = (𝐿‘𝑓)} |
13 | 12 | lcfl1lem 36780 |
. . . . 5
⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
14 | 11, 13 | sylib 208 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺))) |
15 | 14 | simpld 475 |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
16 | 1, 2, 3, 4, 5, 9, 10, 15 | ldualvscl 34426 |
. 2
⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐹) |
17 | | lclkrlem1.o |
. . . . . 6
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
18 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑈) =
(Base‘𝑈) |
19 | 6, 7, 17, 18, 8 | dochoc1 36650 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(Base‘𝑈))) =
(Base‘𝑈)) |
20 | 19 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = (0g‘𝑅)) → ( ⊥ ‘( ⊥
‘(Base‘𝑈))) =
(Base‘𝑈)) |
21 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑋 = (0g‘𝑅) → (𝑋 · 𝐺) = ((0g‘𝑅) · 𝐺)) |
22 | 21 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑋 = (0g‘𝑅) → (𝐿‘(𝑋 · 𝐺)) = (𝐿‘((0g‘𝑅) · 𝐺))) |
23 | 4, 9 | lduallmod 34440 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ LMod) |
24 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Base‘𝐷) =
(Base‘𝐷) |
25 | 1, 4, 24, 9, 15 | ldualelvbase 34414 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ (Base‘𝐷)) |
26 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝐷) =
(Scalar‘𝐷) |
27 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝐷)) =
(0g‘(Scalar‘𝐷)) |
28 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(0g‘𝐷) = (0g‘𝐷) |
29 | 24, 26, 5, 27, 28 | lmod0vs 18896 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ LMod ∧ 𝐺 ∈ (Base‘𝐷)) →
((0g‘(Scalar‘𝐷)) · 𝐺) = (0g‘𝐷)) |
30 | 23, 25, 29 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 →
((0g‘(Scalar‘𝐷)) · 𝐺) = (0g‘𝐷)) |
31 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(0g‘𝑅) = (0g‘𝑅) |
32 | 2, 31, 4, 26, 27, 9 | ldual0 34434 |
. . . . . . . . . . 11
⊢ (𝜑 →
(0g‘(Scalar‘𝐷)) = (0g‘𝑅)) |
33 | 32 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 →
((0g‘(Scalar‘𝐷)) · 𝐺) = ((0g‘𝑅) · 𝐺)) |
34 | 18, 2, 31, 4, 28, 9 | ldual0v 34437 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝐷) = ((Base‘𝑈) ×
{(0g‘𝑅)})) |
35 | 30, 33, 34 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ (𝜑 →
((0g‘𝑅)
·
𝐺) = ((Base‘𝑈) ×
{(0g‘𝑅)})) |
36 | 35 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘((0g‘𝑅) · 𝐺)) = (𝐿‘((Base‘𝑈) × {(0g‘𝑅)}))) |
37 | | eqid 2622 |
. . . . . . . . 9
⊢
((Base‘𝑈)
× {(0g‘𝑅)}) = ((Base‘𝑈) × {(0g‘𝑅)}) |
38 | 2, 31, 18, 1 | lfl0f 34356 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ LMod →
((Base‘𝑈) ×
{(0g‘𝑅)})
∈ 𝐹) |
39 | 9, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((Base‘𝑈) ×
{(0g‘𝑅)})
∈ 𝐹) |
40 | | lclkrlem1.l |
. . . . . . . . . . 11
⊢ 𝐿 = (LKer‘𝑈) |
41 | 2, 31, 18, 1, 40 | lkr0f 34381 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ LMod ∧
((Base‘𝑈) ×
{(0g‘𝑅)})
∈ 𝐹) → ((𝐿‘((Base‘𝑈) ×
{(0g‘𝑅)}))
= (Base‘𝑈) ↔
((Base‘𝑈) ×
{(0g‘𝑅)})
= ((Base‘𝑈) ×
{(0g‘𝑅)}))) |
42 | 9, 39, 41 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿‘((Base‘𝑈) × {(0g‘𝑅)})) = (Base‘𝑈) ↔ ((Base‘𝑈) ×
{(0g‘𝑅)})
= ((Base‘𝑈) ×
{(0g‘𝑅)}))) |
43 | 37, 42 | mpbiri 248 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘((Base‘𝑈) × {(0g‘𝑅)})) = (Base‘𝑈)) |
44 | 36, 43 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (𝐿‘((0g‘𝑅) · 𝐺)) = (Base‘𝑈)) |
45 | 22, 44 | sylan9eqr 2678 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = (0g‘𝑅)) → (𝐿‘(𝑋 · 𝐺)) = (Base‘𝑈)) |
46 | 45 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = (0g‘𝑅)) → ( ⊥ ‘(𝐿‘(𝑋 · 𝐺))) = ( ⊥
‘(Base‘𝑈))) |
47 | 46 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = (0g‘𝑅)) → ( ⊥ ‘( ⊥
‘(𝐿‘(𝑋 · 𝐺)))) = ( ⊥ ‘( ⊥
‘(Base‘𝑈)))) |
48 | 20, 47, 45 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = (0g‘𝑅)) → ( ⊥ ‘( ⊥
‘(𝐿‘(𝑋 · 𝐺)))) = (𝐿‘(𝑋 · 𝐺))) |
49 | 14 | simprd 479 |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
50 | 49 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) = (𝐿‘𝐺)) |
51 | 6, 7, 8 | dvhlvec 36398 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LVec) |
52 | 51 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑈 ∈ LVec) |
53 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → 𝐺 ∈ 𝐹) |
54 | 10 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ∈ 𝐵) |
55 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → 𝑋 ≠ (0g‘𝑅)) |
56 | 2, 3, 31, 1, 40, 4, 5, 52, 53, 54, 55 | ldualkrsc 34454 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → (𝐿‘(𝑋 · 𝐺)) = (𝐿‘𝐺)) |
57 | 56 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → ( ⊥ ‘(𝐿‘(𝑋 · 𝐺))) = ( ⊥ ‘(𝐿‘𝐺))) |
58 | 57 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → ( ⊥ ‘( ⊥
‘(𝐿‘(𝑋 · 𝐺)))) = ( ⊥ ‘( ⊥
‘(𝐿‘𝐺)))) |
59 | 50, 58, 56 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ≠ (0g‘𝑅)) → ( ⊥ ‘( ⊥
‘(𝐿‘(𝑋 · 𝐺)))) = (𝐿‘(𝑋 · 𝐺))) |
60 | 48, 59 | pm2.61dane 2881 |
. 2
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(𝐿‘(𝑋 · 𝐺)))) = (𝐿‘(𝑋 · 𝐺))) |
61 | 12 | lcfl1lem 36780 |
. 2
⊢ ((𝑋 · 𝐺) ∈ 𝐶 ↔ ((𝑋 · 𝐺) ∈ 𝐹 ∧ ( ⊥ ‘( ⊥
‘(𝐿‘(𝑋 · 𝐺)))) = (𝐿‘(𝑋 · 𝐺)))) |
62 | 16, 60, 61 | sylanbrc 698 |
1
⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐶) |