Theorem dihmeetlem5 38484

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014.)

Hypotheses

Ref	Expression
dihmeetlem5.b	⊢ 𝐵 = (Base‘𝐾)
dihmeetlem5.l	⊢ ≤ = (le‘𝐾)
dihmeetlem5.j	⊢ ∨ = (join‘𝐾)
dihmeetlem5.m	⊢ ∧ = (meet‘𝐾)
dihmeetlem5.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
dihmeetlem5	⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → (𝑋 ∧ (𝑌 ∨ 𝑄)) = ((𝑋 ∧ 𝑌) ∨ 𝑄))

Proof of Theorem dihmeetlem5

Step	Hyp	Ref	Expression
1		simpl1 1186	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → 𝐾 ∈ HL)
2		simprl 769	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → 𝑄 ∈ 𝐴)
3		simpl2 1187	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → 𝑋 ∈ 𝐵)
4		simpl3 1188	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → 𝑌 ∈ 𝐵)
5		simprr 771	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → 𝑄 ≤ 𝑋)
6		dihmeetlem5.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
7		dihmeetlem5.l	. . . 4 ⊢ ≤ = (le‘𝐾)
8		dihmeetlem5.j	. . . 4 ⊢ ∨ = (join‘𝐾)
9		dihmeetlem5.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
10		dihmeetlem5.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
11	6, 7, 8, 9, 10	atmod2i1 37037	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑄 ≤ 𝑋) → ((𝑋 ∧ 𝑌) ∨ 𝑄) = (𝑋 ∧ (𝑌 ∨ 𝑄)))
12	1, 2, 3, 4, 5, 11	syl131anc 1378	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → ((𝑋 ∧ 𝑌) ∨ 𝑄) = (𝑋 ∧ (𝑌 ∨ 𝑄)))
13	12	eqcomd 2826	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → (𝑋 ∧ (𝑌 ∨ 𝑄)) = ((𝑋 ∧ 𝑌) ∨ 𝑄))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082   = wceq 1536   ∈ wcel 2113   class class class wbr 5059  ‘cfv 6348  (class class class)co 7149  Basecbs 16476  lecple 16565  joincjn 17547  meetcmee 17548  Atomscatm 36439  HLchlt 36526

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5323  ax-un 7454

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-ral 3142  df-rex 3143  df-reu 3144  df-rab 3146  df-v 3493  df-sbc 3769  df-csb 3877  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-pw 4534  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4914  df-iin 4915  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-1st 7682  df-2nd 7683  df-proset 17531  df-poset 17549  df-plt 17561  df-lub 17577  df-glb 17578  df-join 17579  df-meet 17580  df-p0 17642  df-lat 17649  df-clat 17711  df-oposet 36352  df-ol 36354  df-oml 36355  df-covers 36442  df-ats 36443  df-atl 36474  df-cvlat 36498  df-hlat 36527  df-psubsp 36679  df-pmap 36680  df-padd 36972

This theorem is referenced by:  dihmeetlem6  38485  dihjatc1  38487  dihmeetlem10N  38492