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 ( 𝜑 → ( ‘ ( 𝑄 ) ) = 𝑄 )