Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. 2
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) |
2 | | pssss 4010 |
. . . 4
⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵) |
3 | 2 | adantr 484 |
. . 3
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐴 ⊆ 𝐵) |
4 | | pssnel 4385 |
. . . . . . 7
⊢ (𝐴 ⊊ 𝐵 → ∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴)) |
5 | | ssel2 3895 |
. . . . . . . . . . . 12
⊢ ((𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ (𝐴 ∨ℋ (span‘{𝐶}))) |
6 | | spansncv.1 |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 ∈
Cℋ |
7 | | spansncv.3 |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 ∈ ℋ |
8 | 6, 7 | spansnji 29727 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 +ℋ
(span‘{𝐶})) = (𝐴 ∨ℋ
(span‘{𝐶})) |
9 | 8 | eleq2i 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴 +ℋ (span‘{𝐶})) ↔ 𝑥 ∈ (𝐴 ∨ℋ (span‘{𝐶}))) |
10 | 7 | spansnchi 29643 |
. . . . . . . . . . . . . . 15
⊢
(span‘{𝐶})
∈ Cℋ |
11 | 6, 10 | chseli 29540 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴 +ℋ (span‘{𝐶})) ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ (span‘{𝐶})𝑥 = (𝑦 +ℎ 𝑧)) |
12 | 9, 11 | bitr3i 280 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴 ∨ℋ (span‘{𝐶})) ↔ ∃𝑦 ∈ 𝐴 ∃𝑧 ∈ (span‘{𝐶})𝑥 = (𝑦 +ℎ 𝑧)) |
13 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → (𝑥 ∈ 𝐵 ↔ (𝑦 +ℎ 𝑧) ∈ 𝐵)) |
14 | 13 | biimpac 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 = (𝑦 +ℎ 𝑧)) → (𝑦 +ℎ 𝑧) ∈ 𝐵) |
15 | 2 | sselda 3901 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵) |
16 | | spansncv.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 𝐵 ∈
Cℋ |
17 | 16 | chshii 29308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝐵 ∈
Sℋ |
18 | | shsubcl 29301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈
Sℋ ∧ (𝑦 +ℎ 𝑧) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑦 +ℎ 𝑧) −ℎ 𝑦) ∈ 𝐵) |
19 | 17, 18 | mp3an1 1450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 +ℎ 𝑧) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑦 +ℎ 𝑧) −ℎ 𝑦) ∈ 𝐵) |
20 | 14, 15, 19 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑥 = (𝑦 +ℎ 𝑧)) ∧ (𝐴 ⊊ 𝐵 ∧ 𝑦 ∈ 𝐴)) → ((𝑦 +ℎ 𝑧) −ℎ 𝑦) ∈ 𝐵) |
21 | 20 | exp43 440 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ 𝐵 → (𝑥 = (𝑦 +ℎ 𝑧) → (𝐴 ⊊ 𝐵 → (𝑦 ∈ 𝐴 → ((𝑦 +ℎ 𝑧) −ℎ 𝑦) ∈ 𝐵)))) |
22 | 21 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝐴 → (𝑥 = (𝑦 +ℎ 𝑧) → (𝐴 ⊊ 𝐵 → (𝑥 ∈ 𝐵 → ((𝑦 +ℎ 𝑧) −ℎ 𝑦) ∈ 𝐵)))) |
23 | 22 | imp45 433 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 = (𝑦 +ℎ 𝑧) ∧ (𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵))) → ((𝑦 +ℎ 𝑧) −ℎ 𝑦) ∈ 𝐵) |
24 | 6 | cheli 29313 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ) |
25 | 10 | cheli 29313 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ (span‘{𝐶}) → 𝑧 ∈ ℋ) |
26 | | hvpncan2 29121 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 +ℎ 𝑧) −ℎ
𝑦) = 𝑧) |
27 | 24, 25, 26 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) → ((𝑦 +ℎ 𝑧) −ℎ 𝑦) = 𝑧) |
28 | 27 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) → (((𝑦 +ℎ 𝑧) −ℎ 𝑦) ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)) |
29 | 23, 28 | syl5ib 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) → ((𝑦 ∈ 𝐴 ∧ (𝑥 = (𝑦 +ℎ 𝑧) ∧ (𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵))) → 𝑧 ∈ 𝐵)) |
30 | 29 | imp 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) ∧ (𝑦 ∈ 𝐴 ∧ (𝑥 = (𝑦 +ℎ 𝑧) ∧ (𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵)))) → 𝑧 ∈ 𝐵) |
31 | 30 | anandis 678 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑧 ∈ (span‘{𝐶}) ∧ (𝑥 = (𝑦 +ℎ 𝑧) ∧ (𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵)))) → 𝑧 ∈ 𝐵) |
32 | 31 | exp45 442 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐴 → (𝑧 ∈ (span‘{𝐶}) → (𝑥 = (𝑦 +ℎ 𝑧) → ((𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵) → 𝑧 ∈ 𝐵)))) |
33 | 32 | imp41 429 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 +ℎ 𝑧)) ∧ (𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵)) → 𝑧 ∈ 𝐵) |
34 | 33 | adantrr 717 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 +ℎ 𝑧)) ∧ ((𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 ∈ 𝐴)) → 𝑧 ∈ 𝐵) |
35 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 0ℎ →
(𝑦 +ℎ
𝑧) = (𝑦 +ℎ
0ℎ)) |
36 | | ax-hvaddid 29085 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ℋ → (𝑦 +ℎ
0ℎ) = 𝑦) |
37 | 24, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ 𝐴 → (𝑦 +ℎ 0ℎ) =
𝑦) |
38 | 35, 37 | sylan9eqr 2800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 = 0ℎ) → (𝑦 +ℎ 𝑧) = 𝑦) |
39 | 38 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 = 0ℎ) → (𝑥 = (𝑦 +ℎ 𝑧) ↔ 𝑥 = 𝑦)) |
40 | | eleq1a 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝑥 ∈ 𝐴)) |
41 | 40 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 = 0ℎ) → (𝑥 = 𝑦 → 𝑥 ∈ 𝐴)) |
42 | 39, 41 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 = 0ℎ) → (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 ∈ 𝐴)) |
43 | 42 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 +ℎ 𝑧)) → (𝑧 = 0ℎ → 𝑥 ∈ 𝐴)) |
44 | 43 | necon3bd 2954 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 +ℎ 𝑧)) → (¬ 𝑥 ∈ 𝐴 → 𝑧 ≠ 0ℎ)) |
45 | 44 | imp 410 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 +ℎ 𝑧)) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑧 ≠ 0ℎ) |
46 | | spansnss 29652 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈
Sℋ ∧ 𝑧 ∈ 𝐵) → (span‘{𝑧}) ⊆ 𝐵) |
47 | 17, 46 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ 𝐵 → (span‘{𝑧}) ⊆ 𝐵) |
48 | | spansneleq 29651 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐶 ∈ ℋ ∧ 𝑧 ≠ 0ℎ)
→ (𝑧 ∈
(span‘{𝐶}) →
(span‘{𝑧}) =
(span‘{𝐶}))) |
49 | 7, 48 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ≠ 0ℎ
→ (𝑧 ∈
(span‘{𝐶}) →
(span‘{𝑧}) =
(span‘{𝐶}))) |
50 | 49 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ≠ 0ℎ ∧
𝑧 ∈ (span‘{𝐶})) → (span‘{𝑧}) = (span‘{𝐶})) |
51 | 50 | sseq1d 3932 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ≠ 0ℎ ∧
𝑧 ∈ (span‘{𝐶})) → ((span‘{𝑧}) ⊆ 𝐵 ↔ (span‘{𝐶}) ⊆ 𝐵)) |
52 | 47, 51 | syl5ib 247 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ≠ 0ℎ ∧
𝑧 ∈ (span‘{𝐶})) → (𝑧 ∈ 𝐵 → (span‘{𝐶}) ⊆ 𝐵)) |
53 | 52 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ (span‘{𝐶}) ∧ 𝑧 ≠ 0ℎ) → (𝑧 ∈ 𝐵 → (span‘{𝐶}) ⊆ 𝐵)) |
54 | 45, 53 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ (span‘{𝐶}) ∧ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (𝑦 +ℎ 𝑧)) ∧ ¬ 𝑥 ∈ 𝐴)) → (𝑧 ∈ 𝐵 → (span‘{𝐶}) ⊆ 𝐵)) |
55 | 54 | exp44 441 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (span‘{𝐶}) → (𝑦 ∈ 𝐴 → (𝑥 = (𝑦 +ℎ 𝑧) → (¬ 𝑥 ∈ 𝐴 → (𝑧 ∈ 𝐵 → (span‘{𝐶}) ⊆ 𝐵))))) |
56 | 55 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐴 → (𝑧 ∈ (span‘{𝐶}) → (𝑥 = (𝑦 +ℎ 𝑧) → (¬ 𝑥 ∈ 𝐴 → (𝑧 ∈ 𝐵 → (span‘{𝐶}) ⊆ 𝐵))))) |
57 | 56 | imp41 429 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 +ℎ 𝑧)) ∧ ¬ 𝑥 ∈ 𝐴) → (𝑧 ∈ 𝐵 → (span‘{𝐶}) ⊆ 𝐵)) |
58 | 57 | adantrl 716 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 +ℎ 𝑧)) ∧ ((𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 ∈ 𝐴)) → (𝑧 ∈ 𝐵 → (span‘{𝐶}) ⊆ 𝐵)) |
59 | 34, 58 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 +ℎ 𝑧)) ∧ ((𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 ∈ 𝐴)) → (span‘{𝐶}) ⊆ 𝐵) |
60 | 59 | exp43 440 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ (span‘{𝐶})) → (𝑥 = (𝑦 +ℎ 𝑧) → ((𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ 𝐴 → (span‘{𝐶}) ⊆ 𝐵)))) |
61 | 60 | rexlimivv 3211 |
. . . . . . . . . . . . 13
⊢
(∃𝑦 ∈
𝐴 ∃𝑧 ∈ (span‘{𝐶})𝑥 = (𝑦 +ℎ 𝑧) → ((𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ 𝐴 → (span‘{𝐶}) ⊆ 𝐵))) |
62 | 12, 61 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∨ℋ (span‘{𝐶})) → ((𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ 𝐴 → (span‘{𝐶}) ⊆ 𝐵))) |
63 | 5, 62 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) ∧ 𝑥 ∈ 𝐵) → ((𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ 𝐴 → (span‘{𝐶}) ⊆ 𝐵))) |
64 | 63 | imp 410 |
. . . . . . . . . 10
⊢ (((𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) ∧ 𝑥 ∈ 𝐵) ∧ (𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ 𝐵)) → (¬ 𝑥 ∈ 𝐴 → (span‘{𝐶}) ⊆ 𝐵)) |
65 | 64 | anandirs 679 |
. . . . . . . . 9
⊢ (((𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) ∧ 𝐴 ⊊ 𝐵) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ 𝐴 → (span‘{𝐶}) ⊆ 𝐵)) |
66 | 65 | expimpd 457 |
. . . . . . . 8
⊢ ((𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) ∧ 𝐴 ⊊ 𝐵) → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴) → (span‘{𝐶}) ⊆ 𝐵)) |
67 | 66 | exlimdv 1941 |
. . . . . . 7
⊢ ((𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) ∧ 𝐴 ⊊ 𝐵) → (∃𝑥(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴) → (span‘{𝐶}) ⊆ 𝐵)) |
68 | 4, 67 | syl5 34 |
. . . . . 6
⊢ ((𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) ∧ 𝐴 ⊊ 𝐵) → (𝐴 ⊊ 𝐵 → (span‘{𝐶}) ⊆ 𝐵)) |
69 | 68 | ex 416 |
. . . . 5
⊢ (𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) → (𝐴 ⊊ 𝐵 → (𝐴 ⊊ 𝐵 → (span‘{𝐶}) ⊆ 𝐵))) |
70 | 69 | pm2.43d 53 |
. . . 4
⊢ (𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶})) → (𝐴 ⊊ 𝐵 → (span‘{𝐶}) ⊆ 𝐵)) |
71 | 70 | impcom 411 |
. . 3
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → (span‘{𝐶}) ⊆ 𝐵) |
72 | 6, 10, 16 | chlubii 29553 |
. . 3
⊢ ((𝐴 ⊆ 𝐵 ∧ (span‘{𝐶}) ⊆ 𝐵) → (𝐴 ∨ℋ (span‘{𝐶})) ⊆ 𝐵) |
73 | 3, 71, 72 | syl2anc 587 |
. 2
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → (𝐴 ∨ℋ (span‘{𝐶})) ⊆ 𝐵) |
74 | 1, 73 | eqssd 3918 |
1
⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐵 = (𝐴 ∨ℋ (span‘{𝐶}))) |