Metamath Proof Explorer


Theorem lpolconN

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

Ref Expression
Hypotheses lpolcon.v V = Base W
lpolcon.p P = LPol W
lpolcon.w φ W X
lpolcon.o φ ˙ P
lpolcon.x φ X V
lpolcon.y φ Y V
lpolcon.c φ X Y
Assertion lpolconN φ ˙ Y ˙ X

Proof

Step Hyp Ref Expression
1 lpolcon.v V = Base W
2 lpolcon.p P = LPol W
3 lpolcon.w φ W X
4 lpolcon.o φ ˙ P
5 lpolcon.x φ X V
6 lpolcon.y φ Y V
7 lpolcon.c φ X Y
8 eqid LSubSp W = LSubSp W
9 eqid 0 W = 0 W
10 eqid LSAtoms W = LSAtoms W
11 eqid LSHyp W = LSHyp W
12 1 8 9 10 11 2 islpolN W X ˙ P ˙ : 𝒫 V LSubSp W ˙ V = 0 W x y x V y V x y ˙ y ˙ x x LSAtoms W ˙ x LSHyp W ˙ ˙ x = x
13 3 12 syl φ ˙ P ˙ : 𝒫 V LSubSp W ˙ V = 0 W x y x V y V x y ˙ y ˙ x x LSAtoms W ˙ x LSHyp W ˙ ˙ x = x
14 4 13 mpbid φ ˙ : 𝒫 V LSubSp W ˙ V = 0 W x y x V y V x y ˙ y ˙ x x LSAtoms W ˙ x LSHyp W ˙ ˙ x = x
15 simpr2 ˙ : 𝒫 V LSubSp W ˙ V = 0 W x y x V y V x y ˙ y ˙ x x LSAtoms W ˙ x LSHyp W ˙ ˙ x = x x y x V y V x y ˙ y ˙ x
16 5 6 7 3jca φ X V Y V X Y
17 1 fvexi V V
18 17 elpw2 X 𝒫 V X V
19 5 18 sylibr φ X 𝒫 V
20 17 elpw2 Y 𝒫 V Y V
21 6 20 sylibr φ Y 𝒫 V
22 sseq1 x = X x V X V
23 biidd x = X y V y V
24 sseq1 x = X x y X y
25 22 23 24 3anbi123d x = X x V y V x y X V y V X y
26 fveq2 x = X ˙ x = ˙ X
27 26 sseq2d x = X ˙ y ˙ x ˙ y ˙ X
28 25 27 imbi12d x = X x V y V x y ˙ y ˙ x X V y V X y ˙ y ˙ X
29 biidd y = Y X V X V
30 sseq1 y = Y y V Y V
31 sseq2 y = Y X y X Y
32 29 30 31 3anbi123d y = Y X V y V X y X V Y V X Y
33 fveq2 y = Y ˙ y = ˙ Y
34 33 sseq1d y = Y ˙ y ˙ X ˙ Y ˙ X
35 32 34 imbi12d y = Y X V y V X y ˙ y ˙ X X V Y V X Y ˙ Y ˙ X
36 28 35 sylan9bb x = X y = Y x V y V x y ˙ y ˙ x X V Y V X Y ˙ Y ˙ X
37 36 spc2gv X 𝒫 V Y 𝒫 V x y x V y V x y ˙ y ˙ x X V Y V X Y ˙ Y ˙ X
38 19 21 37 syl2anc φ x y x V y V x y ˙ y ˙ x X V Y V X Y ˙ Y ˙ X
39 16 38 mpid φ x y x V y V x y ˙ y ˙ x ˙ Y ˙ X
40 15 39 syl5 φ ˙ : 𝒫 V LSubSp W ˙ V = 0 W x y x V y V x y ˙ y ˙ x x LSAtoms W ˙ x LSHyp W ˙ ˙ x = x ˙ Y ˙ X
41 14 40 mpd φ ˙ Y ˙ X