Proof of Theorem lfl1dim2N
Step | Hyp | Ref
| Expression |
1 | | lfl1dim.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | lveclmod 18927 |
. . . . . . . . 9
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ LMod) |
4 | | lfl1dim.d |
. . . . . . . . 9
⊢ 𝐷 = (Scalar‘𝑊) |
5 | | lfl1dim.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝐷) |
6 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐷) = (0g‘𝐷) |
7 | 4, 5, 6 | lmod0cl 18712 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod →
(0g‘𝐷)
∈ 𝐾) |
8 | 3, 7 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0g‘𝐷) ∈ 𝐾) |
9 | 8 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑔 = (𝑉 × {(0g‘𝐷)})) →
(0g‘𝐷)
∈ 𝐾) |
10 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑔 = (𝑉 × {(0g‘𝐷)})) → 𝑔 = (𝑉 × {(0g‘𝐷)})) |
11 | | lfl1dim.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
12 | | lfl1dim.f |
. . . . . . . 8
⊢ 𝐹 = (LFnl‘𝑊) |
13 | | lfl1dim.t |
. . . . . . . 8
⊢ · =
(.r‘𝐷) |
14 | 3 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑔 = (𝑉 × {(0g‘𝐷)})) → 𝑊 ∈ LMod) |
15 | | lfl1dim.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
16 | 15 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑔 = (𝑉 × {(0g‘𝐷)})) → 𝐺 ∈ 𝐹) |
17 | 11, 4, 12, 5, 13, 6, 14, 16 | lfl0sc 33387 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑔 = (𝑉 × {(0g‘𝐷)})) → (𝐺 ∘𝑓 · (𝑉 ×
{(0g‘𝐷)}))
= (𝑉 ×
{(0g‘𝐷)})) |
18 | 10, 17 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑔 = (𝑉 × {(0g‘𝐷)})) → 𝑔 = (𝐺 ∘𝑓 · (𝑉 ×
{(0g‘𝐷)}))) |
19 | | sneq 4135 |
. . . . . . . . . 10
⊢ (𝑘 = (0g‘𝐷) → {𝑘} = {(0g‘𝐷)}) |
20 | 19 | xpeq2d 5063 |
. . . . . . . . 9
⊢ (𝑘 = (0g‘𝐷) → (𝑉 × {𝑘}) = (𝑉 × {(0g‘𝐷)})) |
21 | 20 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑘 = (0g‘𝐷) → (𝐺 ∘𝑓 · (𝑉 × {𝑘})) = (𝐺 ∘𝑓 · (𝑉 ×
{(0g‘𝐷)}))) |
22 | 21 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑘 = (0g‘𝐷) → (𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})) ↔ 𝑔 = (𝐺 ∘𝑓 · (𝑉 ×
{(0g‘𝐷)})))) |
23 | 22 | rspcev 3282 |
. . . . . 6
⊢
(((0g‘𝐷) ∈ 𝐾 ∧ 𝑔 = (𝐺 ∘𝑓 · (𝑉 ×
{(0g‘𝐷)}))) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))) |
24 | 9, 18, 23 | syl2anc 691 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑔 = (𝑉 × {(0g‘𝐷)})) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))) |
25 | 24 | a1d 25 |
. . . 4
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑔 = (𝑉 × {(0g‘𝐷)})) → ((𝐿‘𝐺) ⊆ (𝐿‘𝑔) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})))) |
26 | 8 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → (0g‘𝐷) ∈ 𝐾) |
27 | | lfl1dim.l |
. . . . . . . . . 10
⊢ 𝐿 = (LKer‘𝑊) |
28 | 3 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → 𝑊 ∈ LMod) |
29 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → 𝑔 ∈ 𝐹) |
30 | 11, 12, 27, 28, 29 | lkrssv 33401 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → (𝐿‘𝑔) ⊆ 𝑉) |
31 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝑊 ∈ LMod) |
32 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → 𝐺 ∈ 𝐹) |
33 | 4, 6, 11, 12, 27 | lkr0f 33399 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)}))) |
34 | 31, 32, 33 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝐿‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × {(0g‘𝐷)}))) |
35 | 34 | biimpar 501 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → (𝐿‘𝐺) = 𝑉) |
36 | 35 | sseq1d 3595 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ((𝐿‘𝐺) ⊆ (𝐿‘𝑔) ↔ 𝑉 ⊆ (𝐿‘𝑔))) |
37 | 36 | biimpa 500 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → 𝑉 ⊆ (𝐿‘𝑔)) |
38 | 30, 37 | eqssd 3585 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → (𝐿‘𝑔) = 𝑉) |
39 | 4, 6, 11, 12, 27 | lkr0f 33399 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑔 ∈ 𝐹) → ((𝐿‘𝑔) = 𝑉 ↔ 𝑔 = (𝑉 × {(0g‘𝐷)}))) |
40 | 28, 29, 39 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → ((𝐿‘𝑔) = 𝑉 ↔ 𝑔 = (𝑉 × {(0g‘𝐷)}))) |
41 | 38, 40 | mpbid 221 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → 𝑔 = (𝑉 × {(0g‘𝐷)})) |
42 | 15 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → 𝐺 ∈ 𝐹) |
43 | 11, 4, 12, 5, 13, 6, 28, 42 | lfl0sc 33387 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → (𝐺 ∘𝑓 · (𝑉 ×
{(0g‘𝐷)}))
= (𝑉 ×
{(0g‘𝐷)})) |
44 | 41, 43 | eqtr4d 2647 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → 𝑔 = (𝐺 ∘𝑓 · (𝑉 ×
{(0g‘𝐷)}))) |
45 | 26, 44, 23 | syl2anc 691 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) ∧ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))) |
46 | 45 | ex 449 |
. . . 4
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝐺 = (𝑉 × {(0g‘𝐷)})) → ((𝐿‘𝐺) ⊆ (𝐿‘𝑔) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})))) |
47 | | eqid 2610 |
. . . . . 6
⊢
(LSHyp‘𝑊) =
(LSHyp‘𝑊) |
48 | 1 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → 𝑊 ∈ LVec) |
49 | 15 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → 𝐺 ∈ 𝐹) |
50 | | simprr 792 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) |
51 | 11, 4, 6, 47, 12, 27 | lkrshp 33410 |
. . . . . . 7
⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)})) → (𝐿‘𝐺) ∈ (LSHyp‘𝑊)) |
52 | 48, 49, 50, 51 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → (𝐿‘𝐺) ∈ (LSHyp‘𝑊)) |
53 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → 𝑔 ∈ 𝐹) |
54 | | simprl 790 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → 𝑔 ≠ (𝑉 × {(0g‘𝐷)})) |
55 | 11, 4, 6, 47, 12, 27 | lkrshp 33410 |
. . . . . . 7
⊢ ((𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ 𝑔 ≠ (𝑉 × {(0g‘𝐷)})) → (𝐿‘𝑔) ∈ (LSHyp‘𝑊)) |
56 | 48, 53, 54, 55 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → (𝐿‘𝑔) ∈ (LSHyp‘𝑊)) |
57 | 47, 48, 52, 56 | lshpcmp 33293 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → ((𝐿‘𝐺) ⊆ (𝐿‘𝑔) ↔ (𝐿‘𝐺) = (𝐿‘𝑔))) |
58 | 1 | ad3antrrr 762 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) ∧ (𝐿‘𝐺) = (𝐿‘𝑔)) → 𝑊 ∈ LVec) |
59 | 15 | ad3antrrr 762 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) ∧ (𝐿‘𝐺) = (𝐿‘𝑔)) → 𝐺 ∈ 𝐹) |
60 | | simpllr 795 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) ∧ (𝐿‘𝐺) = (𝐿‘𝑔)) → 𝑔 ∈ 𝐹) |
61 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) ∧ (𝐿‘𝐺) = (𝐿‘𝑔)) → (𝐿‘𝐺) = (𝐿‘𝑔)) |
62 | 4, 5, 13, 11, 12, 27 | eqlkr2 33405 |
. . . . . . 7
⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝑔)) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))) |
63 | 58, 59, 60, 61, 62 | syl121anc 1323 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) ∧ (𝐿‘𝐺) = (𝐿‘𝑔)) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))) |
64 | 63 | ex 449 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → ((𝐿‘𝐺) = (𝐿‘𝑔) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})))) |
65 | 57, 64 | sylbid 229 |
. . . 4
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ (𝑔 ≠ (𝑉 × {(0g‘𝐷)}) ∧ 𝐺 ≠ (𝑉 × {(0g‘𝐷)}))) → ((𝐿‘𝐺) ⊆ (𝐿‘𝑔) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})))) |
66 | 25, 46, 65 | pm2.61da2ne 2870 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝐿‘𝐺) ⊆ (𝐿‘𝑔) → ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})))) |
67 | 1 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑘 ∈ 𝐾) → 𝑊 ∈ LVec) |
68 | 15 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑘 ∈ 𝐾) → 𝐺 ∈ 𝐹) |
69 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑘 ∈ 𝐾) → 𝑘 ∈ 𝐾) |
70 | 11, 4, 5, 13, 12, 27, 67, 68, 69 | lkrscss 33403 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 ∈ 𝐹) ∧ 𝑘 ∈ 𝐾) → (𝐿‘𝐺) ⊆ (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑘})))) |
71 | 70 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑘 ∈ 𝐾 → (𝐿‘𝐺) ⊆ (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑘}))))) |
72 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})) → (𝐿‘𝑔) = (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑘})))) |
73 | 72 | sseq2d 3596 |
. . . . . 6
⊢ (𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})) → ((𝐿‘𝐺) ⊆ (𝐿‘𝑔) ↔ (𝐿‘𝐺) ⊆ (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑘}))))) |
74 | 73 | biimprcd 239 |
. . . . 5
⊢ ((𝐿‘𝐺) ⊆ (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑘}))) → (𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})) → (𝐿‘𝐺) ⊆ (𝐿‘𝑔))) |
75 | 71, 74 | syl6 34 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (𝑘 ∈ 𝐾 → (𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})) → (𝐿‘𝐺) ⊆ (𝐿‘𝑔)))) |
76 | 75 | rexlimdv 3012 |
. . 3
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → (∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})) → (𝐿‘𝐺) ⊆ (𝐿‘𝑔))) |
77 | 66, 76 | impbid 201 |
. 2
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐹) → ((𝐿‘𝐺) ⊆ (𝐿‘𝑔) ↔ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘})))) |
78 | 77 | rabbidva 3163 |
1
⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∈ 𝐹 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))}) |