Theorem ltrnel 40141

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 1202	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ 𝐴)
2		eqid 2737	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		ltrnel.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39290	. . . . 5 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
5	4	adantr 480	. . . 4 ⊢ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) → 𝑃 ∈ (Base‘𝐾))
6		ltrnel.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
7		ltrnel.t	. . . . 5 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
8	2, 3, 6, 7	ltrnatb 40139	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴))
9	5, 8	syl3an3 1166	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ↔ (𝐹‘𝑃) ∈ 𝐴))
10	1, 9	mpbid 232	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑃) ∈ 𝐴)
11		simp3r 1203	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ¬ 𝑃 ≤ 𝑊)
12		simp1 1137	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
13		simp2 1138	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐹 ∈ 𝑇)
14	1, 4	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑃 ∈ (Base‘𝐾))
15		simp1r 1199	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ 𝐻)
16	2, 6	lhpbase 40000	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
17	15, 16	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ∈ (Base‘𝐾))
18		ltrnel.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
19	2, 18, 6, 7	ltrnle 40131	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (𝑃 ≤ 𝑊 ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑊)))
20	12, 13, 14, 17, 19	syl112anc 1376	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ≤ 𝑊 ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑊)))
21		simp1l 1198	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ HL)
22	21	hllatd 39365	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝐾 ∈ Lat)
23	2, 18	latref 18486	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑊 ∈ (Base‘𝐾)) → 𝑊 ≤ 𝑊)
24	22, 17, 23	syl2anc 584	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → 𝑊 ≤ 𝑊)
25	2, 18, 6, 7	ltrnval1 40136	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑊 ∈ (Base‘𝐾) ∧ 𝑊 ≤ 𝑊)) → (𝐹‘𝑊) = 𝑊)
26	12, 13, 17, 24, 25	syl112anc 1376	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝐹‘𝑊) = 𝑊)
27	26	breq2d 5155	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ≤ (𝐹‘𝑊) ↔ (𝐹‘𝑃) ≤ 𝑊))
28	20, 27	bitrd 279	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ≤ 𝑊 ↔ (𝐹‘𝑃) ≤ 𝑊))
29	11, 28	mtbid 324	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ¬ (𝐹‘𝑃) ≤ 𝑊)
30	10, 29	jca 511	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   class class class wbr 5143  ‘cfv 6561  Basecbs 17247  lecple 17304  Latclat 18476  Atomscatm 39264  HLchlt 39351  LHypclh 39986  LTrncltrn 40103

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-proset 18340  df-poset 18359  df-plt 18375  df-glb 18392  df-p0 18470  df-lat 18477  df-oposet 39177  df-ol 39179  df-oml 39180  df-covers 39267  df-ats 39268  df-atl 39299  df-cvlat 39323  df-hlat 39352  df-lhyp 39990  df-laut 39991  df-ldil 40106  df-ltrn 40107

This theorem is referenced by:  ltrncoelN  40145  ltrnmw  40153  trlcnv  40167  trljat2  40169  cdlemc3  40195  cdlemc5  40197  cdlemd9  40208  cdlemeiota  40587  cdlemg1cex  40590  cdlemg2l  40605  cdlemg2m  40606  cdlemg7fvbwN  40609  cdlemg4a  40610  cdlemg4b1  40611  cdlemg4b2  40612  cdlemg4d  40615  cdlemg4e  40616  cdlemg4  40619  cdlemg6e  40624  cdlemg7fvN  40626  cdlemg8b  40630  cdlemg8c  40631  cdlemg10bALTN  40638  cdlemg10a  40642  cdlemg12d  40648  cdlemg13a  40653  cdlemg13  40654  cdlemg14f  40655  cdlemg17b  40664  cdlemg17f  40668  cdlemg17i  40671  trlcoabs  40723  trlcoabs2N  40724  trlcolem  40728  cdlemg43  40732  cdlemg44b  40734  cdlemi2  40821  cdlemi  40822  cdlemk2  40834  cdlemk3  40835  cdlemk4  40836  cdlemk8  40840  cdlemk9  40841  cdlemk9bN  40842  cdlemki  40843  cdlemksv2  40849  cdlemk12  40852  cdlemkoatnle  40853  cdlemk12u  40874  cdlemkfid1N  40923  cdlemk47  40951  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  dia2dimlem6  41071  cdlemm10N  41120  dih1dimatlem0  41330  dih1dimatlem  41331