Theorem idltrn 41300

Description: The identity function is a lattice translation. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 18-May-2012.)

Hypotheses

Ref	Expression
idltrn.b	⊢ 𝐵 = (Base‘𝐾)
idltrn.h	⊢ 𝐻 = (LHyp‘𝐾)
idltrn.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)

Assertion

Ref	Expression
idltrn	⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇)

Proof of Theorem idltrn

Dummy variables 𝑞 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		idltrn.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		idltrn.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
3		eqid 2760	. . 3 ⊢ ((LDil‘𝐾)‘𝑊) = ((LDil‘𝐾)‘𝑊)
4	1, 2, 3	idldil 41264	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ ((LDil‘𝐾)‘𝑊))
5		simpll 779	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
6		simplrr 790	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑞 ∈ (Atoms‘𝐾))
7		simprr 785	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑞(le‘𝐾)𝑊)
8		eqid 2760	. . . . . . 7 ⊢ (le‘𝐾) = (le‘𝐾)
9		eqid 2760	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		eqid 2760	. . . . . . 7 ⊢ (0.‘𝐾) = (0.‘𝐾)
11		eqid 2760	. . . . . . 7 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
12	8, 9, 10, 11, 2	lhpmat 41180	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(meet‘𝐾)𝑊) = (0.‘𝐾))
13	5, 6, 7, 12	syl12anc 850	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(meet‘𝐾)𝑊) = (0.‘𝐾))
14	1, 11	atbase 40439	. . . . . . . . 9 ⊢ (𝑞 ∈ (Atoms‘𝐾) → 𝑞 ∈ 𝐵)
15		fvresi 7178	. . . . . . . . 9 ⊢ (𝑞 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑞) = 𝑞)
16	6, 14, 15	3syl 19	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (( I ↾ 𝐵)‘𝑞) = 𝑞)
17	16	oveq2d 7436	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞)) = (𝑞(join‘𝐾)𝑞))
18		simplll 787	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐾 ∈ HL)
19		eqid 2760	. . . . . . . . 9 ⊢ (join‘𝐾) = (join‘𝐾)
20	19, 11	hlatjidm 40519	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑞 ∈ (Atoms‘𝐾)) → (𝑞(join‘𝐾)𝑞) = 𝑞)
21	18, 6, 20	syl2anc 596	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(join‘𝐾)𝑞) = 𝑞)
22	17, 21	eqtrd 2795	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞)) = 𝑞)
23	22	oveq1d 7435	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊) = (𝑞(meet‘𝐾)𝑊))
24		simplrl 789	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑝 ∈ (Atoms‘𝐾))
25	1, 11	atbase 40439	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ 𝐵)
26		fvresi 7178	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑝) = 𝑝)
27	24, 25, 26	3syl 19	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (( I ↾ 𝐵)‘𝑝) = 𝑝)
28	27	oveq2d 7436	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝)) = (𝑝(join‘𝐾)𝑝))
29	19, 11	hlatjidm 40519	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atoms‘𝐾)) → (𝑝(join‘𝐾)𝑝) = 𝑝)
30	18, 24, 29	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝(join‘𝐾)𝑝) = 𝑝)
31	28, 30	eqtrd 2795	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝)) = 𝑝)
32	31	oveq1d 7435	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = (𝑝(meet‘𝐾)𝑊))
33		simprl 783	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑝(le‘𝐾)𝑊)
34	8, 9, 10, 11, 2	lhpmat 41180	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑝(meet‘𝐾)𝑊) = (0.‘𝐾))
35	5, 24, 33, 34	syl12anc 850	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝(meet‘𝐾)𝑊) = (0.‘𝐾))
36	32, 35	eqtrd 2795	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = (0.‘𝐾))
37	13, 23, 36	3eqtr4rd 2806	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊))
38	37	ex 418	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) → ((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊)))
39	38	ralrimivva 3205	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊)))
40		idltrn.t	. . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
41	8, 19, 9, 11, 2, 3, 40	isltrn 41269	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (( I ↾ 𝐵) ∈ 𝑇 ↔ (( I ↾ 𝐵) ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊)))))
42	4, 39, 41	mpbir2and 726	1 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076   class class class wbr 5102   I cid 5544   ↾ cres 5652  ‘cfv 6538  (class class class)co 7420  Basecbs 17392  lecple 17440  joincjn 18490  meetcmee 18491  0.cp0 18600  Atomscatm 40413  HLchlt 40500  LHypclh 41134  LDilcldil 41250  LTrncltrn 41251

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-map 8852  df-proset 18473  df-poset 18492  df-plt 18507  df-lub 18523  df-glb 18524  df-join 18525  df-meet 18526  df-p0 18602  df-lat 18611  df-covers 40416  df-ats 40417  df-atl 40448  df-cvlat 40472  df-hlat 40501  df-lhyp 41138  df-laut 41139  df-ldil 41254  df-ltrn 41255

This theorem is used by:  trlid0  41326  tgrpgrplem  41899  tendoid  41923  tendo0cl  41940  cdlemkid2  42074  cdlemkid3N  42083  cdlemkid4  42084  cdlemkid5  42085  cdlemk35s-id  42088  dva0g  42177  dian0  42189  dia0  42202  dvhgrp  42257  dvh0g  42261  dvheveccl  42262  dvhopN  42266  dihmeetlem4preN  42456