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