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 40165
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 39364 . . 3 (𝐾 ∈ HL → 𝐾 ∈ Lat)
21anim1i 615 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝐾 ∈ Lat ∧ 𝑊𝐻))
3 eqid 2737 . . . . 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 40164 . . . 4 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) = (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
12113adant3 1133 . . 3 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
13 simp1l 1198 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
14 simp3l 1202 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
153, 7atbase 39290 . . . . . . 7 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1614, 15syl 17 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 ∈ (Base‘𝐾))
173, 8, 9ltrncl 40127 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇𝑃 ∈ (Base‘𝐾)) → (𝐹𝑃) ∈ (Base‘𝐾))
1816, 17syld3an3 1411 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝑃) ∈ (Base‘𝐾))
193, 5latjcl 18484 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐹𝑃) ∈ (Base‘𝐾)) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
2013, 16, 18, 19syl3anc 1373 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾))
21 simp1r 1199 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
223, 8lhpbase 40000 . . . . . 6 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2321, 22syl 17 . . . . 5 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 ∈ (Base‘𝐾))
243, 6latmcl 18485 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 (𝐹𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 (𝐹𝑃)) 𝑊) ∈ (Base‘𝐾))
2513, 20, 23, 24syl3anc 1373 . . . 4 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐹𝑃)) 𝑊) ∈ (Base‘𝐾))
26 simpl3l 1229 . . . . . 6 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → 𝑃𝐴)
27 simpl3r 1230 . . . . . 6 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → ¬ 𝑃 𝑊)
28 breq1 5146 . . . . . . . . . 10 (𝑞 = 𝑃 → (𝑞 𝑊𝑃 𝑊))
2928notbid 318 . . . . . . . . 9 (𝑞 = 𝑃 → (¬ 𝑞 𝑊 ↔ ¬ 𝑃 𝑊))
30 id 22 . . . . . . . . . . . 12 (𝑞 = 𝑃𝑞 = 𝑃)
31 fveq2 6906 . . . . . . . . . . . 12 (𝑞 = 𝑃 → (𝐹𝑞) = (𝐹𝑃))
3230, 31oveq12d 7449 . . . . . . . . . . 11 (𝑞 = 𝑃 → (𝑞 (𝐹𝑞)) = (𝑃 (𝐹𝑃)))
3332oveq1d 7446 . . . . . . . . . 10 (𝑞 = 𝑃 → ((𝑞 (𝐹𝑞)) 𝑊) = ((𝑃 (𝐹𝑃)) 𝑊))
3433eqeq2d 2748 . . . . . . . . 9 (𝑞 = 𝑃 → (𝑥 = ((𝑞 (𝐹𝑞)) 𝑊) ↔ 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
3529, 34imbi12d 344 . . . . . . . 8 (𝑞 = 𝑃 → ((¬ 𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) ↔ (¬ 𝑃 𝑊𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3635rspcv 3618 . . . . . . 7 (𝑃𝐴 → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → (¬ 𝑃 𝑊𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3736com23 86 . . . . . 6 (𝑃𝐴 → (¬ 𝑃 𝑊 → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊))))
3826, 27, 37sylc 65 . . . . 5 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) → 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
39 simp11 1204 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → (𝐾 ∈ Lat ∧ 𝑊𝐻))
40 simp12 1205 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝐹𝑇)
41 simp13l 1289 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝑃𝐴)
42 simp13r 1290 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ¬ 𝑃 𝑊)
43 simp3 1139 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → 𝑞𝐴)
44 simp2 1138 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ¬ 𝑞 𝑊)
454, 5, 6, 7, 8, 9ltrnu 40123 . . . . . . . . . . 11 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑞𝐴 ∧ ¬ 𝑞 𝑊)) → ((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊))
4639, 40, 41, 42, 43, 44, 45syl222anc 1388 . . . . . . . . . 10 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → ((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊))
47 eqeq2 2749 . . . . . . . . . . 11 (((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) ↔ 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
4847biimpd 229 . . . . . . . . . 10 (((𝑃 (𝐹𝑃)) 𝑊) = ((𝑞 (𝐹𝑞)) 𝑊) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
4946, 48syl 17 . . . . . . . . 9 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ ¬ 𝑞 𝑊𝑞𝐴) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))
50493exp 1120 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (¬ 𝑞 𝑊 → (𝑞𝐴 → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → 𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))))
5150com24 95 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → (𝑞𝐴 → (¬ 𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)))))
5251ralrimdv 3152 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → ∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
5352adantr 480 . . . . 5 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = ((𝑃 (𝐹𝑃)) 𝑊) → ∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))))
5438, 53impbid 212 . . . 4 ((((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊)) ↔ 𝑥 = ((𝑃 (𝐹𝑃)) 𝑊)))
5525, 54riota5 7417 . . 3 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑥 ∈ (Base‘𝐾)∀𝑞𝐴𝑞 𝑊𝑥 = ((𝑞 (𝐹𝑞)) 𝑊))) = ((𝑃 (𝐹𝑃)) 𝑊))
5612, 55eqtrd 2777 . 2 (((𝐾 ∈ Lat ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
572, 56syl3an1 1164 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃)) 𝑊))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061   class class class wbr 5143  cfv 6561  crio 7387  (class class class)co 7431  Basecbs 17247  lecple 17304  joincjn 18357  meetcmee 18358  Latclat 18476  Atomscatm 39264  HLchlt 39351  LHypclh 39986  LTrncltrn 40103  trLctrl 40160
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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868  df-lub 18391  df-glb 18392  df-join 18393  df-meet 18394  df-lat 18477  df-ats 39268  df-atl 39299  df-cvlat 39323  df-hlat 39352  df-lhyp 39990  df-laut 39991  df-ldil 40106  df-ltrn 40107  df-trl 40161
This theorem is referenced by:  trlcl  40166  trlcnv  40167  trljat1  40168  trljat2  40169  trlat  40171  trl0  40172  trlle  40186  trlval3  40189  trlval5  40191  cdlemd6  40205  cdlemf  40565  cdlemg4a  40610  cdlemg4b1  40611  cdlemg4b2  40612  cdlemg4  40619  cdlemg11b  40644  cdlemg13a  40653  cdlemg13  40654  cdlemg17a  40663  cdlemg17dN  40665  cdlemg17e  40667  cdlemg17f  40668  trlcoabs2N  40724  trlcolem  40728  cdlemg42  40731  cdlemg43  40732  cdlemi1  40820  cdlemk4  40836  cdlemk39  40918  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  cdlemm10N  41120  cdlemn2  41197  cdlemn10  41208  dihjatcclem3  41422
  Copyright terms: Public domain W3C validator