Theorem lhpjat2 40583

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

Hypotheses

Ref	Expression
lhpjat.l	⊢ ≤ = (le‘𝐾)
lhpjat.j	⊢ ∨ = (join‘𝐾)
lhpjat.u	⊢ 1 = (1.‘𝐾)
lhpjat.a	⊢ 𝐴 = (Atoms‘𝐾)
lhpjat.h	⊢ 𝐻 = (LHyp‘𝐾)

Assertion

Ref	Expression
lhpjat2	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ 𝑊) = 1 )

Proof of Theorem lhpjat2

Step	Hyp	Ref	Expression
1		hllat 39925	. . . 4 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2	1	ad2antrr 734	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
3		eqid 2752	. . . . 5 ⊢ (Base‘𝐾) = (Base‘𝐾)
4		lhpjat.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
5	3, 4	atbase 39851	. . . 4 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
6	5	ad2antrl 736	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ (Base‘𝐾))
7		lhpjat.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
8	3, 7	lhpbase 40560	. . . 4 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
9	8	ad2antlr 735	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
10		lhpjat.j	. . . 4 ⊢ ∨ = (join‘𝐾)
11	3, 10	latjcom 18451	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑊) = (𝑊 ∨ 𝑃))
12	2, 6, 9, 11	syl3anc 1382	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ 𝑊) = (𝑊 ∨ 𝑃))
13		lhpjat.l	. . 3 ⊢ ≤ = (le‘𝐾)
14		lhpjat.u	. . 3 ⊢ 1 = (1.‘𝐾)
15	13, 10, 14, 4, 7	lhpjat1 40582	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑊 ∨ 𝑃) = 1 )
16	12, 15	eqtrd 2787	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ 𝑊) = 1 )

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1550   ∈ wcel 2132   class class class wbr 5090  ‘cfv 6506  (class class class)co 7381  Basecbs 17217  lecple 17265  joincjn 18315  1.cp1 18426  Latclat 18435  Atomscatm 39825  HLchlt 39912  LHypclh 40546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-rep 5217  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rmo 3357  df-reu 3358  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-riota 7338  df-ov 7384  df-oprab 7385  df-proset 18298  df-poset 18317  df-plt 18332  df-lub 18348  df-glb 18349  df-join 18350  df-meet 18351  df-p0 18427  df-p1 18428  df-lat 18436  df-clat 18503  df-oposet 39738  df-ol 39740  df-oml 39741  df-covers 39828  df-ats 39829  df-atl 39860  df-cvlat 39884  df-hlat 39913  df-lhyp 40550

This theorem is referenced by:  lhpmcvr3  40587  cdleme0cp  40776  cdleme0cq  40777  cdleme1  40789  cdleme4  40800  cdleme5  40802  cdleme8  40812  cdleme9  40815  cdleme10  40816  cdleme22e  40906  cdleme22eALTN  40907  cdleme35b  41012  cdleme35e  41015  cdleme42a  41033  trlcoabs2N  41284  cdlemi1  41380  cdlemk4  41396  dia2dimlem1  41626  cdlemn10  41768  dihglbcpreN  41862