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 39659

Description: Lemma for dalem14 39660. (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 39606	. . 3 ⊢ (𝜑 → 𝐾 ∈ HL)
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝐾 ∈ HL)
4	1	dalemyeo 39615	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝑂)
5	4	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ∈ 𝑂)
6	1	dalemzeo 39616	. . 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 2729	. . 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 39655	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑊 ∈ (LVols‘𝐾))
17	1	dalemkelat 39607	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Lat)
18	1, 11	dalemyeb 39632	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾))
19	1, 10	dalemceb 39621	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾))
20		eqid 2729	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
21	20, 8, 9	latlej1 18354	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾)) → 𝑌 ≤ (𝑌 ∨ 𝐶))
22	17, 18, 19, 21	syl3anc 1373	. . . 4 ⊢ (𝜑 → 𝑌 ≤ (𝑌 ∨ 𝐶))
23	22, 15	breqtrrdi 5134	. . 3 ⊢ (𝜑 → 𝑌 ≤ 𝑊)
24	23	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ≤ 𝑊)
25	1, 8, 9, 10, 11, 13, 14, 15	dalem8 39653	. . 3 ⊢ (𝜑 → 𝑍 ≤ 𝑊)
26	25	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑍 ≤ 𝑊)
27		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ≠ 𝑍)
28	8, 9, 11, 12	2lplnj 39603	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ∧ 𝑊 ∈ (LVols‘𝐾)) ∧ (𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ∧ 𝑌 ≠ 𝑍)) → (𝑌 ∨ 𝑍) = 𝑊)
29	3, 5, 7, 16, 24, 26, 27, 28	syl133anc 1395	1 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → (𝑌 ∨ 𝑍) = 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 class class class wbr 5092 ‘cfv 6482 (class class class)co 7349 Basecbs 17120 lecple 17168 joincjn 18217 Latclat 18337 Atomscatm 39246 HLchlt 39333 LPlanesclpl 39475 LVolsclvol 39476

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 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 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-proset 18200 df-poset 18219 df-plt 18234 df-lub 18250 df-glb 18251 df-join 18252 df-meet 18253 df-p0 18329 df-lat 18338 df-clat 18405 df-oposet 39159 df-ol 39161 df-oml 39162 df-covers 39249 df-ats 39250 df-atl 39281 df-cvlat 39305 df-hlat 39334 df-llines 39481 df-lplanes 39482 df-lvols 39483

This theorem is referenced by: dalem14 39660

W3C validator