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	$⊢ A = LSAtoms (W)$
	lpolsat.h	$⊢ H = LSHyp (W)$
	lpolsat.p	$⊢ P = LPol (W)$
	lpolsat.w	$⊢ φ \to W \in X$
	lpolsat.o	$⊢ φ \to \underset{˙}{⊥} \in P$
	lpolsat.q	$⊢ φ \to Q \in A$
Assertion	lpolsatN	$⊢ φ \to \underset{˙}{⊥} (Q) \in H$

Proof

Step	Hyp	Ref	Expression
1		lpolsat.a	$⊢ A = LSAtoms (W)$
2		lpolsat.h	$⊢ H = LSHyp (W)$
3		lpolsat.p	$⊢ P = LPol (W)$
4		lpolsat.w	$⊢ φ \to W \in X$
5		lpolsat.o	$⊢ φ \to \underset{˙}{⊥} \in P$
6		lpolsat.q	$⊢ φ \to Q \in A$
7		eqid	$⊢ {Base}_{W} = {Base}_{W}$
8		eqid	$⊢ LSubSp (W) = LSubSp (W)$
9		eqid	$⊢ 0_{W} = 0_{W}$
10	7 8 9 1 2 3	islpolN	$⊢ W \in X \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))))$
11	4 10	syl	$⊢ φ \to (\underset{˙}{⊥} \in P \leftrightarrow (\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))))$
12	5 11	mpbid	$⊢ φ \to (\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)))$
13		simpr3	$⊢ (\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))) \to \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)$
14		fveq2	$⊢ x = Q \to \underset{˙}{⊥} (x) = \underset{˙}{⊥} (Q)$
15	14	eleq1d	$⊢ x = Q \to (\underset{˙}{⊥} (x) \in H \leftrightarrow \underset{˙}{⊥} (Q) \in H)$
16		2fveq3	$⊢ x = Q \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = \underset{˙}{⊥} (\underset{˙}{⊥} (Q))$
17		id	$⊢ x = Q \to x = Q$
18	16 17	eqeq12d	$⊢ x = Q \to (\underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q)$
19	15 18	anbi12d	$⊢ x = Q \to ((\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x) \leftrightarrow (\underset{˙}{⊥} (Q) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q))$
20	19	rspcv	$⊢ Q \in A \to (\forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x) \to (\underset{˙}{⊥} (Q) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q))$
21	6 20	syl	$⊢ φ \to (\forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x) \to (\underset{˙}{⊥} (Q) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q))$
22		simpl	$⊢ (\underset{˙}{⊥} (Q) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (Q)) = Q) \to \underset{˙}{⊥} (Q) \in H$
23	13 21 22	syl56	$⊢ φ \to ((\underset{˙}{⊥} : 𝒫 {Base}_{W} ⟶ LSubSp (W) \land (\underset{˙}{⊥} ({Base}_{W}) = \{0_{W}\} \land \forall x \forall y ((x \subseteq {Base}_{W} \land y \subseteq {Base}_{W} \land x \subseteq y) \to \underset{˙}{⊥} (y) \subseteq \underset{˙}{⊥} (x)) \land \forall x \in A (\underset{˙}{⊥} (x) \in H \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x))) \to \underset{˙}{⊥} (Q) \in H)$
24	12 23	mpd	$⊢ φ \to \underset{˙}{⊥} (Q) \in H$

Metamath Proof Explorer

Theorem lpolsatN

Proof