dalem13 - Mathbox for Norm Megill

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

Theorem dalem13 39637

Description: Lemma for dalem14 39638. (Contributed by NM, 21-Jul-2012.)

**Hypotheses**
Ref	Expression
dalema.ph	⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
dalemc.l	⊢ ≤ = (le‘𝐾)
dalemc.j	⊢ ∨ = (join‘𝐾)
dalemc.a	⊢ 𝐴 = (Atoms‘𝐾)
dalem13.o	⊢ 𝑂 = (LPlanes‘𝐾)
dalem13.y	⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
dalem13.z	⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)
dalem13.w	⊢ 𝑊 = (𝑌 ∨ 𝐶)

**Assertion**
Ref	Expression
dalem13	⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → (𝑌 ∨ 𝑍) = 𝑊)

**Proof of Theorem dalem13**
Step	Hyp	Ref	Expression
1		dalema.ph	. . . 4 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
2	1	dalemkehl 39584	. . 3 ⊢ (𝜑 → 𝐾 ∈ HL)
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝐾 ∈ HL)
4	1	dalemyeo 39593	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝑂)
5	4	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ∈ 𝑂)
6	1	dalemzeo 39594	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝑂)
7	6	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑍 ∈ 𝑂)
8		dalemc.l	. . 3 ⊢ ≤ = (le‘𝐾)
9		dalemc.j	. . 3 ⊢ ∨ = (join‘𝐾)
10		dalemc.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
11		dalem13.o	. . 3 ⊢ 𝑂 = (LPlanes‘𝐾)
12		eqid 2734	. . 3 ⊢ (LVols‘𝐾) = (LVols‘𝐾)
13		dalem13.y	. . 3 ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)
14		dalem13.z	. . 3 ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)
15		dalem13.w	. . 3 ⊢ 𝑊 = (𝑌 ∨ 𝐶)
16	1, 8, 9, 10, 11, 12, 13, 14, 15	dalem9 39633	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑊 ∈ (LVols‘𝐾))
17	1	dalemkelat 39585	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Lat)
18	1, 11	dalemyeb 39610	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾))
19	1, 10	dalemceb 39599	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾))
20		eqid 2734	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
21	20, 8, 9	latlej1 18462	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾)) → 𝑌 ≤ (𝑌 ∨ 𝐶))
22	17, 18, 19, 21	syl3anc 1372	. . . 4 ⊢ (𝜑 → 𝑌 ≤ (𝑌 ∨ 𝐶))
23	22, 15	breqtrrdi 5165	. . 3 ⊢ (𝜑 → 𝑌 ≤ 𝑊)
24	23	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ≤ 𝑊)
25	1, 8, 9, 10, 11, 13, 14, 15	dalem8 39631	. . 3 ⊢ (𝜑 → 𝑍 ≤ 𝑊)
26	25	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑍 ≤ 𝑊)
27		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ≠ 𝑍)
28	8, 9, 11, 12	2lplnj 39581	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ∧ 𝑊 ∈ (LVols‘𝐾)) ∧ (𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ∧ 𝑌 ≠ 𝑍)) → (𝑌 ∨ 𝑍) = 𝑊)
29	3, 5, 7, 16, 24, 26, 27, 28	syl133anc 1394	1 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → (𝑌 ∨ 𝑍) = 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2931 class class class wbr 5123 ‘cfv 6541 (class class class)co 7413 Basecbs 17229 lecple 17280 joincjn 18327 Latclat 18445 Atomscatm 39223 HLchlt 39310 LPlanesclpl 39453 LVolsclvol 39454

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4888 df-iun 4973 df-br 5124 df-opab 5186 df-mpt 5206 df-id 5558 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-proset 18310 df-poset 18329 df-plt 18344 df-lub 18360 df-glb 18361 df-join 18362 df-meet 18363 df-p0 18439 df-lat 18446 df-clat 18513 df-oposet 39136 df-ol 39138 df-oml 39139 df-covers 39226 df-ats 39227 df-atl 39258 df-cvlat 39282 df-hlat 39311 df-llines 39459 df-lplanes 39460 df-lvols 39461

This theorem is referenced by: dalem14 39638

W3C validator