Proof of Theorem lsppratlem4
Step | Hyp | Ref
| Expression |
1 | | lspprat.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | lveclmod 19501 |
. . . . 5
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LMod) |
4 | | lspprat.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
5 | | lspprat.s |
. . . . 5
⊢ 𝑆 = (LSubSp‘𝑊) |
6 | | lspprat.n |
. . . . 5
⊢ 𝑁 = (LSpan‘𝑊) |
7 | | lspprat.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
8 | 4, 5 | lssss 19329 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ⊆ 𝑉) |
10 | 9 | ssdifssd 3971 |
. . . . . 6
⊢ (𝜑 → (𝑈 ∖ { 0 }) ⊆ 𝑉) |
11 | | lsppratlem1.x2 |
. . . . . 6
⊢ (𝜑 → 𝑥 ∈ (𝑈 ∖ { 0 })) |
12 | 10, 11 | sseldd 3822 |
. . . . 5
⊢ (𝜑 → 𝑥 ∈ 𝑉) |
13 | 9 | ssdifssd 3971 |
. . . . . 6
⊢ (𝜑 → (𝑈 ∖ (𝑁‘{𝑥})) ⊆ 𝑉) |
14 | | lsppratlem1.y2 |
. . . . . 6
⊢ (𝜑 → 𝑦 ∈ (𝑈 ∖ (𝑁‘{𝑥}))) |
15 | 13, 14 | sseldd 3822 |
. . . . 5
⊢ (𝜑 → 𝑦 ∈ 𝑉) |
16 | 4, 5, 6, 3, 12, 15 | lspprcl 19373 |
. . . 4
⊢ (𝜑 → (𝑁‘{𝑥, 𝑦}) ∈ 𝑆) |
17 | | df-pr 4401 |
. . . . 5
⊢ {𝑥, 𝑌} = ({𝑥} ∪ {𝑌}) |
18 | | snsspr1 4576 |
. . . . . . 7
⊢ {𝑥} ⊆ {𝑥, 𝑦} |
19 | | prssi 4583 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → {𝑥, 𝑦} ⊆ 𝑉) |
20 | 12, 15, 19 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → {𝑥, 𝑦} ⊆ 𝑉) |
21 | 4, 6 | lspssid 19380 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ {𝑥, 𝑦} ⊆ 𝑉) → {𝑥, 𝑦} ⊆ (𝑁‘{𝑥, 𝑦})) |
22 | 3, 20, 21 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → {𝑥, 𝑦} ⊆ (𝑁‘{𝑥, 𝑦})) |
23 | 18, 22 | syl5ss 3832 |
. . . . . 6
⊢ (𝜑 → {𝑥} ⊆ (𝑁‘{𝑥, 𝑦})) |
24 | 12 | snssd 4571 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥} ⊆ 𝑉) |
25 | | lspprat.y |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
26 | | lspprat.p |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊊ (𝑁‘{𝑋, 𝑌})) |
27 | 26 | pssssd 3926 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ⊆ (𝑁‘{𝑋, 𝑌})) |
28 | 4, 5, 6, 3, 12, 25 | lspprcl 19373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁‘{𝑥, 𝑌}) ∈ 𝑆) |
29 | | df-pr 4401 |
. . . . . . . . . . . . . . 15
⊢ {𝑋, 𝑌} = ({𝑋} ∪ {𝑌}) |
30 | | lsppratlem4.x3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑌})) |
31 | 30 | snssd 4571 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑋} ⊆ (𝑁‘{𝑥, 𝑌})) |
32 | | snsspr2 4577 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑌} ⊆ {𝑥, 𝑌} |
33 | | prssi 4583 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑥, 𝑌} ⊆ 𝑉) |
34 | 12, 25, 33 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {𝑥, 𝑌} ⊆ 𝑉) |
35 | 4, 6 | lspssid 19380 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ LMod ∧ {𝑥, 𝑌} ⊆ 𝑉) → {𝑥, 𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) |
36 | 3, 34, 35 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {𝑥, 𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) |
37 | 32, 36 | syl5ss 3832 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) |
38 | 31, 37 | unssd 4012 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ({𝑋} ∪ {𝑌}) ⊆ (𝑁‘{𝑥, 𝑌})) |
39 | 29, 38 | syl5eqss 3868 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑋, 𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) |
40 | 5, 6 | lspssp 19383 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑥, 𝑌}) ∈ 𝑆 ∧ {𝑋, 𝑌} ⊆ (𝑁‘{𝑥, 𝑌})) → (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌})) |
41 | 3, 28, 39, 40 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑌})) |
42 | 27, 41 | sstrd 3831 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ⊆ (𝑁‘{𝑥, 𝑌})) |
43 | 17 | fveq2i 6449 |
. . . . . . . . . . . 12
⊢ (𝑁‘{𝑥, 𝑌}) = (𝑁‘({𝑥} ∪ {𝑌})) |
44 | 42, 43 | syl6sseq 3870 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ⊆ (𝑁‘({𝑥} ∪ {𝑌}))) |
45 | 44 | ssdifd 3969 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈 ∖ (𝑁‘{𝑥})) ⊆ ((𝑁‘({𝑥} ∪ {𝑌})) ∖ (𝑁‘{𝑥}))) |
46 | 45, 14 | sseldd 3822 |
. . . . . . . . 9
⊢ (𝜑 → 𝑦 ∈ ((𝑁‘({𝑥} ∪ {𝑌})) ∖ (𝑁‘{𝑥}))) |
47 | 4, 5, 6 | lspsolv 19539 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LVec ∧ ({𝑥} ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑦 ∈ ((𝑁‘({𝑥} ∪ {𝑌})) ∖ (𝑁‘{𝑥})))) → 𝑌 ∈ (𝑁‘({𝑥} ∪ {𝑦}))) |
48 | 1, 24, 25, 46, 47 | syl13anc 1440 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑁‘({𝑥} ∪ {𝑦}))) |
49 | | df-pr 4401 |
. . . . . . . . 9
⊢ {𝑥, 𝑦} = ({𝑥} ∪ {𝑦}) |
50 | 49 | fveq2i 6449 |
. . . . . . . 8
⊢ (𝑁‘{𝑥, 𝑦}) = (𝑁‘({𝑥} ∪ {𝑦})) |
51 | 48, 50 | syl6eleqr 2870 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑥, 𝑦})) |
52 | 51 | snssd 4571 |
. . . . . 6
⊢ (𝜑 → {𝑌} ⊆ (𝑁‘{𝑥, 𝑦})) |
53 | 23, 52 | unssd 4012 |
. . . . 5
⊢ (𝜑 → ({𝑥} ∪ {𝑌}) ⊆ (𝑁‘{𝑥, 𝑦})) |
54 | 17, 53 | syl5eqss 3868 |
. . . 4
⊢ (𝜑 → {𝑥, 𝑌} ⊆ (𝑁‘{𝑥, 𝑦})) |
55 | 5, 6 | lspssp 19383 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑥, 𝑦}) ∈ 𝑆 ∧ {𝑥, 𝑌} ⊆ (𝑁‘{𝑥, 𝑦})) → (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦})) |
56 | 3, 16, 54, 55 | syl3anc 1439 |
. . 3
⊢ (𝜑 → (𝑁‘{𝑥, 𝑌}) ⊆ (𝑁‘{𝑥, 𝑦})) |
57 | 56, 30 | sseldd 3822 |
. 2
⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑥, 𝑦})) |
58 | 57, 51 | jca 507 |
1
⊢ (𝜑 → (𝑋 ∈ (𝑁‘{𝑥, 𝑦}) ∧ 𝑌 ∈ (𝑁‘{𝑥, 𝑦}))) |