Step | Hyp | Ref
| Expression |
1 | | islshpcv.v |
. . 3
⊢ 𝑉 = (Base‘𝑊) |
2 | | islshpcv.s |
. . 3
⊢ 𝑆 = (LSubSp‘𝑊) |
3 | | eqid 2740 |
. . 3
⊢
(LSSum‘𝑊) =
(LSSum‘𝑊) |
4 | | islshpcv.h |
. . 3
⊢ 𝐻 = (LSHyp‘𝑊) |
5 | | eqid 2740 |
. . 3
⊢
(LSAtoms‘𝑊) =
(LSAtoms‘𝑊) |
6 | | islshpcv.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ LVec) |
7 | | lveclmod 20366 |
. . . 4
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝑊 ∈ LMod) |
9 | 1, 2, 3, 4, 5, 8 | islshpat 37027 |
. 2
⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ (LSAtoms‘𝑊)(𝑈(LSSum‘𝑊)𝑞) = 𝑉))) |
10 | | simp12 1203 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑈 ∈ 𝑆) |
11 | 1, 2 | lssss 20196 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑈 ⊆ 𝑉) |
13 | | simp13 1204 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑈 ≠ 𝑉) |
14 | | df-pss 3911 |
. . . . . . . . . . 11
⊢ (𝑈 ⊊ 𝑉 ↔ (𝑈 ⊆ 𝑉 ∧ 𝑈 ≠ 𝑉)) |
15 | 12, 13, 14 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑈 ⊊ 𝑉) |
16 | | psseq2 4028 |
. . . . . . . . . . 11
⊢ ((𝑈(LSSum‘𝑊)𝑞) = 𝑉 → (𝑈 ⊊ (𝑈(LSSum‘𝑊)𝑞) ↔ 𝑈 ⊊ 𝑉)) |
17 | 16 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → (𝑈 ⊊ (𝑈(LSSum‘𝑊)𝑞) ↔ 𝑈 ⊊ 𝑉)) |
18 | 15, 17 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑈 ⊊ (𝑈(LSSum‘𝑊)𝑞)) |
19 | | islshpcv.c |
. . . . . . . . . 10
⊢ 𝐶 = ( ⋖L
‘𝑊) |
20 | 6 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) → 𝑊 ∈ LVec) |
21 | 20 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑊 ∈ LVec) |
22 | | simp2 1136 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑞 ∈ (LSAtoms‘𝑊)) |
23 | 2, 3, 5, 19, 21, 10, 22 | lcv2 37052 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → (𝑈 ⊊ (𝑈(LSSum‘𝑊)𝑞) ↔ 𝑈𝐶(𝑈(LSSum‘𝑊)𝑞))) |
24 | 18, 23 | mpbid 231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑈𝐶(𝑈(LSSum‘𝑊)𝑞)) |
25 | | simp3 1137 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → (𝑈(LSSum‘𝑊)𝑞) = 𝑉) |
26 | 24, 25 | breqtrd 5105 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → 𝑈𝐶𝑉) |
27 | 10, 26 | jca 512 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) ∧ 𝑞 ∈ (LSAtoms‘𝑊) ∧ (𝑈(LSSum‘𝑊)𝑞) = 𝑉) → (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) |
28 | 27 | rexlimdv3a 3217 |
. . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉) → (∃𝑞 ∈ (LSAtoms‘𝑊)(𝑈(LSSum‘𝑊)𝑞) = 𝑉 → (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉))) |
29 | 28 | 3exp 1118 |
. . . 4
⊢ (𝜑 → (𝑈 ∈ 𝑆 → (𝑈 ≠ 𝑉 → (∃𝑞 ∈ (LSAtoms‘𝑊)(𝑈(LSSum‘𝑊)𝑞) = 𝑉 → (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉))))) |
30 | 29 | 3impd 1347 |
. . 3
⊢ (𝜑 → ((𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ (LSAtoms‘𝑊)(𝑈(LSSum‘𝑊)𝑞) = 𝑉) → (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉))) |
31 | | simprl 768 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → 𝑈 ∈ 𝑆) |
32 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → 𝑊 ∈ LVec) |
33 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → 𝑊 ∈ LMod) |
34 | 1, 2 | lss1 20198 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod → 𝑉 ∈ 𝑆) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → 𝑉 ∈ 𝑆) |
36 | | simprr 770 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → 𝑈𝐶𝑉) |
37 | 2, 19, 32, 31, 35, 36 | lcvpss 37034 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → 𝑈 ⊊ 𝑉) |
38 | 37 | pssned 4038 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → 𝑈 ≠ 𝑉) |
39 | 2, 3, 5, 19, 33, 31, 35, 36 | lcvat 37040 |
. . . . 5
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → ∃𝑞 ∈ (LSAtoms‘𝑊)(𝑈(LSSum‘𝑊)𝑞) = 𝑉) |
40 | 31, 38, 39 | 3jca 1127 |
. . . 4
⊢ ((𝜑 ∧ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉)) → (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ (LSAtoms‘𝑊)(𝑈(LSSum‘𝑊)𝑞) = 𝑉)) |
41 | 40 | ex 413 |
. . 3
⊢ (𝜑 → ((𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉) → (𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ (LSAtoms‘𝑊)(𝑈(LSSum‘𝑊)𝑞) = 𝑉))) |
42 | 30, 41 | impbid 211 |
. 2
⊢ (𝜑 → ((𝑈 ∈ 𝑆 ∧ 𝑈 ≠ 𝑉 ∧ ∃𝑞 ∈ (LSAtoms‘𝑊)(𝑈(LSSum‘𝑊)𝑞) = 𝑉) ↔ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉))) |
43 | 9, 42 | bitrd 278 |
1
⊢ (𝜑 → (𝑈 ∈ 𝐻 ↔ (𝑈 ∈ 𝑆 ∧ 𝑈𝐶𝑉))) |