Metamath Proof Explorer

Theorem lpolpolsatN

Description: Property of a polarity. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lpolpolsat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lpolpolsat.p ⊢ 𝑃 = ( LPol ‘ 𝑊 )
lpolpolsat.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑋 )
lpolpolsat.o ⊢ ( 𝜑 → ⊥ ∈ 𝑃 )
lpolpolsat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion lpolpolsatN ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑄 ) ) = 𝑄 )

Proof

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