| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lpolpolsat.o | . . 3
⊢ (𝜑 → ⊥ ∈ 𝑃) | 
| 2 |  | lpolpolsat.w | . . . 4
⊢ (𝜑 → 𝑊 ∈ 𝑋) | 
| 3 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝑊) =
(Base‘𝑊) | 
| 4 |  | eqid 2737 | . . . . 5
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) | 
| 5 |  | eqid 2737 | . . . . 5
⊢
(0g‘𝑊) = (0g‘𝑊) | 
| 6 |  | lpolpolsat.a | . . . . 5
⊢ 𝐴 = (LSAtoms‘𝑊) | 
| 7 |  | eqid 2737 | . . . . 5
⊢
(LSHyp‘𝑊) =
(LSHyp‘𝑊) | 
| 8 |  | lpolpolsat.p | . . . . 5
⊢ 𝑃 = (LPol‘𝑊) | 
| 9 | 3, 4, 5, 6, 7, 8 | islpolN 41485 | . . . 4
⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫
(Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))))) | 
| 10 | 2, 9 | syl 17 | . . 3
⊢ (𝜑 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫
(Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))))) | 
| 11 | 1, 10 | mpbid 232 | . 2
⊢ (𝜑 → ( ⊥ :𝒫
(Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) | 
| 12 |  | simpr3 1197 | . . 3
⊢ (( ⊥
:𝒫 (Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) → ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)) | 
| 13 |  | lpolpolsat.q | . . . 4
⊢ (𝜑 → 𝑄 ∈ 𝐴) | 
| 14 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑥 = 𝑄 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑄)) | 
| 15 | 14 | eleq1d 2826 | . . . . . 6
⊢ (𝑥 = 𝑄 → (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ↔ ( ⊥ ‘𝑄) ∈ (LSHyp‘𝑊))) | 
| 16 |  | 2fveq3 6911 | . . . . . . 7
⊢ (𝑥 = 𝑄 → ( ⊥ ‘( ⊥
‘𝑥)) = ( ⊥
‘( ⊥ ‘𝑄))) | 
| 17 |  | id 22 | . . . . . . 7
⊢ (𝑥 = 𝑄 → 𝑥 = 𝑄) | 
| 18 | 16, 17 | eqeq12d 2753 | . . . . . 6
⊢ (𝑥 = 𝑄 → (( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ↔ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄)) | 
| 19 | 15, 18 | anbi12d 632 | . . . . 5
⊢ (𝑥 = 𝑄 → ((( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥) ↔ (( ⊥ ‘𝑄) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄))) | 
| 20 | 19 | rspcv 3618 | . . . 4
⊢ (𝑄 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥) → (( ⊥ ‘𝑄) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄))) | 
| 21 | 13, 20 | syl 17 | . . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥) → (( ⊥ ‘𝑄) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄))) | 
| 22 |  | simpr 484 | . . 3
⊢ ((( ⊥
‘𝑄) ∈
(LSHyp‘𝑊) ∧ (
⊥
‘( ⊥ ‘𝑄)) = 𝑄) → ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄) | 
| 23 | 12, 21, 22 | syl56 36 | . 2
⊢ (𝜑 → (( ⊥ :𝒫
(Base‘𝑊)⟶(LSubSp‘𝑊) ∧ (( ⊥
‘(Base‘𝑊)) =
{(0g‘𝑊)}
∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑊) ∧ 𝑦 ⊆ (Base‘𝑊) ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ 𝐴 (( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) → ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄)) | 
| 24 | 11, 23 | mpd 15 | 1
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘𝑄)) = 𝑄) |