Theorem trlcnv 40154

Description: The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013.)

Hypotheses

Ref	Expression
trlcnv.h	⊢ 𝐻 = (LHyp‘𝐾)
trlcnv.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlcnv.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

Assertion

Ref	Expression
trlcnv	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘◡𝐹) = (𝑅‘𝐹))

Proof of Theorem trlcnv

Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2729	. . . 4 ⊢ (le‘𝐾) = (le‘𝐾)
2		eqid 2729	. . . 4 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
3		trlcnv.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
4	1, 2, 3	lhpexnle 39995	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ (Atoms‘𝐾) ¬ 𝑝(le‘𝐾)𝑊)
5	4	adantr 480	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ∃𝑝 ∈ (Atoms‘𝐾) ¬ 𝑝(le‘𝐾)𝑊)
6		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		trlcnv.t	. . . . . . . . . 10 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
8	6, 3, 7	ltrn1o 40113	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
9	8	3adant3 1132	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾))
10		simp3l 1202	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → 𝑝 ∈ (Atoms‘𝐾))
11	6, 2	atbase 39277	. . . . . . . . 9 ⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ (Base‘𝐾))
12	10, 11	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → 𝑝 ∈ (Base‘𝐾))
13		f1ocnvfv1 7234	. . . . . . . 8 ⊢ ((𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ 𝑝 ∈ (Base‘𝐾)) → (◡𝐹‘(𝐹‘𝑝)) = 𝑝)
14	9, 12, 13	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (◡𝐹‘(𝐹‘𝑝)) = 𝑝)
15	14	oveq2d 7386	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝))) = ((𝐹‘𝑝)(join‘𝐾)𝑝))
16		simp1l 1198	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → 𝐾 ∈ HL)
17	1, 2, 3, 7	ltrnat 40129	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑝 ∈ (Atoms‘𝐾)) → (𝐹‘𝑝) ∈ (Atoms‘𝐾))
18	17	3adant3r 1182	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝐹‘𝑝) ∈ (Atoms‘𝐾))
19		eqid 2729	. . . . . . . 8 ⊢ (join‘𝐾) = (join‘𝐾)
20	19, 2	hlatjcom 39356	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ((𝐹‘𝑝)(join‘𝐾)𝑝) = (𝑝(join‘𝐾)(𝐹‘𝑝)))
21	16, 18, 10, 20	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((𝐹‘𝑝)(join‘𝐾)𝑝) = (𝑝(join‘𝐾)(𝐹‘𝑝)))
22	15, 21	eqtrd 2764	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝))) = (𝑝(join‘𝐾)(𝐹‘𝑝)))
23	22	oveq1d 7385	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝)))(meet‘𝐾)𝑊) = ((𝑝(join‘𝐾)(𝐹‘𝑝))(meet‘𝐾)𝑊))
24		simp1 1136	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
25	3, 7	ltrncnv 40135	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ◡𝐹 ∈ 𝑇)
26	25	3adant3 1132	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ◡𝐹 ∈ 𝑇)
27	1, 2, 3, 7	ltrnel 40128	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → ((𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (𝐹‘𝑝)(le‘𝐾)𝑊))
28		eqid 2729	. . . . . 6 ⊢ (meet‘𝐾) = (meet‘𝐾)
29		trlcnv.r	. . . . . 6 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
30	1, 19, 28, 2, 3, 7, 29	trlval2 40152	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ◡𝐹 ∈ 𝑇 ∧ ((𝐹‘𝑝) ∈ (Atoms‘𝐾) ∧ ¬ (𝐹‘𝑝)(le‘𝐾)𝑊)) → (𝑅‘◡𝐹) = (((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝)))(meet‘𝐾)𝑊))
31	24, 26, 27, 30	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑅‘◡𝐹) = (((𝐹‘𝑝)(join‘𝐾)(◡𝐹‘(𝐹‘𝑝)))(meet‘𝐾)𝑊))
32	1, 19, 28, 2, 3, 7, 29	trlval2 40152	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑅‘𝐹) = ((𝑝(join‘𝐾)(𝐹‘𝑝))(meet‘𝐾)𝑊))
33	23, 31, 32	3eqtr4d 2774	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑅‘◡𝐹) = (𝑅‘𝐹))
34	33	3expa 1118	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑅‘◡𝐹) = (𝑅‘𝐹))
35	5, 34	rexlimddv 3140	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘◡𝐹) = (𝑅‘𝐹))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∃wrex 3053   class class class wbr 5102  ^◡ccnv 5630  –1-1-onto→wf1o 6499  ‘cfv 6500  (class class class)co 7370  Basecbs 17157  lecple 17205  joincjn 18254  meetcmee 18255  Atomscatm 39251  HLchlt 39338  LHypclh 39973  LTrncltrn 40090  trLctrl 40147

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6453  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-map 8779  df-proset 18237  df-poset 18256  df-plt 18271  df-lub 18287  df-glb 18288  df-join 18289  df-meet 18290  df-p0 18366  df-p1 18367  df-lat 18375  df-clat 18442  df-oposet 39164  df-ol 39166  df-oml 39167  df-covers 39254  df-ats 39255  df-atl 39286  df-cvlat 39310  df-hlat 39339  df-lhyp 39977  df-laut 39978  df-ldil 40093  df-ltrn 40094  df-trl 40148

This theorem is referenced by:  trlcocnv  40709  trlcoat  40712  trlcocnvat  40713  trlcone  40717  cdlemg46  40724  tendoicl  40785  cdlemh1  40804  cdlemh2  40805  cdlemh  40806  cdlemk3  40822  cdlemk12  40839  cdlemk12u  40861  cdlemkfid1N  40910  cdlemkid1  40911  cdlemkid2  40913  cdlemk45  40936