cdlemefs31fv1 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemefs31fv1		Structured version Visualization version GIF version

Theorem cdlemefs31fv1 40543

Description: Value of (𝐹‘𝑅) when 𝑅 ≤ (𝑃 ∨ 𝑄). TODO This may be useful for shortening others that now use riotasv 39078 3d . TODO: FIX COMMENT. ***END OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW***

       "cdleme3xsn1aw" decreased using "cdlemefs32sn1aw"
       "cdleme32sn1aw" decreased from 3302 to 36 using "cdlemefs32sn1aw".
       "cdleme32sn2aw" decreased from 1687 to 26 using "cdlemefr32sn2aw".
       "cdleme32snaw" decreased from 376 to 375 using "cdlemefs32sn1aw".
       "cdleme32snaw" decreased from 375 to 368 using "cdlemefr32sn2aw".
       "cdleme35sn3a" decreased from 547 to 523 using "cdleme43frv1sn".

(Contributed by NM, 27-Mar-2013.)

**Hypotheses**
Ref	Expression
cdlemefs32.b	⊢ 𝐵 = (Base‘𝐾)
cdlemefs32.l	⊢ ≤ = (le‘𝐾)
cdlemefs32.j	⊢ ∨ = (join‘𝐾)
cdlemefs32.m	⊢ ∧ = (meet‘𝐾)
cdlemefs32.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemefs32.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemefs32.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdlemefs32.d	⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
cdlemefs32.e	⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
cdlemefs32.i	⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸))
cdlemefs32.n	⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶)
cdleme29fs.o	⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊))))
cdleme29fs.f	⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥))
cdleme43fsv.y	⊢ 𝑌 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
cdleme43fsv.z	⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝑌 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)))

**Assertion**
Ref	Expression
cdlemefs31fv1	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝐹‘𝑅) = 𝑍)

Distinct variable groups: 𝑡,𝑠,𝑥,𝑦,𝑧,𝐴 𝐵,𝑠,𝑡,𝑥,𝑦,𝑧 𝑦,𝐷 𝑦,𝐸 𝐻,𝑠,𝑡,𝑦 ∨ ,𝑠,𝑡,𝑥,𝑦,𝑧 𝐾,𝑠,𝑡,𝑦 ≤ ,𝑠,𝑡,𝑥,𝑦,𝑧 ∧ ,𝑠,𝑡,𝑥,𝑦,𝑧 𝑥,𝑁,𝑧 𝑃,𝑠,𝑡,𝑦,𝑧 𝑄,𝑠,𝑡,𝑦,𝑧 𝑅,𝑠,𝑡,𝑦 𝑡,𝑈,𝑦 𝑊,𝑠,𝑡,𝑥,𝑦,𝑧 𝑦,𝑌 𝐷,𝑠 𝑧,𝐻 𝑧,𝐾 𝑧,𝑅 𝑡,𝑆,𝑦 𝑡,𝑍 𝑥,𝑅 𝑥,𝑃 𝑥,𝑄 Allowed substitution hints: 𝐶(𝑥,𝑦,𝑧,𝑡,𝑠) 𝐷(𝑥,𝑧,𝑡) 𝑆(𝑥,𝑧,𝑠) 𝑈(𝑥,𝑧,𝑠) 𝐸(𝑥,𝑧,𝑡,𝑠) 𝐹(𝑥,𝑦,𝑧,𝑡,𝑠) 𝐻(𝑥) 𝐼(𝑥,𝑦,𝑧,𝑡,𝑠) 𝐾(𝑥) 𝑁(𝑦,𝑡,𝑠) 𝑂(𝑥,𝑦,𝑧,𝑡,𝑠) 𝑌(𝑥,𝑧,𝑡,𝑠) 𝑍(𝑥,𝑦,𝑧,𝑠)

**Proof of Theorem cdlemefs31fv1**
Step	Hyp	Ref	Expression
1		simp1 1136	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
2		simp21 1207	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → 𝑃 ≠ 𝑄)
3		simp22 1208	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))
4		simp3l 1202	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
5		cdlemefs32.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
6		cdlemefs32.l	. . . 4 ⊢ ≤ = (le‘𝐾)
7		cdlemefs32.j	. . . 4 ⊢ ∨ = (join‘𝐾)
8		cdlemefs32.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
9		cdlemefs32.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
10		cdlemefs32.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
11		cdlemefs32.u	. . . 4 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
12		cdlemefs32.d	. . . 4 ⊢ 𝐷 = ((𝑡 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑡) ∧ 𝑊)))
13		cdlemefs32.e	. . . 4 ⊢ 𝐸 = ((𝑃 ∨ 𝑄) ∧ (𝐷 ∨ ((𝑠 ∨ 𝑡) ∧ 𝑊)))
14		cdlemefs32.i	. . . 4 ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐸))
15		cdlemefs32.n	. . . 4 ⊢ 𝑁 = if(𝑠 ≤ (𝑃 ∨ 𝑄), 𝐼, 𝐶)
16		cdleme29fs.o	. . . 4 ⊢ 𝑂 = (℩𝑧 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ (𝑠 ∨ (𝑥 ∧ 𝑊)) = 𝑥) → 𝑧 = (𝑁 ∨ (𝑥 ∧ 𝑊))))
17		cdleme29fs.f	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if((𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊), 𝑂, 𝑥))
18	5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17	cdlemefs32fva1 40542	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → (𝐹‘𝑅) = ⦋𝑅 / 𝑠⦌𝑁)
19	1, 2, 3, 4, 18	syl121anc 1377	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝐹‘𝑅) = ⦋𝑅 / 𝑠⦌𝑁)
20		cdleme43fsv.y	. . 3 ⊢ 𝑌 = ((𝑆 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑆) ∧ 𝑊)))
21		cdleme43fsv.z	. . 3 ⊢ 𝑍 = ((𝑃 ∨ 𝑄) ∧ (𝑌 ∨ ((𝑅 ∨ 𝑆) ∧ 𝑊)))
22	5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 20, 21	cdleme43fsv1sn 40540	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ⦋𝑅 / 𝑠⦌𝑁 = 𝑍)
23	19, 22	eqtrd 2768	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝐹‘𝑅) = 𝑍)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ∀wral 3048 ⦋csb 3846 ifcif 4474 class class class wbr 5093 ↦ cmpt 5174 ‘cfv 6486 ℩crio 7308 (class class class)co 7352 Basecbs 17122 lecple 17170 joincjn 18219 meetcmee 18220 Atomscatm 39382 HLchlt 39469 LHypclh 40103

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-riotaBAD 39072

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-iun 4943 df-iin 4944 df-br 5094 df-opab 5156 df-mpt 5175 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-1st 7927 df-2nd 7928 df-undef 8209 df-proset 18202 df-poset 18221 df-plt 18236 df-lub 18252 df-glb 18253 df-join 18254 df-meet 18255 df-p0 18331 df-p1 18332 df-lat 18340 df-clat 18407 df-oposet 39295 df-ol 39297 df-oml 39298 df-covers 39385 df-ats 39386 df-atl 39417 df-cvlat 39441 df-hlat 39470 df-llines 39617 df-lplanes 39618 df-lvols 39619 df-lines 39620 df-psubsp 39622 df-pmap 39623 df-padd 39915 df-lhyp 40107

This theorem is referenced by: cdlemefs44 40545

W3C validator