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

Theorem hlmod1i 37052
Description: A version of the modular law pmod1i 37044 that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012.)
Hypotheses
Ref Expression
hlmod.b 𝐵 = (Base‘𝐾)
hlmod.l = (le‘𝐾)
hlmod.j = (join‘𝐾)
hlmod.m = (meet‘𝐾)
hlmod.f 𝐹 = (pmap‘𝐾)
hlmod.p + = (+𝑃𝐾)
Assertion
Ref Expression
hlmod1i ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌))) → ((𝑋 𝑌) 𝑍) = (𝑋 (𝑌 𝑍))))

Proof of Theorem hlmod1i
StepHypRef Expression
1 hlmod.b . . 3 𝐵 = (Base‘𝐾)
2 hlmod.l . . 3 = (le‘𝐾)
3 hllat 36559 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ Lat)
433ad2ant1 1130 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → 𝐾 ∈ Lat)
5 simp21 1203 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → 𝑋𝐵)
6 simp22 1204 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → 𝑌𝐵)
7 hlmod.j . . . . . 6 = (join‘𝐾)
81, 7latjcl 17650 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
94, 5, 6, 8syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝑋 𝑌) ∈ 𝐵)
10 simp23 1205 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → 𝑍𝐵)
11 hlmod.m . . . . 5 = (meet‘𝐾)
121, 11latmcl 17651 . . . 4 ((𝐾 ∈ Lat ∧ (𝑋 𝑌) ∈ 𝐵𝑍𝐵) → ((𝑋 𝑌) 𝑍) ∈ 𝐵)
134, 9, 10, 12syl3anc 1368 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → ((𝑋 𝑌) 𝑍) ∈ 𝐵)
141, 11latmcl 17651 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑍𝐵) → (𝑌 𝑍) ∈ 𝐵)
154, 6, 10, 14syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝑌 𝑍) ∈ 𝐵)
161, 7latjcl 17650 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑌 𝑍) ∈ 𝐵) → (𝑋 (𝑌 𝑍)) ∈ 𝐵)
174, 5, 15, 16syl3anc 1368 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝑋 (𝑌 𝑍)) ∈ 𝐵)
18 simp1 1133 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → 𝐾 ∈ HL)
19 eqid 2824 . . . . . . . . 9 (Atoms‘𝐾) = (Atoms‘𝐾)
20 hlmod.f . . . . . . . . 9 𝐹 = (pmap‘𝐾)
211, 19, 20pmapssat 36955 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝐹𝑋) ⊆ (Atoms‘𝐾))
2218, 5, 21syl2anc 587 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹𝑋) ⊆ (Atoms‘𝐾))
231, 19, 20pmapssat 36955 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑌𝐵) → (𝐹𝑌) ⊆ (Atoms‘𝐾))
2418, 6, 23syl2anc 587 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹𝑌) ⊆ (Atoms‘𝐾))
25 eqid 2824 . . . . . . . . 9 (PSubSp‘𝐾) = (PSubSp‘𝐾)
261, 25, 20pmapsub 36964 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑍𝐵) → (𝐹𝑍) ∈ (PSubSp‘𝐾))
274, 10, 26syl2anc 587 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹𝑍) ∈ (PSubSp‘𝐾))
28 simp3l 1198 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → 𝑋 𝑍)
291, 2, 20pmaple 36957 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑋𝐵𝑍𝐵) → (𝑋 𝑍 ↔ (𝐹𝑋) ⊆ (𝐹𝑍)))
3018, 5, 10, 29syl3anc 1368 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝑋 𝑍 ↔ (𝐹𝑋) ⊆ (𝐹𝑍)))
3128, 30mpbid 235 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹𝑋) ⊆ (𝐹𝑍))
32 hlmod.p . . . . . . . . 9 + = (+𝑃𝐾)
3319, 25, 32pmod1i 37044 . . . . . . . 8 ((𝐾 ∈ HL ∧ ((𝐹𝑋) ⊆ (Atoms‘𝐾) ∧ (𝐹𝑌) ⊆ (Atoms‘𝐾) ∧ (𝐹𝑍) ∈ (PSubSp‘𝐾))) → ((𝐹𝑋) ⊆ (𝐹𝑍) → (((𝐹𝑋) + (𝐹𝑌)) ∩ (𝐹𝑍)) = ((𝐹𝑋) + ((𝐹𝑌) ∩ (𝐹𝑍)))))
34333impia 1114 . . . . . . 7 ((𝐾 ∈ HL ∧ ((𝐹𝑋) ⊆ (Atoms‘𝐾) ∧ (𝐹𝑌) ⊆ (Atoms‘𝐾) ∧ (𝐹𝑍) ∈ (PSubSp‘𝐾)) ∧ (𝐹𝑋) ⊆ (𝐹𝑍)) → (((𝐹𝑋) + (𝐹𝑌)) ∩ (𝐹𝑍)) = ((𝐹𝑋) + ((𝐹𝑌) ∩ (𝐹𝑍))))
3518, 22, 24, 27, 31, 34syl131anc 1380 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (((𝐹𝑋) + (𝐹𝑌)) ∩ (𝐹𝑍)) = ((𝐹𝑋) + ((𝐹𝑌) ∩ (𝐹𝑍))))
361, 11, 19, 20pmapmeet 36969 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋 𝑌) ∈ 𝐵𝑍𝐵) → (𝐹‘((𝑋 𝑌) 𝑍)) = ((𝐹‘(𝑋 𝑌)) ∩ (𝐹𝑍)))
3718, 9, 10, 36syl3anc 1368 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹‘((𝑋 𝑌) 𝑍)) = ((𝐹‘(𝑋 𝑌)) ∩ (𝐹𝑍)))
38 simp3r 1199 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))
3938ineq1d 4171 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → ((𝐹‘(𝑋 𝑌)) ∩ (𝐹𝑍)) = (((𝐹𝑋) + (𝐹𝑌)) ∩ (𝐹𝑍)))
4037, 39eqtrd 2859 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹‘((𝑋 𝑌) 𝑍)) = (((𝐹𝑋) + (𝐹𝑌)) ∩ (𝐹𝑍)))
411, 11, 19, 20pmapmeet 36969 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑌𝐵𝑍𝐵) → (𝐹‘(𝑌 𝑍)) = ((𝐹𝑌) ∩ (𝐹𝑍)))
4218, 6, 10, 41syl3anc 1368 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹‘(𝑌 𝑍)) = ((𝐹𝑌) ∩ (𝐹𝑍)))
4342oveq2d 7154 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → ((𝐹𝑋) + (𝐹‘(𝑌 𝑍))) = ((𝐹𝑋) + ((𝐹𝑌) ∩ (𝐹𝑍))))
4435, 40, 433eqtr4d 2869 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹‘((𝑋 𝑌) 𝑍)) = ((𝐹𝑋) + (𝐹‘(𝑌 𝑍))))
451, 7, 20, 32pmapjoin 37048 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑌 𝑍) ∈ 𝐵) → ((𝐹𝑋) + (𝐹‘(𝑌 𝑍))) ⊆ (𝐹‘(𝑋 (𝑌 𝑍))))
464, 5, 15, 45syl3anc 1368 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → ((𝐹𝑋) + (𝐹‘(𝑌 𝑍))) ⊆ (𝐹‘(𝑋 (𝑌 𝑍))))
4744, 46eqsstrd 3989 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝐹‘((𝑋 𝑌) 𝑍)) ⊆ (𝐹‘(𝑋 (𝑌 𝑍))))
481, 2, 20pmaple 36957 . . . . 5 ((𝐾 ∈ HL ∧ ((𝑋 𝑌) 𝑍) ∈ 𝐵 ∧ (𝑋 (𝑌 𝑍)) ∈ 𝐵) → (((𝑋 𝑌) 𝑍) (𝑋 (𝑌 𝑍)) ↔ (𝐹‘((𝑋 𝑌) 𝑍)) ⊆ (𝐹‘(𝑋 (𝑌 𝑍)))))
4918, 13, 17, 48syl3anc 1368 . . . 4 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (((𝑋 𝑌) 𝑍) (𝑋 (𝑌 𝑍)) ↔ (𝐹‘((𝑋 𝑌) 𝑍)) ⊆ (𝐹‘(𝑋 (𝑌 𝑍)))))
5047, 49mpbird 260 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → ((𝑋 𝑌) 𝑍) (𝑋 (𝑌 𝑍)))
511, 2, 7, 11mod1ile 17704 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑍 → (𝑋 (𝑌 𝑍)) ((𝑋 𝑌) 𝑍)))
52513impia 1114 . . . 4 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ 𝑋 𝑍) → (𝑋 (𝑌 𝑍)) ((𝑋 𝑌) 𝑍))
534, 5, 6, 10, 28, 52syl131anc 1380 . . 3 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → (𝑋 (𝑌 𝑍)) ((𝑋 𝑌) 𝑍))
541, 2, 4, 13, 17, 50, 53latasymd 17656 . 2 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌)))) → ((𝑋 𝑌) 𝑍) = (𝑋 (𝑌 𝑍)))
55543expia 1118 1 ((𝐾 ∈ HL ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑍 ∧ (𝐹‘(𝑋 𝑌)) = ((𝐹𝑋) + (𝐹𝑌))) → ((𝑋 𝑌) 𝑍) = (𝑋 (𝑌 𝑍))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2115  cin 3917  wss 3918   class class class wbr 5047  cfv 6336  (class class class)co 7138  Basecbs 16472  lecple 16561  joincjn 17543  meetcmee 17544  Latclat 17644  Atomscatm 36459  HLchlt 36546  PSubSpcpsubsp 36692  pmapcpmap 36693  +𝑃cpadd 36991
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-reu 3139  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-iun 4902  df-iin 4903  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7096  df-ov 7141  df-oprab 7142  df-mpo 7143  df-1st 7672  df-2nd 7673  df-proset 17527  df-poset 17545  df-plt 17557  df-lub 17573  df-glb 17574  df-join 17575  df-meet 17576  df-p0 17638  df-lat 17645  df-clat 17707  df-oposet 36372  df-ol 36374  df-oml 36375  df-covers 36462  df-ats 36463  df-atl 36494  df-cvlat 36518  df-hlat 36547  df-psubsp 36699  df-pmap 36700  df-padd 36992
This theorem is referenced by:  atmod1i1  37053  atmod1i2  37055  llnmod1i2  37056
  Copyright terms: Public domain W3C validator