Theorem ltrnel 40760

Description: The lattice translation of an atom not under the fiducial co-atom is also an atom not under the fiducial co-atom. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 22-May-2012.)

Hypotheses

Ref	Expression
ltrnel.l	⊢ ≤ = (le‘𝐾)
ltrnel.a	⊢ 𝐴 = (Atoms‘𝐾)
ltrnel.h	⊢ 𝐻 = (LHyp‘𝐾)
ltrnel.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)

Assertion

Ref	Expression
ltrnel	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))

Proof of Theorem ltrnel

Step	Hyp	Ref	Expression
1		simp3l 1215	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
2		eqid 2762	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		ltrnel.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39910	. . . . 5 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
5	4	adantr 484	. . . 4 ⊢ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) → 𝑃 ∈ (Base‘𝐾))
6		ltrnel.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
7		ltrnel.t	. . . . 5 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
8	2, 3, 6, 7	ltrnatb 40758	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴))
9	5, 8	syl3an3 1178	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴))
10	1, 9	mpbid 234	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐴)
11		simp3r 1216	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ¬ 𝑃 ≤ 𝑊)
12		simp1 1149	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
13		simp2 1150	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
14	1, 4	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ (Base‘𝐾))
15		simp1r 1212	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
16	2, 6	lhpbase 40619	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
17	15, 16	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
18		ltrnel.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
19	2, 18, 6, 7	ltrnle 40750	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (𝑃 ≤ 𝑊 ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑊)))
20	12, 13, 14, 17, 19	syl112anc 1393	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ≤ 𝑊 ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑊)))
21		simp1l 1211	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
22	21	hllatd 39985	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
23	2, 18	latref 18473	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑊 ∈ (Base‘𝐾)) → 𝑊 ≤ 𝑊)
24	22, 17, 23	syl2anc 593	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ≤ 𝑊)
25	2, 18, 6, 7	ltrnval1 40755	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑊 ∈ (Base‘𝐾) ∧ 𝑊 ≤ 𝑊)) → (𝐹‘𝑊) = 𝑊)
26	12, 13, 17, 24, 25	syl112anc 1393	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑊) = 𝑊)
27	26	breq2d 5112	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ≤ (𝐹‘𝑊) ↔ (𝐹‘𝑃) ≤ 𝑊))
28	20, 27	bitrd 281	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ≤ 𝑊 ↔ (𝐹‘𝑃) ≤ 𝑊))
29	11, 28	mtbid 326	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ¬ (𝐹‘𝑃) ≤ 𝑊)
30	10, 29	jca 519	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142   class class class wbr 5100  ‘cfv 6521  Basecbs 17245  lecple 17293  Latclat 18463  Atomscatm 39884  HLchlt 39971  LHypclh 40605  LTrncltrn 40722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-map 8810  df-proset 18326  df-poset 18345  df-plt 18360  df-glb 18377  df-p0 18455  df-lat 18464  df-oposet 39797  df-ol 39799  df-oml 39800  df-covers 39887  df-ats 39888  df-atl 39919  df-cvlat 39943  df-hlat 39972  df-lhyp 40609  df-laut 40610  df-ldil 40725  df-ltrn 40726

This theorem is referenced by:  ltrncoelN  40764  ltrnmw  40772  trlcnv  40786  trljat2  40788  cdlemc3  40814  cdlemc5  40816  cdlemd9  40827  cdlemeiota  41206  cdlemg1cex  41209  cdlemg2l  41224  cdlemg2m  41225  cdlemg7fvbwN  41228  cdlemg4a  41229  cdlemg4b1  41230  cdlemg4b2  41231  cdlemg4d  41234  cdlemg4e  41235  cdlemg4  41238  cdlemg6e  41243  cdlemg7fvN  41245  cdlemg8b  41249  cdlemg8c  41250  cdlemg10bALTN  41257  cdlemg10a  41261  cdlemg12d  41267  cdlemg13a  41272  cdlemg13  41273  cdlemg14f  41274  cdlemg17b  41283  cdlemg17f  41287  cdlemg17i  41290  trlcoabs  41342  trlcoabs2N  41343  trlcolem  41347  cdlemg43  41351  cdlemg44b  41353  cdlemi2  41440  cdlemi  41441  cdlemk2  41453  cdlemk3  41454  cdlemk4  41455  cdlemk8  41459  cdlemk9  41460  cdlemk9bN  41461  cdlemki  41462  cdlemksv2  41468  cdlemk12  41471  cdlemkoatnle  41472  cdlemk12u  41493  cdlemkfid1N  41542  cdlemk47  41570  dia2dimlem1  41685  dia2dimlem2  41686  dia2dimlem3  41687  dia2dimlem6  41690  cdlemm10N  41739  dih1dimatlem0  41949  dih1dimatlem  41950