Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > dihord2cN | Structured version Visualization version GIF version |
Description: Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: needed? shorten other proof with it? (Contributed by NM, 3-Mar-2014.) (New usage is discouraged.) |
Ref | Expression |
---|---|
dihjust.b | ⊢ 𝐵 = (Base‘𝐾) |
dihjust.l | ⊢ ≤ = (le‘𝐾) |
dihjust.j | ⊢ ∨ = (join‘𝐾) |
dihjust.m | ⊢ ∧ = (meet‘𝐾) |
dihjust.a | ⊢ 𝐴 = (Atoms‘𝐾) |
dihjust.h | ⊢ 𝐻 = (LHyp‘𝐾) |
dihjust.i | ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
dihjust.J | ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊) |
dihjust.u | ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
dihjust.s | ⊢ ⊕ = (LSSum‘𝑈) |
dihord2c.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
dihord2c.r | ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
dihord2c.o | ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
Ref | Expression |
---|---|
dihord2cN | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 〈𝑓, 𝑂〉 ∈ (𝐼‘(𝑋 ∧ 𝑊))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 1137 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) | |
2 | eqidd 2741 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑂 = 𝑂) | |
3 | simp1 1135 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
4 | simp1l 1196 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝐾 ∈ HL) | |
5 | 4 | hllatd 37372 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝐾 ∈ Lat) |
6 | simp2 1136 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑋 ∈ 𝐵) | |
7 | simp1r 1197 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑊 ∈ 𝐻) | |
8 | dihjust.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐾) | |
9 | dihjust.h | . . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾) | |
10 | 8, 9 | lhpbase 38006 | . . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
11 | 7, 10 | syl 17 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 𝑊 ∈ 𝐵) |
12 | dihjust.m | . . . . 5 ⊢ ∧ = (meet‘𝐾) | |
13 | 8, 12 | latmcl 18154 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
14 | 5, 6, 11, 13 | syl3anc 1370 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑋 ∧ 𝑊) ∈ 𝐵) |
15 | dihjust.l | . . . . 5 ⊢ ≤ = (le‘𝐾) | |
16 | 8, 15, 12 | latmle2 18179 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
17 | 5, 6, 11, 16 | syl3anc 1370 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (𝑋 ∧ 𝑊) ≤ 𝑊) |
18 | dihord2c.t | . . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
19 | dihord2c.r | . . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) | |
20 | dihord2c.o | . . . 4 ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) | |
21 | dihjust.i | . . . 4 ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) | |
22 | 8, 15, 9, 18, 19, 20, 21 | dibopelval3 39156 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (〈𝑓, 𝑂〉 ∈ (𝐼‘(𝑋 ∧ 𝑊)) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑂 = 𝑂))) |
23 | 3, 14, 17, 22 | syl12anc 834 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → (〈𝑓, 𝑂〉 ∈ (𝐼‘(𝑋 ∧ 𝑊)) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑂 = 𝑂))) |
24 | 1, 2, 23 | mpbir2and 710 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ (𝑋 ∧ 𝑊))) → 〈𝑓, 𝑂〉 ∈ (𝐼‘(𝑋 ∧ 𝑊))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1542 ∈ wcel 2110 〈cop 4573 class class class wbr 5079 ↦ cmpt 5162 I cid 5488 ↾ cres 5591 ‘cfv 6431 (class class class)co 7269 Basecbs 16908 lecple 16965 joincjn 18025 meetcmee 18026 Latclat 18145 LSSumclsm 19235 Atomscatm 37271 HLchlt 37358 LHypclh 37992 LTrncltrn 38109 trLctrl 38166 DVecHcdvh 39086 DIsoBcdib 39146 DIsoCcdic 39180 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-rep 5214 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7580 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-ral 3071 df-rex 3072 df-reu 3073 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4846 df-iun 4932 df-br 5080 df-opab 5142 df-mpt 5163 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6389 df-fun 6433 df-fn 6434 df-f 6435 df-f1 6436 df-fo 6437 df-f1o 6438 df-fv 6439 df-riota 7226 df-ov 7272 df-oprab 7273 df-lub 18060 df-glb 18061 df-join 18062 df-meet 18063 df-lat 18146 df-atl 37306 df-cvlat 37330 df-hlat 37359 df-lhyp 37996 df-disoa 39037 df-dib 39147 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |