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 36286

Description: Lemma for dalem14 36287. (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 36233	. . 3 ⊢ (𝜑 → 𝐾 ∈ HL)
3	2	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝐾 ∈ HL)
4	1	dalemyeo 36242	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝑂)
5	4	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ∈ 𝑂)
6	1	dalemzeo 36243	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝑂)
7	6	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑍 ∈ 𝑂)
8		dalemc.l	. . 3 ⊢ ≤ = (le‘𝐾)
9		dalemc.j	. . 3 ⊢ ∨ = (join‘𝐾)
10		dalemc.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
11		dalem13.o	. . 3 ⊢ 𝑂 = (LPlanes‘𝐾)
12		eqid 2772	. . 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 36282	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑊 ∈ (LVols‘𝐾))
17	1	dalemkelat 36234	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Lat)
18	1, 11	dalemyeb 36259	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾))
19	1, 10	dalemceb 36248	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾))
20		eqid 2772	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
21	20, 8, 9	latlej1 17540	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾)) → 𝑌 ≤ (𝑌 ∨ 𝐶))
22	17, 18, 19, 21	syl3anc 1351	. . . 4 ⊢ (𝜑 → 𝑌 ≤ (𝑌 ∨ 𝐶))
23	22, 15	syl6breqr 4967	. . 3 ⊢ (𝜑 → 𝑌 ≤ 𝑊)
24	23	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ≤ 𝑊)
25	1, 8, 9, 10, 11, 13, 14, 15	dalem8 36280	. . 3 ⊢ (𝜑 → 𝑍 ≤ 𝑊)
26	25	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑍 ≤ 𝑊)
27		simpr 477	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ≠ 𝑍)
28	8, 9, 11, 12	2lplnj 36230	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ∧ 𝑊 ∈ (LVols‘𝐾)) ∧ (𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ∧ 𝑌 ≠ 𝑍)) → (𝑌 ∨ 𝑍) = 𝑊)
29	3, 5, 7, 16, 24, 26, 27, 28	syl133anc 1373	1 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → (𝑌 ∨ 𝑍) = 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2050 ≠ wne 2961 class class class wbr 4925 ‘cfv 6185 (class class class)co 6974 Basecbs 16337 lecple 16426 joincjn 17424 Latclat 17525 Atomscatm 35873 HLchlt 35960 LPlanesclpl 36102 LVolsclvol 36103

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-rep 5045 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-proset 17408 df-poset 17426 df-plt 17438 df-lub 17454 df-glb 17455 df-join 17456 df-meet 17457 df-p0 17519 df-lat 17526 df-clat 17588 df-oposet 35786 df-ol 35788 df-oml 35789 df-covers 35876 df-ats 35877 df-atl 35908 df-cvlat 35932 df-hlat 35961 df-llines 36108 df-lplanes 36109 df-lvols 36110

This theorem is referenced by: dalem14 36287

W3C validator