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 A = LSAtoms W
lpolsat.h H = LSHyp W
lpolsat.p P = LPol W
lpolsat.w φ W X
lpolsat.o φ ˙ P
lpolsat.q φ Q A
Assertion lpolsatN φ ˙ Q 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 φ W X
5 lpolsat.o φ ˙ P
6 lpolsat.q φ Q 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 X ˙ P ˙ : 𝒫 Base W LSubSp W ˙ Base W = 0 W x y x Base W y Base W x y ˙ y ˙ x x A ˙ x H ˙ ˙ x = x
11 4 10 syl φ ˙ P ˙ : 𝒫 Base W LSubSp W ˙ Base W = 0 W x y x Base W y Base W x y ˙ y ˙ x x A ˙ x H ˙ ˙ x = x
12 5 11 mpbid φ ˙ : 𝒫 Base W LSubSp W ˙ Base W = 0 W x y x Base W y Base W x y ˙ y ˙ x x A ˙ x H ˙ ˙ x = x
13 simpr3 ˙ : 𝒫 Base W LSubSp W ˙ Base W = 0 W x y x Base W y Base W x y ˙ y ˙ x x A ˙ x H ˙ ˙ x = x x A ˙ x H ˙ ˙ x = x
14 fveq2 x = Q ˙ x = ˙ Q
15 14 eleq1d x = Q ˙ x H ˙ Q H
16 2fveq3 x = Q ˙ ˙ x = ˙ ˙ Q
17 id x = Q x = Q
18 16 17 eqeq12d x = Q ˙ ˙ x = x ˙ ˙ Q = Q
19 15 18 anbi12d x = Q ˙ x H ˙ ˙ x = x ˙ Q H ˙ ˙ Q = Q
20 19 rspcv Q A x A ˙ x H ˙ ˙ x = x ˙ Q H ˙ ˙ Q = Q
21 6 20 syl φ x A ˙ x H ˙ ˙ x = x ˙ Q H ˙ ˙ Q = Q
22 simpl ˙ Q H ˙ ˙ Q = Q ˙ Q H
23 13 21 22 syl56 φ ˙ : 𝒫 Base W LSubSp W ˙ Base W = 0 W x y x Base W y Base W x y ˙ y ˙ x x A ˙ x H ˙ ˙ x = x ˙ Q H
24 12 23 mpd φ ˙ Q H