Metamath Proof Explorer

Theorem lpolsatN

Description: The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolsat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lpolsat.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lpolsat.p ⊢ 𝑃 = ( LPol ‘ 𝑊 )
lpolsat.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
lpolsat.o ⊢ ( 𝜑 → ⊥ ∈ 𝑃 )
lpolsat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion lpolsatN ( 𝜑 → ( ⊥ ‘ 𝑄 ) ∈ 𝐻 )

Proof

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