Metamath Proof Explorer


Theorem lhpjat1

Description: The join of a co-atom (hyperplane) and an atom not under it is the lattice unit. (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses lhpjat.l ˙=K
lhpjat.j ˙=joinK
lhpjat.u 1˙=1.K
lhpjat.a A=AtomsK
lhpjat.h H=LHypK
Assertion lhpjat1 KHLWHPA¬P˙WW˙P=1˙

Proof

Step Hyp Ref Expression
1 lhpjat.l ˙=K
2 lhpjat.j ˙=joinK
3 lhpjat.u 1˙=1.K
4 lhpjat.a A=AtomsK
5 lhpjat.h H=LHypK
6 simpll KHLWHPA¬P˙WKHL
7 eqid BaseK=BaseK
8 7 5 lhpbase WHWBaseK
9 8 ad2antlr KHLWHPA¬P˙WWBaseK
10 simprl KHLWHPA¬P˙WPA
11 eqid K=K
12 3 11 5 lhp1cvr KHLWHWK1˙
13 12 adantr KHLWHPA¬P˙WWK1˙
14 simprr KHLWHPA¬P˙W¬P˙W
15 7 1 2 3 11 4 1cvrjat KHLWBaseKPAWK1˙¬P˙WW˙P=1˙
16 6 9 10 13 14 15 syl32anc KHLWHPA¬P˙WW˙P=1˙