Theorem idltrn 37762

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 2759	. . 3 ⊢ ((LDil‘𝐾)‘𝑊) = ((LDil‘𝐾)‘𝑊)
4	1, 2, 3	idldil 37726	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ ((LDil‘𝐾)‘𝑊))
5		simpll 766	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
6		simplrr 777	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑞 ∈ (Atoms‘𝐾))
7		simprr 772	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑞(le‘𝐾)𝑊)
8		eqid 2759	. . . . . . 7 ⊢ (le‘𝐾) = (le‘𝐾)
9		eqid 2759	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		eqid 2759	. . . . . . 7 ⊢ (0.‘𝐾) = (0.‘𝐾)
11		eqid 2759	. . . . . . 7 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
12	8, 9, 10, 11, 2	lhpmat 37642	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑞 ∈ (Atoms‘𝐾) ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(meet‘𝐾)𝑊) = (0.‘𝐾))
13	5, 6, 7, 12	syl12anc 835	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(meet‘𝐾)𝑊) = (0.‘𝐾))
14	1, 11	atbase 36901	. . . . . . . . 9 ⊢ (𝑞 ∈ (Atoms‘𝐾) → 𝑞 ∈ 𝐵)
15		fvresi 6933	. . . . . . . . 9 ⊢ (𝑞 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑞) = 𝑞)
16	6, 14, 15	3syl 18	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (( I ↾ 𝐵)‘𝑞) = 𝑞)
17	16	oveq2d 7173	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞)) = (𝑞(join‘𝐾)𝑞))
18		simplll 774	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝐾 ∈ HL)
19		eqid 2759	. . . . . . . . 9 ⊢ (join‘𝐾) = (join‘𝐾)
20	19, 11	hlatjidm 36981	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑞 ∈ (Atoms‘𝐾)) → (𝑞(join‘𝐾)𝑞) = 𝑞)
21	18, 6, 20	syl2anc 587	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(join‘𝐾)𝑞) = 𝑞)
22	17, 21	eqtrd 2794	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞)) = 𝑞)
23	22	oveq1d 7172	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊) = (𝑞(meet‘𝐾)𝑊))
24		simplrl 776	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → 𝑝 ∈ (Atoms‘𝐾))
25	1, 11	atbase 36901	. . . . . . . . . 10 ⊢ (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ 𝐵)
26		fvresi 6933	. . . . . . . . . 10 ⊢ (𝑝 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑝) = 𝑝)
27	24, 25, 26	3syl 18	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (( I ↾ 𝐵)‘𝑝) = 𝑝)
28	27	oveq2d 7173	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝)) = (𝑝(join‘𝐾)𝑝))
29	19, 11	hlatjidm 36981	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atoms‘𝐾)) → (𝑝(join‘𝐾)𝑝) = 𝑝)
30	18, 24, 29	syl2anc 587	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝(join‘𝐾)𝑝) = 𝑝)
31	28, 30	eqtrd 2794	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝)) = 𝑝)
32	31	oveq1d 7172	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = (𝑝(meet‘𝐾)𝑊))
33		simprl 770	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ¬ 𝑝(le‘𝐾)𝑊)
34	8, 9, 10, 11, 2	lhpmat 37642	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝(le‘𝐾)𝑊)) → (𝑝(meet‘𝐾)𝑊) = (0.‘𝐾))
35	5, 24, 33, 34	syl12anc 835	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → (𝑝(meet‘𝐾)𝑊) = (0.‘𝐾))
36	32, 35	eqtrd 2794	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = (0.‘𝐾))
37	13, 23, 36	3eqtr4rd 2805	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) ∧ (¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊)) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊))
38	37	ex 416	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ 𝑞 ∈ (Atoms‘𝐾))) → ((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊)))
39	38	ralrimivva 3121	. 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 37731	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (( I ↾ 𝐵) ∈ 𝑇 ↔ (( I ↾ 𝐵) ∈ ((LDil‘𝐾)‘𝑊) ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)((¬ 𝑝(le‘𝐾)𝑊 ∧ ¬ 𝑞(le‘𝐾)𝑊) → ((𝑝(join‘𝐾)(( I ↾ 𝐵)‘𝑝))(meet‘𝐾)𝑊) = ((𝑞(join‘𝐾)(( I ↾ 𝐵)‘𝑞))(meet‘𝐾)𝑊)))))
42	4, 39, 41	mpbir2and 712	1 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1539   ∈ wcel 2112  ∀wral 3071   class class class wbr 5037   I cid 5434   ↾ cres 5531  ‘cfv 6341  (class class class)co 7157  Basecbs 16556  lecple 16645  joincjn 17635  meetcmee 17636  0.cp0 17728  Atomscatm 36875  HLchlt 36962  LHypclh 37596  LDilcldil 37712  LTrncltrn 37713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-map 8425  df-proset 17619  df-poset 17637  df-plt 17649  df-lub 17665  df-glb 17666  df-join 17667  df-meet 17668  df-p0 17730  df-lat 17737  df-covers 36878  df-ats 36879  df-atl 36910  df-cvlat 36934  df-hlat 36963  df-lhyp 37600  df-laut 37601  df-ldil 37716  df-ltrn 37717

This theorem is referenced by:  trlid0  37788  tgrpgrplem  38361  tendoid  38385  tendo0cl  38402  cdlemkid2  38536  cdlemkid3N  38545  cdlemkid4  38546  cdlemkid5  38547  cdlemk35s-id  38550  dva0g  38639  dian0  38651  dia0  38664  dvhgrp  38719  dvh0g  38723  dvheveccl  38724  dvhopN  38728  dihmeetlem4preN  38918