Step | Hyp | Ref
| Expression |
1 | | lpolsat.o |
. . 3
⊢ (𝜑 → ⊥ ∈ 𝑃) |
2 | | lpolsat.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ 𝑋) |
3 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) |
4 | | eqid 2738 |
. . . . 5
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
5 | | eqid 2738 |
. . . . 5
⊢
(0g‘𝑊) = (0g‘𝑊) |
6 | | lpolsat.a |
. . . . 5
⊢ 𝐴 = (LSAtoms‘𝑊) |
7 | | lpolsat.h |
. . . . 5
⊢ 𝐻 = (LSHyp‘𝑊) |
8 | | lpolsat.p |
. . . . 5
⊢ 𝑃 = (LPol‘𝑊) |
9 | 3, 4, 5, 6, 7, 8 | islpolN 39497 |
. . . 4
⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫
(Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))))) |
10 | 2, 9 | syl 17 |
. . 3
⊢ (𝜑 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫
(Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))))) |
11 | 1, 10 | mpbid 231 |
. 2
⊢ (𝜑 → ( ⊥ :𝒫
(Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) |
12 | | simpr3 1195 |
. . 3
⊢ (( ⊥
:𝒫 (Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) → ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)) |
13 | | lpolsat.q |
. . . 4
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
14 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑥 = 𝑄 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑄)) |
15 | 14 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 𝑄 → (( ⊥ ‘𝑥) ∈ 𝐻 ↔ ( ⊥ ‘𝑄) ∈ 𝐻)) |
16 | | 2fveq3 6779 |
. . . . . . 7
⊢ (𝑥 = 𝑄 → ( ⊥ ‘( ⊥
‘𝑥)) = ( ⊥
‘( ⊥ ‘𝑄))) |
17 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑄 → 𝑥 = 𝑄) |
18 | 16, 17 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑥 = 𝑄 → (( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ↔ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄)) |
19 | 15, 18 | anbi12d 631 |
. . . . 5
⊢ (𝑥 = 𝑄 → ((( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥) ↔ (( ⊥ ‘𝑄) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄))) |
20 | 19 | rspcv 3557 |
. . . 4
⊢ (𝑄 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥) → (( ⊥ ‘𝑄) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄))) |
21 | 13, 20 | syl 17 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥) → (( ⊥ ‘𝑄) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄))) |
22 | | simpl 483 |
. . 3
⊢ ((( ⊥
‘𝑄) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄) → ( ⊥ ‘𝑄) ∈ 𝐻) |
23 | 12, 21, 22 | syl56 36 |
. 2
⊢ (𝜑 → (( ⊥ :𝒫
(Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ 𝐻 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) → ( ⊥ ‘𝑄) ∈ 𝐻)) |
24 | 11, 23 | mpd 15 |
1
⊢ (𝜑 → ( ⊥ ‘𝑄) ∈ 𝐻) |