Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  1cvrat Structured version   Visualization version   GIF version

Theorem 1cvrat 37086
 Description: Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 30-Apr-2012.)
Hypotheses
Ref Expression
1cvrat.b 𝐵 = (Base‘𝐾)
1cvrat.l = (le‘𝐾)
1cvrat.j = (join‘𝐾)
1cvrat.m = (meet‘𝐾)
1cvrat.u 1 = (1.‘𝐾)
1cvrat.c 𝐶 = ( ⋖ ‘𝐾)
1cvrat.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
1cvrat ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → ((𝑃 𝑄) 𝑋) ∈ 𝐴)

Proof of Theorem 1cvrat
StepHypRef Expression
1 hllat 36973 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ Lat)
213ad2ant1 1130 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝐾 ∈ Lat)
3 simp21 1203 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑃𝐴)
4 1cvrat.b . . . . . . 7 𝐵 = (Base‘𝐾)
5 1cvrat.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
64, 5atbase 36899 . . . . . 6 (𝑃𝐴𝑃𝐵)
73, 6syl 17 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑃𝐵)
8 simp22 1204 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑄𝐴)
94, 5atbase 36899 . . . . . 6 (𝑄𝐴𝑄𝐵)
108, 9syl 17 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑄𝐵)
11 1cvrat.j . . . . . 6 = (join‘𝐾)
124, 11latjcom 17748 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃𝐵𝑄𝐵) → (𝑃 𝑄) = (𝑄 𝑃))
132, 7, 10, 12syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → (𝑃 𝑄) = (𝑄 𝑃))
1413oveq1d 7171 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → ((𝑃 𝑄) 𝑋) = ((𝑄 𝑃) 𝑋))
154, 11latjcl 17740 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑄𝐵𝑃𝐵) → (𝑄 𝑃) ∈ 𝐵)
162, 10, 7, 15syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → (𝑄 𝑃) ∈ 𝐵)
17 simp23 1205 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑋𝐵)
18 1cvrat.m . . . . 5 = (meet‘𝐾)
194, 18latmcom 17764 . . . 4 ((𝐾 ∈ Lat ∧ (𝑄 𝑃) ∈ 𝐵𝑋𝐵) → ((𝑄 𝑃) 𝑋) = (𝑋 (𝑄 𝑃)))
202, 16, 17, 19syl3anc 1368 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → ((𝑄 𝑃) 𝑋) = (𝑋 (𝑄 𝑃)))
2114, 20eqtrd 2793 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → ((𝑃 𝑄) 𝑋) = (𝑋 (𝑄 𝑃)))
22 simp1 1133 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝐾 ∈ HL)
2317, 8, 33jca 1125 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → (𝑋𝐵𝑄𝐴𝑃𝐴))
24 simp31 1206 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑃𝑄)
2524necomd 3006 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑄𝑃)
26 simp33 1208 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → ¬ 𝑃 𝑋)
27 hlop 36972 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ OP)
28273ad2ant1 1130 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝐾 ∈ OP)
29 1cvrat.l . . . . . 6 = (le‘𝐾)
30 1cvrat.u . . . . . 6 1 = (1.‘𝐾)
314, 29, 30ople1 36801 . . . . 5 ((𝐾 ∈ OP ∧ 𝑄𝐵) → 𝑄 1 )
3228, 10, 31syl2anc 587 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑄 1 )
33 simp32 1207 . . . . 5 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑋𝐶 1 )
34 1cvrat.c . . . . . 6 𝐶 = ( ⋖ ‘𝐾)
354, 29, 11, 30, 34, 51cvrjat 37085 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑃𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → (𝑋 𝑃) = 1 )
3622, 17, 3, 33, 26, 35syl32anc 1375 . . . 4 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → (𝑋 𝑃) = 1 )
3732, 36breqtrrd 5064 . . 3 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → 𝑄 (𝑋 𝑃))
384, 29, 11, 18, 5cvrat3 37052 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑄𝐴𝑃𝐴)) → ((𝑄𝑃 ∧ ¬ 𝑃 𝑋𝑄 (𝑋 𝑃)) → (𝑋 (𝑄 𝑃)) ∈ 𝐴))
3938imp 410 . . 3 (((𝐾 ∈ HL ∧ (𝑋𝐵𝑄𝐴𝑃𝐴)) ∧ (𝑄𝑃 ∧ ¬ 𝑃 𝑋𝑄 (𝑋 𝑃))) → (𝑋 (𝑄 𝑃)) ∈ 𝐴)
4022, 23, 25, 26, 37, 39syl23anc 1374 . 2 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → (𝑋 (𝑄 𝑃)) ∈ 𝐴)
4121, 40eqeltrd 2852 1 ((𝐾 ∈ HL ∧ (𝑃𝐴𝑄𝐴𝑋𝐵) ∧ (𝑃𝑄𝑋𝐶 1 ∧ ¬ 𝑃 𝑋)) → ((𝑃 𝑄) 𝑋) ∈ 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951   class class class wbr 5036  ‘cfv 6340  (class class class)co 7156  Basecbs 16554  lecple 16643  joincjn 17633  meetcmee 17634  1.cp1 17727  Latclat 17734  OPcops 36782   ⋖ ccvr 36872  Atomscatm 36873  HLchlt 36960 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-proset 17617  df-poset 17635  df-plt 17647  df-lub 17663  df-glb 17664  df-join 17665  df-meet 17666  df-p0 17728  df-p1 17729  df-lat 17735  df-clat 17797  df-oposet 36786  df-ol 36788  df-oml 36789  df-covers 36876  df-ats 36877  df-atl 36908  df-cvlat 36932  df-hlat 36961 This theorem is referenced by:  cdlemblem  37403  cdlemb  37404  lhpat  37653
 Copyright terms: Public domain W3C validator