![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ltrniotacl | Structured version Visualization version GIF version |
Description: Version of cdleme50ltrn 39514 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 17-Apr-2013.) |
Ref | Expression |
---|---|
ltrniotaval.l | β’ β€ = (leβπΎ) |
ltrniotaval.a | β’ π΄ = (AtomsβπΎ) |
ltrniotaval.h | β’ π» = (LHypβπΎ) |
ltrniotaval.t | β’ π = ((LTrnβπΎ)βπ) |
ltrniotaval.f | β’ πΉ = (β©π β π (πβπ) = π) |
Ref | Expression |
---|---|
ltrniotacl | β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2732 | . 2 β’ (BaseβπΎ) = (BaseβπΎ) | |
2 | ltrniotaval.l | . 2 β’ β€ = (leβπΎ) | |
3 | eqid 2732 | . 2 β’ (joinβπΎ) = (joinβπΎ) | |
4 | eqid 2732 | . 2 β’ (meetβπΎ) = (meetβπΎ) | |
5 | ltrniotaval.a | . 2 β’ π΄ = (AtomsβπΎ) | |
6 | ltrniotaval.h | . 2 β’ π» = (LHypβπΎ) | |
7 | eqid 2732 | . 2 β’ ((π(joinβπΎ)π)(meetβπΎ)π) = ((π(joinβπΎ)π)(meetβπΎ)π) | |
8 | eqid 2732 | . 2 β’ ((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))) = ((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))) | |
9 | eqid 2732 | . 2 β’ ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))) = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))) | |
10 | eqid 2732 | . 2 β’ (π₯ β (BaseβπΎ) β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β (BaseβπΎ)βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β (BaseβπΎ)βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯)) = (π₯ β (BaseβπΎ) β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β (BaseβπΎ)βπ β π΄ ((Β¬ π β€ π β§ (π (joinβπΎ)(π₯(meetβπΎ)π)) = π₯) β π§ = (if(π β€ (π(joinβπΎ)π), (β©π¦ β (BaseβπΎ)βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π(joinβπΎ)π)) β π¦ = ((π(joinβπΎ)π)(meetβπΎ)(((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π)))(joinβπΎ)((π (joinβπΎ)π‘)(meetβπΎ)π))))), β¦π / π‘β¦((π‘(joinβπΎ)((π(joinβπΎ)π)(meetβπΎ)π))(meetβπΎ)(π(joinβπΎ)((π(joinβπΎ)π‘)(meetβπΎ)π))))(joinβπΎ)(π₯(meetβπΎ)π)))), π₯)) | |
11 | ltrniotaval.t | . 2 β’ π = ((LTrnβπΎ)βπ) | |
12 | ltrniotaval.f | . 2 β’ πΉ = (β©π β π (πβπ) = π) | |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | cdlemg1ltrnlem 39531 | 1 β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
Colors of variables: wff setvar class |
Syntax hints: Β¬ wn 3 β wi 4 β§ wa 396 β§ w3a 1087 = wceq 1541 β wcel 2106 β wne 2940 βwral 3061 β¦csb 3893 ifcif 4528 class class class wbr 5148 β¦ cmpt 5231 βcfv 6543 β©crio 7366 (class class class)co 7411 Basecbs 17146 lecple 17206 joincjn 18266 meetcmee 18267 Atomscatm 38219 HLchlt 38306 LHypclh 38941 LTrncltrn 39058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-riotaBAD 37909 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7977 df-2nd 7978 df-undef 8260 df-map 8824 df-proset 18250 df-poset 18268 df-plt 18285 df-lub 18301 df-glb 18302 df-join 18303 df-meet 18304 df-p0 18380 df-p1 18381 df-lat 18387 df-clat 18454 df-oposet 38132 df-ol 38134 df-oml 38135 df-covers 38222 df-ats 38223 df-atl 38254 df-cvlat 38278 df-hlat 38307 df-llines 38455 df-lplanes 38456 df-lvols 38457 df-lines 38458 df-psubsp 38460 df-pmap 38461 df-padd 38753 df-lhyp 38945 df-laut 38946 df-ldil 39061 df-ltrn 39062 df-trl 39116 |
This theorem is referenced by: ltrniotacnvval 39539 ltrniotaidvalN 39540 ltrniotavalbN 39541 cdlemg1ci2 39543 cdlemki 39798 cdlemkj 39820 cdlemm10N 40075 dicssdvh 40143 dicvaddcl 40147 dicvscacl 40148 dicn0 40149 diclspsn 40151 cdlemn2 40152 cdlemn2a 40153 cdlemn3 40154 cdlemn4 40155 cdlemn4a 40156 cdlemn6 40159 cdlemn8 40161 cdlemn9 40162 cdlemn11a 40164 dihordlem7b 40172 dihopelvalcpre 40205 dih1 40243 dihmeetlem1N 40247 dihglblem5apreN 40248 dihglbcpreN 40257 dihmeetlem4preN 40263 dihmeetlem13N 40276 dih1dimatlem0 40285 dihatlat 40291 dihatexv 40295 dihjatcclem3 40377 dihjatcclem4 40378 |
Copyright terms: Public domain | W3C validator |