![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > trlco | Structured version Visualization version GIF version |
Description: The trace of a composition of translations is less than or equal to the join of their traces. Part of proof of Lemma G of [Crawley] p. 116, second paragraph on p. 117. (Contributed by NM, 2-Jun-2013.) |
Ref | Expression |
---|---|
trlco.l | ⊢ ≤ = (le‘𝐾) |
trlco.j | ⊢ ∨ = (join‘𝐾) |
trlco.h | ⊢ 𝐻 = (LHyp‘𝐾) |
trlco.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
trlco.r | ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
trlco | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺)) ≤ ((𝑅‘𝐹) ∨ (𝑅‘𝐺))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trlco.l | . . . 4 ⊢ ≤ = (le‘𝐾) | |
2 | eqid 2800 | . . . 4 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾) | |
3 | trlco.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
4 | 1, 2, 3 | lhpexnle 36026 | . . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ (Atoms‘𝐾) ¬ 𝑝 ≤ 𝑊) |
5 | 4 | 3ad2ant1 1164 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ∃𝑝 ∈ (Atoms‘𝐾) ¬ 𝑝 ≤ 𝑊) |
6 | simpl1 1243 | . . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
7 | simpl2 1245 | . . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝 ≤ 𝑊)) → 𝐹 ∈ 𝑇) | |
8 | simpl3 1247 | . . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝 ≤ 𝑊)) → 𝐺 ∈ 𝑇) | |
9 | simpr 478 | . . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝 ≤ 𝑊)) | |
10 | trlco.j | . . . 4 ⊢ ∨ = (join‘𝐾) | |
11 | trlco.t | . . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
12 | trlco.r | . . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) | |
13 | eqid 2800 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
14 | 1, 10, 3, 11, 12, 13, 2 | trlcolem 36746 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑅‘(𝐹 ∘ 𝐺)) ≤ ((𝑅‘𝐹) ∨ (𝑅‘𝐺))) |
15 | 6, 7, 8, 9, 14 | syl121anc 1495 | . 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑝 ∈ (Atoms‘𝐾) ∧ ¬ 𝑝 ≤ 𝑊)) → (𝑅‘(𝐹 ∘ 𝐺)) ≤ ((𝑅‘𝐹) ∨ (𝑅‘𝐺))) |
16 | 5, 15 | rexlimddv 3217 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ 𝐺)) ≤ ((𝑅‘𝐹) ∨ (𝑅‘𝐺))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ∃wrex 3091 class class class wbr 4844 ∘ ccom 5317 ‘cfv 6102 (class class class)co 6879 lecple 16273 joincjn 17258 meetcmee 17259 Atomscatm 35283 HLchlt 35370 LHypclh 36004 LTrncltrn 36121 trLctrl 36178 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2378 ax-ext 2778 ax-rep 4965 ax-sep 4976 ax-nul 4984 ax-pow 5036 ax-pr 5098 ax-un 7184 ax-riotaBAD 34973 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2592 df-eu 2610 df-clab 2787 df-cleq 2793 df-clel 2796 df-nfc 2931 df-ne 2973 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rmo 3098 df-rab 3099 df-v 3388 df-sbc 3635 df-csb 3730 df-dif 3773 df-un 3775 df-in 3777 df-ss 3784 df-nul 4117 df-if 4279 df-pw 4352 df-sn 4370 df-pr 4372 df-op 4376 df-uni 4630 df-iun 4713 df-iin 4714 df-br 4845 df-opab 4907 df-mpt 4924 df-id 5221 df-xp 5319 df-rel 5320 df-cnv 5321 df-co 5322 df-dm 5323 df-rn 5324 df-res 5325 df-ima 5326 df-iota 6065 df-fun 6104 df-fn 6105 df-f 6106 df-f1 6107 df-fo 6108 df-f1o 6109 df-fv 6110 df-riota 6840 df-ov 6882 df-oprab 6883 df-mpt2 6884 df-1st 7402 df-2nd 7403 df-undef 7638 df-map 8098 df-proset 17242 df-poset 17260 df-plt 17272 df-lub 17288 df-glb 17289 df-join 17290 df-meet 17291 df-p0 17353 df-p1 17354 df-lat 17360 df-clat 17422 df-oposet 35196 df-ol 35198 df-oml 35199 df-covers 35286 df-ats 35287 df-atl 35318 df-cvlat 35342 df-hlat 35371 df-llines 35518 df-lplanes 35519 df-lvols 35520 df-lines 35521 df-psubsp 35523 df-pmap 35524 df-padd 35816 df-lhyp 36008 df-laut 36009 df-ldil 36124 df-ltrn 36125 df-trl 36179 |
This theorem is referenced by: trlcone 36748 cdlemg46 36755 trljco 36760 tendopltp 36800 dialss 37066 diblss 37190 |
Copyright terms: Public domain | W3C validator |