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 40052

Description: Lemma for dalem14 40053. (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 39999	. . 3 ⊢ (𝜑 → 𝐾 ∈ HL)
3	2	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝐾 ∈ HL)
4	1	dalemyeo 40008	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝑂)
5	4	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ∈ 𝑂)
6	1	dalemzeo 40009	. . 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 2737	. . 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 40048	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑊 ∈ (LVols‘𝐾))
17	1	dalemkelat 40000	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Lat)
18	1, 11	dalemyeb 40025	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾))
19	1, 10	dalemceb 40014	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾))
20		eqid 2737	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
21	20, 8, 9	latlej1 18383	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝐶 ∈ (Base‘𝐾)) → 𝑌 ≤ (𝑌 ∨ 𝐶))
22	17, 18, 19, 21	syl3anc 1374	. . . 4 ⊢ (𝜑 → 𝑌 ≤ (𝑌 ∨ 𝐶))
23	22, 15	breqtrrdi 5142	. . 3 ⊢ (𝜑 → 𝑌 ≤ 𝑊)
24	23	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ≤ 𝑊)
25	1, 8, 9, 10, 11, 13, 14, 15	dalem8 40046	. . 3 ⊢ (𝜑 → 𝑍 ≤ 𝑊)
26	25	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑍 ≤ 𝑊)
27		simpr 484	. 2 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → 𝑌 ≠ 𝑍)
28	8, 9, 11, 12	2lplnj 39996	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂 ∧ 𝑊 ∈ (LVols‘𝐾)) ∧ (𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊 ∧ 𝑌 ≠ 𝑍)) → (𝑌 ∨ 𝑍) = 𝑊)
29	3, 5, 7, 16, 24, 26, 27, 28	syl133anc 1396	1 ⊢ ((𝜑 ∧ 𝑌 ≠ 𝑍) → (𝑌 ∨ 𝑍) = 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 class class class wbr 5100 ‘cfv 6500 (class class class)co 7368 Basecbs 17148 lecple 17196 joincjn 18246 Latclat 18366 Atomscatm 39639 HLchlt 39726 LPlanesclpl 39868 LVolsclvol 39869

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-proset 18229 df-poset 18248 df-plt 18263 df-lub 18279 df-glb 18280 df-join 18281 df-meet 18282 df-p0 18358 df-lat 18367 df-clat 18434 df-oposet 39552 df-ol 39554 df-oml 39555 df-covers 39642 df-ats 39643 df-atl 39674 df-cvlat 39698 df-hlat 39727 df-llines 39874 df-lplanes 39875 df-lvols 39876

This theorem is referenced by: dalem14 40053

W3C validator