Theorem lhp2at0ne 40022

Description: Inequality for joins with 2 different atoms (or an atom and zero) under co-atom 𝑊. (Contributed by NM, 28-Jul-2013.)

Hypotheses

Ref	Expression
lhp2at0nle.l	⊢ ≤ = (le‘𝐾)
lhp2at0nle.j	⊢ ∨ = (join‘𝐾)
lhp2at0nle.z	⊢ 0 = (0.‘𝐾)
lhp2at0nle.a	⊢ 𝐴 = (Atoms‘𝐾)
lhp2at0nle.h	⊢ 𝐻 = (LHyp‘𝐾)

Assertion

Ref	Expression
lhp2at0ne	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝑃 ∨ 𝑈) ≠ (𝑄 ∨ 𝑉))

Proof of Theorem lhp2at0ne

Step	Hyp	Ref	Expression
1		simp11 1204	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp12 1205	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
3		simp3 1138	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → 𝑈 ≠ 𝑉)
4		simp2l 1200	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → ((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊))
5		simp2r 1201	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
6		lhp2at0nle.l	. . . 4 ⊢ ≤ = (le‘𝐾)
7		lhp2at0nle.j	. . . 4 ⊢ ∨ = (join‘𝐾)
8		lhp2at0nle.z	. . . 4 ⊢ 0 = (0.‘𝐾)
9		lhp2at0nle.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
10		lhp2at0nle.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
11	6, 7, 8, 9, 10	lhp2at0nle 40021	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑈 ≠ 𝑉) ∧ ((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ¬ 𝑉 ≤ (𝑃 ∨ 𝑈))
12	1, 2, 3, 4, 5, 11	syl311anc 1386	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → ¬ 𝑉 ≤ (𝑃 ∨ 𝑈))
13		simp11l 1285	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → 𝐾 ∈ HL)
14		simp13 1206	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → 𝑄 ∈ 𝐴)
15		simp2rl 1243	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → 𝑉 ∈ 𝐴)
16	6, 7, 9	hlatlej2 39361	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → 𝑉 ≤ (𝑄 ∨ 𝑉))
17	13, 14, 15, 16	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → 𝑉 ≤ (𝑄 ∨ 𝑉))
18	17	adantr 480	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) ∧ (𝑃 ∨ 𝑈) = (𝑄 ∨ 𝑉)) → 𝑉 ≤ (𝑄 ∨ 𝑉))
19		simpr 484	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) ∧ (𝑃 ∨ 𝑈) = (𝑄 ∨ 𝑉)) → (𝑃 ∨ 𝑈) = (𝑄 ∨ 𝑉))
20	18, 19	breqtrrd 5143	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) ∧ (𝑃 ∨ 𝑈) = (𝑄 ∨ 𝑉)) → 𝑉 ≤ (𝑃 ∨ 𝑈))
21	20	ex 412	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → ((𝑃 ∨ 𝑈) = (𝑄 ∨ 𝑉) → 𝑉 ≤ (𝑃 ∨ 𝑈)))
22	21	necon3bd 2941	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (¬ 𝑉 ≤ (𝑃 ∨ 𝑈) → (𝑃 ∨ 𝑈) ≠ (𝑄 ∨ 𝑉)))
23	12, 22	mpd 15	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝑃 ∨ 𝑈) ≠ (𝑄 ∨ 𝑉))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2927   class class class wbr 5115  ‘cfv 6519  (class class class)co 7394  lecple 17233  joincjn 18278  0.cp0 18388  Atomscatm 39248  HLchlt 39335  LHypclh 39970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5242  ax-sep 5259  ax-nul 5269  ax-pow 5328  ax-pr 5395  ax-un 7718

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2880  df-ne 2928  df-ral 3047  df-rex 3056  df-rmo 3357  df-reu 3358  df-rab 3412  df-v 3457  df-sbc 3762  df-csb 3871  df-dif 3925  df-un 3927  df-in 3929  df-ss 3939  df-nul 4305  df-if 4497  df-pw 4573  df-sn 4598  df-pr 4600  df-op 4604  df-uni 4880  df-iun 4965  df-iin 4966  df-br 5116  df-opab 5178  df-mpt 5197  df-id 5541  df-xp 5652  df-rel 5653  df-cnv 5654  df-co 5655  df-dm 5656  df-rn 5657  df-res 5658  df-ima 5659  df-iota 6472  df-fun 6521  df-fn 6522  df-f 6523  df-f1 6524  df-fo 6525  df-f1o 6526  df-fv 6527  df-riota 7351  df-ov 7397  df-oprab 7398  df-mpo 7399  df-1st 7977  df-2nd 7978  df-proset 18261  df-poset 18280  df-plt 18295  df-lub 18311  df-glb 18312  df-join 18313  df-meet 18314  df-p0 18390  df-lat 18397  df-clat 18464  df-oposet 39161  df-ol 39163  df-oml 39164  df-covers 39251  df-ats 39252  df-atl 39283  df-cvlat 39307  df-hlat 39336  df-psubsp 39489  df-pmap 39490  df-padd 39782  df-lhyp 39974

This theorem is referenced by:  cdlemg31b0a  40681