lvolnle3at - Mathbox for Norm Megill

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

Theorem lvolnle3at 39110

Description: A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.)

**Hypotheses**
Ref	Expression
lvolnle3at.l	⊢ ≤ = (le‘𝐾)
lvolnle3at.j	⊢ ∨ = (join‘𝐾)
lvolnle3at.a	⊢ 𝐴 = (Atoms‘𝐾)
lvolnle3at.v	⊢ 𝑉 = (LVols‘𝐾)

**Assertion**
Ref	Expression
lvolnle3at	⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))

Proof of Theorem lvolnle3at Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplr 767	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑋 ∈ 𝑉)
2		eqid 2725	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		eqid 2725	. . . . . 6 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
4		eqid 2725	. . . . . 6 ⊢ (LPlanes‘𝐾) = (LPlanes‘𝐾)
5		lvolnle3at.v	. . . . . 6 ⊢ 𝑉 = (LVols‘𝐾)
6	2, 3, 4, 5	islvol 39101	. . . . 5 ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
7	6	ad2antrr 724	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
8	1, 7	mpbid 231	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋))
9	8	simprd 494	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)
10		oveq1 7422	. . . . . . . . 9 ⊢ (𝑃 = 𝑄 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑄))
11	10	oveq1d 7430	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑄 ∨ 𝑄) ∨ 𝑅))
12	11	breq2d 5155	. . . . . . 7 ⊢ (𝑃 = 𝑄 → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)))
13	12	notbid 317	. . . . . 6 ⊢ (𝑃 = 𝑄 → (¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ¬ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)))
14		simp1l 1194	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ HL)
15		simp3l 1198	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (LPlanes‘𝐾))
16		simp21 1203	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑃 ∈ 𝐴)
17		simp22 1204	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑄 ∈ 𝐴)
18		lvolnle3at.l	. . . . . . . . . . . . 13 ⊢ ≤ = (le‘𝐾)
19		lvolnle3at.j	. . . . . . . . . . . . 13 ⊢ ∨ = (join‘𝐾)
20		lvolnle3at.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (Atoms‘𝐾)
21	18, 19, 20, 4	lplnnle2at 39069	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ¬ 𝑦 ≤ (𝑃 ∨ 𝑄))
22	14, 15, 16, 17, 21	syl13anc 1369	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦 ≤ (𝑃 ∨ 𝑄))
23	2, 4	lplnbase 39062	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (LPlanes‘𝐾) → 𝑦 ∈ (Base‘𝐾))
24	15, 23	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (Base‘𝐾))
25		simp1r 1195	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ 𝑉)
26	2, 5	lvolbase 39106	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (Base‘𝐾))
27	25, 26	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ (Base‘𝐾))
28		simp3r 1199	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦( ⋖ ‘𝐾)𝑋)
29		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (lt‘𝐾) = (lt‘𝐾)
30	2, 29, 3	cvrlt 38797	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → 𝑦(lt‘𝐾)𝑋)
31	14, 24, 27, 28, 30	syl31anc 1370	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦(lt‘𝐾)𝑋)
32		hlpos 38893	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
33	14, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Poset)
34	2, 19, 20	hlatjcl 38894	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
35	14, 16, 17, 34	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
36	2, 18, 29	pltletr 18332	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑃 ∨ 𝑄)) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
37	33, 24, 27, 35, 36	syl13anc 1369	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑃 ∨ 𝑄)) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
38	31, 37	mpand 693	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑃 ∨ 𝑄) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
39	18, 29	pltle 18322	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
40	14, 15, 35, 39	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
41	38, 40	syld 47	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
42	22, 41	mtod 197	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ (𝑃 ∨ 𝑄))
43	42	adantr 479	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ (𝑃 ∨ 𝑄))
44		simprr 771	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
45	14	hllatd 38891	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Lat)
46		simp23 1205	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ 𝐴)
47	2, 20	atbase 38816	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
48	46, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ (Base‘𝐾))
49	2, 18, 19	latleeqj2 18441	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
50	45, 48, 35, 49	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
51	50	adantr 479	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
52	44, 51	mpbid 231	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄))
53	52	breq2d 5155	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ (𝑃 ∨ 𝑄)))
54	43, 53	mtbird 324	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
55	54	anassrs 466	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
56		simpl1l 1221	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐾 ∈ HL)
57		simpl3l 1225	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑦 ∈ (LPlanes‘𝐾))
58		simpl2 1189	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
59		simpr 483	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)))
60	18, 19, 20, 4	lplni2 39065	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾))
61	56, 58, 59, 60	syl3anc 1368	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾))
62	29, 4	lplnnlt 39093	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾)) → ¬ 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅))
63	56, 57, 61, 62	syl3anc 1368	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅))
64	2, 19	latjcl 18428	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
65	45, 35, 48, 64	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
66	2, 18, 29	pltletr 18332	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
67	33, 24, 27, 65, 66	syl13anc 1369	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
68	31, 67	mpand 693	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
69	68	adantr 479	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
70	63, 69	mtod 197	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
71	70	anassrs 466	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
72	55, 71	pm2.61dan 811	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
73		eqid 2725	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
74	73, 19, 20, 4	lplnnle2at 39069	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑦(le‘𝐾)(𝑄 ∨ 𝑅))
75	14, 15, 17, 46, 74	syl13anc 1369	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦(le‘𝐾)(𝑄 ∨ 𝑅))
76	2, 19, 20	hlatjcl 38894	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
77	14, 17, 46, 76	syl3anc 1368	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
78	2, 18, 29	pltletr 18332	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑄 ∨ 𝑅)) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
79	33, 24, 27, 77, 78	syl13anc 1369	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑄 ∨ 𝑅)) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
80	31, 79	mpand 693	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑄 ∨ 𝑅) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
81	73, 29	pltle 18322	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
82	14, 15, 77, 81	syl3anc 1368	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
83	80, 82	syld 47	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
84	75, 83	mtod 197	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ (𝑄 ∨ 𝑅))
85	19, 20	hlatjidm 38896	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑄 ∨ 𝑄) = 𝑄)
86	14, 17, 85	syl2anc 582	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 ∨ 𝑄) = 𝑄)
87	86	oveq1d 7430	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑄 ∨ 𝑄) ∨ 𝑅) = (𝑄 ∨ 𝑅))
88	87	breq2d 5155	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ (𝑄 ∨ 𝑅)))
89	84, 88	mtbird 324	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅))
90	13, 72, 89	pm2.61ne 3017	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
91	90	3expia 1118	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
92	91	expd 414	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑦 ∈ (LPlanes‘𝐾) → (𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))))
93	92	rexlimdv 3143	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
94	9, 93	mpd 15	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2930 ∃wrex 3060 class class class wbr 5143 ‘cfv 6542 (class class class)co 7415 Basecbs 17177 lecple 17237 Posetcpo 18296 ltcplt 18297 joincjn 18300 Latclat 18420 ⋖ ccvr 38789 Atomscatm 38790 HLchlt 38877 LPlanesclpl 39020 LVolsclvol 39021

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7737

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5227 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7371 df-ov 7418 df-oprab 7419 df-proset 18284 df-poset 18302 df-plt 18319 df-lub 18335 df-glb 18336 df-join 18337 df-meet 18338 df-p0 18414 df-lat 18421 df-clat 18488 df-oposet 38703 df-ol 38705 df-oml 38706 df-covers 38793 df-ats 38794 df-atl 38825 df-cvlat 38849 df-hlat 38878 df-llines 39026 df-lplanes 39027 df-lvols 39028

This theorem is referenced by: lvolnleat 39111 lvolnlelln 39112 lvolnlelpln 39113 3atnelvolN 39114 4atlem3 39124 dalem39 39239

W3C validator