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

Theorem trlval2 38626
Description: The value of the trace of a lattice translation, given any atom 𝑃 not under the fiducial co-atom 𝑊. Note: this requires only the weaker assumption 𝐾 ∈ Lat; we use 𝐾 ∈ HL for convenience. (Contributed by NM, 20-May-2012.)
Hypotheses
Ref Expression
trlval2.l = (le‘𝐾)
trlval2.j = (join‘𝐾)
trlval2.m = (meet‘𝐾)
trlval2.a 𝐴 = (Atoms‘𝐾)
trlval2.h 𝐻 = (LHyp‘𝐾)
trlval2.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlval2.r 𝑅 = ((trL‘𝐾)‘𝑊)
Assertion
Ref Expression
trlval2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))

Proof of Theorem trlval2
Dummy variables 𝑥 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hllat 37825 . . 3 (𝐾 ∈ HL → 𝐾 ∈ Lat)
21anim1i 615 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝐾 ∈ Lat ∧ 𝑊𝐻))
3 eqid 2736 . . . . 5 (Base‘𝐾) = (Base‘𝐾)
4 trlval2.l . . . . 5 = (le‘𝐾)
5 trlval2.j . . . . 5 = (join‘𝐾)
6 trlval2.m . . . . 5 = (meet‘𝐾)
7 trlval2.a . . . . 5 𝐴 = (Atoms‘𝐾)
8 trlval2.h . . . . 5 𝐻 = (LHyp‘𝐾)
9 trlval2.t . . . . 5 𝑇 = ((LTrn‘𝐾)‘𝑊)
10 trlval2.r . . . . 5 𝑅 = ((trL‘𝐾)‘𝑊)
113, 4, 5, 6, 7, 8, 9, 10trlval 38625 . . . 4 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) = (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
12113adant3 1132 . . 3 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
13 simp1l 1197 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
14 simp3l 1201 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
153, 7atbase 37751 . . . . . . 7 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1614, 15syl 17 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 ∈ (Base‘𝐾))
173, 8, 9ltrncl 38588 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃 ∈ (Base‘𝐾)) → (𝐹𝑃) ∈ (Base‘𝐾))
1816, 17syld3an3 1409 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑃) ∈ (Base‘𝐾))
193, 5latjcl 18328 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐹𝑃) ∈ (Base‘𝐾)) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
2013, 16, 18, 19syl3anc 1371 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
21 simp1r 1198 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
223, 8lhpbase 38461 . . . . . 6 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2321, 22syl 17 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 ∈ (Base‘𝐾))
243, 6latmcl 18329 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃)) 𝑊) ∈ (Base‘𝐾))
2513, 20, 23, 24syl3anc 1371 . . . 4 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐹𝑃)) 𝑊) ∈ (Base‘𝐾))
26 simpl3l 1228 . . . . . 6 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → 𝑃𝐴)
27 simpl3r 1229 . . . . . 6 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → ¬ 𝑃 𝑊)
28 breq1 5108 . . . . . . . . . 10 (𝑞 = 𝑃 → (𝑞 𝑊𝑃 𝑊))
2928notbid 317 . . . . . . . . 9 (𝑞 = 𝑃 → (¬ 𝑞 𝑊 ↔ ¬ 𝑃 𝑊))
30 id 22 . . . . . . . . . . . 12 (𝑞 = 𝑃𝑞 = 𝑃)
31 fveq2 6842 . . . . . . . . . . . 12 (𝑞 = 𝑃 → (𝐹𝑞) = (𝐹𝑃))
3230, 31oveq12d 7375 . . . . . . . . . . 11 (𝑞 = 𝑃 → (𝑞 (𝐹𝑞)) = (𝑃 (𝐹𝑃)))
3332oveq1d 7372 . . . . . . . . . 10 (𝑞 = 𝑃 → ((𝑞 (𝐹𝑞)) 𝑊) = ((𝑃 (𝐹𝑃)) 𝑊))
3433eqeq2d 2747 . . . . . . . . 9 (𝑞 = 𝑃 → (𝑥 = ((𝑞 (𝐹𝑞)) 𝑊) ↔ 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
3529, 34imbi12d 344 . . . . . . . 8 (𝑞 = 𝑃 → ((¬ 𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) ↔ (¬ 𝑃 𝑊𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3635rspcv 3577 . . . . . . 7 (𝑃𝐴 → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → (¬ 𝑃 𝑊𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3736com23 86 . . . . . 6 (𝑃𝐴 → (¬ 𝑃 𝑊 → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3826, 27, 37sylc 65 . . . . 5 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
39 simp11 1203 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → (𝐾 ∈ Lat ∧ 𝑊𝐻))
40 simp12 1204 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝐹𝑇)
41 simp13l 1288 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝑃𝐴)
42 simp13r 1289 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ¬ 𝑃 𝑊)
43 simp3 1138 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝑞𝐴)
44 simp2 1137 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ¬ 𝑞 𝑊)
454, 5, 6, 7, 8, 9ltrnu 38584 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑞𝐴 ∧ ¬ 𝑞 𝑊)) → ((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊))
4639, 40, 41, 42, 43, 44, 45syl222anc 1386 . . . . . . . . . 10 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊))
47 eqeq2 2748 . . . . . . . . . . 11 (((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) ↔ 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
4847biimpd 228 . . . . . . . . . 10 (((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
4946, 48syl 17 . . . . . . . . 9 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
50493exp 1119 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (¬ 𝑞 𝑊 → (𝑞𝐴 → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))))
5150com24 95 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → (𝑞𝐴 → (¬ 𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))))
5251ralrimdv 3149 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → ∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
5352adantr 481 . . . . 5 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → ∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
5438, 53impbid 211 . . . 4 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) ↔ 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
5525, 54riota5 7343 . . 3 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))) = ((𝑃 (𝐹𝑃)) 𝑊))
5612, 55eqtrd 2776 . 2 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
572, 56syl3an1 1163 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064   class class class wbr 5105  cfv 6496  crio 7312  (class class class)co 7357  Basecbs 17083  lecple 17140  joincjn 18200  meetcmee 18201  Latclat 18320  Atomscatm 37725  HLchlt 37812  LHypclh 38447  LTrncltrn 38564  trLctrl 38621
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-map 8767  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-lat 18321  df-ats 37729  df-atl 37760  df-cvlat 37784  df-hlat 37813  df-lhyp 38451  df-laut 38452  df-ldil 38567  df-ltrn 38568  df-trl 38622
This theorem is referenced by:  trlcl  38627  trlcnv  38628  trljat1  38629  trljat2  38630  trlat  38632  trl0  38633  trlle  38647  trlval3  38650  trlval5  38652  cdlemd6  38666  cdlemf  39026  cdlemg4a  39071  cdlemg4b1  39072  cdlemg4b2  39073  cdlemg4  39080  cdlemg11b  39105  cdlemg13a  39114  cdlemg13  39115  cdlemg17a  39124  cdlemg17dN  39126  cdlemg17e  39128  cdlemg17f  39129  trlcoabs2N  39185  trlcolem  39189  cdlemg42  39192  cdlemg43  39193  cdlemi1  39281  cdlemk4  39297  cdlemk39  39379  dia2dimlem1  39527  dia2dimlem2  39528  dia2dimlem3  39529  cdlemm10N  39581  cdlemn2  39658  cdlemn10  39669  dihjatcclem3  39883
  Copyright terms: Public domain W3C validator