Theorem lvolnle3at 38045

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 2736	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		eqid 2736	. . . . . 6 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
4		eqid 2736	. . . . . 6 ⊢ (LPlanes‘𝐾) = (LPlanes‘𝐾)
5		lvolnle3at.v	. . . . . 6 ⊢ 𝑉 = (LVols‘𝐾)
6	2, 3, 4, 5	islvol 38036	. . . . 5 ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
7	6	ad2antrr 724	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
8	1, 7	mpbid 231	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋))
9	8	simprd 496	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)
10		oveq1 7364	. . . . . . . . 9 ⊢ (𝑃 = 𝑄 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑄))
11	10	oveq1d 7372	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑄 ∨ 𝑄) ∨ 𝑅))
12	11	breq2d 5117	. . . . . . 7 ⊢ (𝑃 = 𝑄 → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)))
13	12	notbid 317	. . . . . 6 ⊢ (𝑃 = 𝑄 → (¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ¬ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)))
14		simp1l 1197	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ HL)
15		simp3l 1201	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (LPlanes‘𝐾))
16		simp21 1206	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑃 ∈ 𝐴)
17		simp22 1207	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑄 ∈ 𝐴)
18		lvolnle3at.l	. . . . . . . . . . . . 13 ⊢ ≤ = (le‘𝐾)
19		lvolnle3at.j	. . . . . . . . . . . . 13 ⊢ ∨ = (join‘𝐾)
20		lvolnle3at.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (Atoms‘𝐾)
21	18, 19, 20, 4	lplnnle2at 38004	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ¬ 𝑦 ≤ (𝑃 ∨ 𝑄))
22	14, 15, 16, 17, 21	syl13anc 1372	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦 ≤ (𝑃 ∨ 𝑄))
23	2, 4	lplnbase 37997	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (LPlanes‘𝐾) → 𝑦 ∈ (Base‘𝐾))
24	15, 23	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (Base‘𝐾))
25		simp1r 1198	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ 𝑉)
26	2, 5	lvolbase 38041	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (Base‘𝐾))
27	25, 26	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ (Base‘𝐾))
28		simp3r 1202	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦( ⋖ ‘𝐾)𝑋)
29		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (lt‘𝐾) = (lt‘𝐾)
30	2, 29, 3	cvrlt 37732	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → 𝑦(lt‘𝐾)𝑋)
31	14, 24, 27, 28, 30	syl31anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦(lt‘𝐾)𝑋)
32		hlpos 37828	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
33	14, 32	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Poset)
34	2, 19, 20	hlatjcl 37829	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
35	14, 16, 17, 34	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
36	2, 18, 29	pltletr 18232	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑃 ∨ 𝑄)) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
37	33, 24, 27, 35, 36	syl13anc 1372	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑃 ∨ 𝑄)) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
38	31, 37	mpand 693	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑃 ∨ 𝑄) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
39	18, 29	pltle 18222	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
40	14, 15, 35, 39	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
41	38, 40	syld 47	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
42	22, 41	mtod 197	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ (𝑃 ∨ 𝑄))
43	42	adantr 481	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ (𝑃 ∨ 𝑄))
44		simprr 771	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
45	14	hllatd 37826	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Lat)
46		simp23 1208	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ 𝐴)
47	2, 20	atbase 37751	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
48	46, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ (Base‘𝐾))
49	2, 18, 19	latleeqj2 18341	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
50	45, 48, 35, 49	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
51	50	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
52	44, 51	mpbid 231	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄))
53	52	breq2d 5117	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ (𝑃 ∨ 𝑄)))
54	43, 53	mtbird 324	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
55	54	anassrs 468	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
56		simpl1l 1224	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐾 ∈ HL)
57		simpl3l 1228	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑦 ∈ (LPlanes‘𝐾))
58		simpl2 1192	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
59		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)))
60	18, 19, 20, 4	lplni2 38000	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾))
61	56, 58, 59, 60	syl3anc 1371	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾))
62	29, 4	lplnnlt 38028	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾)) → ¬ 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅))
63	56, 57, 61, 62	syl3anc 1371	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅))
64	2, 19	latjcl 18328	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
65	45, 35, 48, 64	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
66	2, 18, 29	pltletr 18232	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
67	33, 24, 27, 65, 66	syl13anc 1372	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
68	31, 67	mpand 693	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
69	68	adantr 481	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
70	63, 69	mtod 197	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
71	70	anassrs 468	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
72	55, 71	pm2.61dan 811	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
73		eqid 2736	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
74	73, 19, 20, 4	lplnnle2at 38004	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑦(le‘𝐾)(𝑄 ∨ 𝑅))
75	14, 15, 17, 46, 74	syl13anc 1372	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦(le‘𝐾)(𝑄 ∨ 𝑅))
76	2, 19, 20	hlatjcl 37829	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
77	14, 17, 46, 76	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
78	2, 18, 29	pltletr 18232	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑄 ∨ 𝑅)) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
79	33, 24, 27, 77, 78	syl13anc 1372	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑄 ∨ 𝑅)) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
80	31, 79	mpand 693	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑄 ∨ 𝑅) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
81	73, 29	pltle 18222	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
82	14, 15, 77, 81	syl3anc 1371	. . . . . . . . 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 37831	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑄 ∨ 𝑄) = 𝑄)
86	14, 17, 85	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 ∨ 𝑄) = 𝑄)
87	86	oveq1d 7372	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑄 ∨ 𝑄) ∨ 𝑅) = (𝑄 ∨ 𝑅))
88	87	breq2d 5117	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ (𝑄 ∨ 𝑅)))
89	84, 88	mtbird 324	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅))
90	13, 72, 89	pm2.61ne 3030	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
91	90	3expia 1121	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
92	91	expd 416	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑦 ∈ (LPlanes‘𝐾) → (𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))))
93	92	rexlimdv 3150	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
94	9, 93	mpd 15	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3073   class class class wbr 5105  ‘cfv 6496  (class class class)co 7357  Basecbs 17083  lecple 17140  Posetcpo 18196  ltcplt 18197  joincjn 18200  Latclat 18320   ⋖ ccvr 37724  Atomscatm 37725  HLchlt 37812  LPlanesclpl 37955  LVolsclvol 37956

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-proset 18184  df-poset 18202  df-plt 18219  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-p0 18314  df-lat 18321  df-clat 18388  df-oposet 37638  df-ol 37640  df-oml 37641  df-covers 37728  df-ats 37729  df-atl 37760  df-cvlat 37784  df-hlat 37813  df-llines 37961  df-lplanes 37962  df-lvols 37963

This theorem is referenced by:  lvolnleat  38046  lvolnlelln  38047  lvolnlelpln  38048  3atnelvolN  38049  4atlem3  38059  dalem39  38174