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 37181
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 36381 . . 3 (𝐾 ∈ HL → 𝐾 ∈ Lat)
21anim1i 614 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝐾 ∈ Lat ∧ 𝑊𝐻))
3 eqid 2821 . . . . 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 37180 . . . 4 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) = (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
12113adant3 1124 . . 3 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
13 simp1l 1189 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
14 simp3l 1193 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
153, 7atbase 36307 . . . . . . 7 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1614, 15syl 17 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 ∈ (Base‘𝐾))
173, 8, 9ltrncl 37143 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃 ∈ (Base‘𝐾)) → (𝐹𝑃) ∈ (Base‘𝐾))
1816, 17syld3an3 1401 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑃) ∈ (Base‘𝐾))
193, 5latjcl 17651 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐹𝑃) ∈ (Base‘𝐾)) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
2013, 16, 18, 19syl3anc 1363 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
21 simp1r 1190 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
223, 8lhpbase 37016 . . . . . 6 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2321, 22syl 17 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 ∈ (Base‘𝐾))
243, 6latmcl 17652 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃)) 𝑊) ∈ (Base‘𝐾))
2513, 20, 23, 24syl3anc 1363 . . . 4 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐹𝑃)) 𝑊) ∈ (Base‘𝐾))
26 simpl3l 1220 . . . . . 6 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → 𝑃𝐴)
27 simpl3r 1221 . . . . . 6 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → ¬ 𝑃 𝑊)
28 breq1 5061 . . . . . . . . . 10 (𝑞 = 𝑃 → (𝑞 𝑊𝑃 𝑊))
2928notbid 319 . . . . . . . . 9 (𝑞 = 𝑃 → (¬ 𝑞 𝑊 ↔ ¬ 𝑃 𝑊))
30 id 22 . . . . . . . . . . . 12 (𝑞 = 𝑃𝑞 = 𝑃)
31 fveq2 6664 . . . . . . . . . . . 12 (𝑞 = 𝑃 → (𝐹𝑞) = (𝐹𝑃))
3230, 31oveq12d 7163 . . . . . . . . . . 11 (𝑞 = 𝑃 → (𝑞 (𝐹𝑞)) = (𝑃 (𝐹𝑃)))
3332oveq1d 7160 . . . . . . . . . 10 (𝑞 = 𝑃 → ((𝑞 (𝐹𝑞)) 𝑊) = ((𝑃 (𝐹𝑃)) 𝑊))
3433eqeq2d 2832 . . . . . . . . 9 (𝑞 = 𝑃 → (𝑥 = ((𝑞 (𝐹𝑞)) 𝑊) ↔ 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
3529, 34imbi12d 346 . . . . . . . 8 (𝑞 = 𝑃 → ((¬ 𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) ↔ (¬ 𝑃 𝑊𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3635rspcv 3617 . . . . . . 7 (𝑃𝐴 → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → (¬ 𝑃 𝑊𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3736com23 86 . . . . . 6 (𝑃𝐴 → (¬ 𝑃 𝑊 → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3826, 27, 37sylc 65 . . . . 5 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
39 simp11 1195 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → (𝐾 ∈ Lat ∧ 𝑊𝐻))
40 simp12 1196 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝐹𝑇)
41 simp13l 1280 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝑃𝐴)
42 simp13r 1281 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ¬ 𝑃 𝑊)
43 simp3 1130 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝑞𝐴)
44 simp2 1129 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ¬ 𝑞 𝑊)
454, 5, 6, 7, 8, 9ltrnu 37139 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑞𝐴 ∧ ¬ 𝑞 𝑊)) → ((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊))
4639, 40, 41, 42, 43, 44, 45syl222anc 1378 . . . . . . . . . 10 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊))
47 eqeq2 2833 . . . . . . . . . . 11 (((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) ↔ 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
4847biimpd 230 . . . . . . . . . 10 (((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
4946, 48syl 17 . . . . . . . . 9 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
50493exp 1111 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (¬ 𝑞 𝑊 → (𝑞𝐴 → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))))
5150com24 95 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → (𝑞𝐴 → (¬ 𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))))
5251ralrimdv 3188 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → ∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
5352adantr 481 . . . . 5 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → ∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
5438, 53impbid 213 . . . 4 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) ↔ 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
5525, 54riota5 7132 . . 3 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))) = ((𝑃 (𝐹𝑃)) 𝑊))
5612, 55eqtrd 2856 . 2 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
572, 56syl3an1 1155 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1079   = wceq 1528  wcel 2105  wral 3138   class class class wbr 5058  cfv 6349  crio 7102  (class class class)co 7145  Basecbs 16473  lecple 16562  joincjn 17544  meetcmee 17545  Latclat 17645  Atomscatm 36281  HLchlt 36368  LHypclh 37002  LTrncltrn 37119  trLctrl 37176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-map 8398  df-lub 17574  df-glb 17575  df-join 17576  df-meet 17577  df-lat 17646  df-ats 36285  df-atl 36316  df-cvlat 36340  df-hlat 36369  df-lhyp 37006  df-laut 37007  df-ldil 37122  df-ltrn 37123  df-trl 37177
This theorem is referenced by:  trlcl  37182  trlcnv  37183  trljat1  37184  trljat2  37185  trlat  37187  trl0  37188  trlle  37202  trlval3  37205  trlval5  37207  cdlemd6  37221  cdlemf  37581  cdlemg4a  37626  cdlemg4b1  37627  cdlemg4b2  37628  cdlemg4  37635  cdlemg11b  37660  cdlemg13a  37669  cdlemg13  37670  cdlemg17a  37679  cdlemg17dN  37681  cdlemg17e  37683  cdlemg17f  37684  trlcoabs2N  37740  trlcolem  37744  cdlemg42  37747  cdlemg43  37748  cdlemi1  37836  cdlemk4  37852  cdlemk39  37934  dia2dimlem1  38082  dia2dimlem2  38083  dia2dimlem3  38084  cdlemm10N  38136  cdlemn2  38213  cdlemn10  38224  dihjatcclem3  38438
  Copyright terms: Public domain W3C validator