Theorem lvolnle3at 40733

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 781	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝑋 ∈ 𝑉)
2		eqid 2760	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		eqid 2760	. . . . . 6 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
4		eqid 2760	. . . . . 6 ⊢ (LPlanes‘𝐾) = (LPlanes‘𝐾)
5		lvolnle3at.v	. . . . . 6 ⊢ 𝑉 = (LVols‘𝐾)
6	2, 3, 4, 5	islvol 40724	. . . . 5 ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
7	6	ad2antrr 739	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)))
8	1, 7	mpbid 235	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑋 ∈ (Base‘𝐾) ∧ ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋))
9	8	simprd 501	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋)
10		oveq1 7428	. . . . . . . . 9 ⊢ (𝑃 = 𝑄 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑄))
11	10	oveq1d 7436	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑄 ∨ 𝑄) ∨ 𝑅))
12	11	breq2d 5114	. . . . . . 7 ⊢ (𝑃 = 𝑄 → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)))
13	12	notbid 321	. . . . . 6 ⊢ (𝑃 = 𝑄 → (¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ ¬ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅)))
14		simp1l 1216	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ HL)
15		simp3l 1220	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (LPlanes‘𝐾))
16		simp21 1225	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑃 ∈ 𝐴)
17		simp22 1226	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑄 ∈ 𝐴)
18		lvolnle3at.l	. . . . . . . . . . . . 13 ⊢ ≤ = (le‘𝐾)
19		lvolnle3at.j	. . . . . . . . . . . . 13 ⊢ ∨ = (join‘𝐾)
20		lvolnle3at.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (Atoms‘𝐾)
21	18, 19, 20, 4	lplnnle2at 40692	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ¬ 𝑦 ≤ (𝑃 ∨ 𝑄))
22	14, 15, 16, 17, 21	syl13anc 1399	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦 ≤ (𝑃 ∨ 𝑄))
23	2, 4	lplnbase 40685	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (LPlanes‘𝐾) → 𝑦 ∈ (Base‘𝐾))
24	15, 23	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦 ∈ (Base‘𝐾))
25		simp1r 1217	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ 𝑉)
26	2, 5	lvolbase 40729	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (Base‘𝐾))
27	25, 26	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑋 ∈ (Base‘𝐾))
28		simp3r 1221	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦( ⋖ ‘𝐾)𝑋)
29		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (lt‘𝐾) = (lt‘𝐾)
30	2, 29, 3	cvrlt 40421	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → 𝑦(lt‘𝐾)𝑋)
31	14, 24, 27, 28, 30	syl31anc 1400	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑦(lt‘𝐾)𝑋)
32		hlpos 40517	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
33	14, 32	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Poset)
34	2, 19, 20	hlatjcl 40518	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
35	14, 16, 17, 34	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
36	2, 18, 29	pltletr 18521	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑃 ∨ 𝑄)) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
37	33, 24, 27, 35, 36	syl13anc 1399	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑃 ∨ 𝑄)) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
38	31, 37	mpand 708	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑃 ∨ 𝑄) → 𝑦(lt‘𝐾)(𝑃 ∨ 𝑄)))
39	18, 29	pltle 18511	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
40	14, 15, 35, 39	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
41	38, 40	syld 48	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑃 ∨ 𝑄) → 𝑦 ≤ (𝑃 ∨ 𝑄)))
42	22, 41	mtod 201	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ (𝑃 ∨ 𝑄))
43	42	adantr 486	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ (𝑃 ∨ 𝑄))
44		simprr 785	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ≤ (𝑃 ∨ 𝑄))
45	14	hllatd 40515	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝐾 ∈ Lat)
46		simp23 1227	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ 𝐴)
47	2, 20	atbase 40440	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
48	46, 47	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → 𝑅 ∈ (Base‘𝐾))
49	2, 18, 19	latleeqj2 18632	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
50	45, 48, 35, 49	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
51	50	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ (𝑃 ∨ 𝑄) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄)))
52	44, 51	mpbid 235	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ 𝑄))
53	52	breq2d 5114	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ (𝑃 ∨ 𝑄)))
54	43, 53	mtbird 328	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
55	54	anassrs 473	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
56		simpl1l 1243	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝐾 ∈ HL)
57		simpl3l 1247	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑦 ∈ (LPlanes‘𝐾))
58		simpl2 1211	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴))
59		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)))
60	18, 19, 20, 4	lplni2 40688	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾))
61	56, 58, 59, 60	syl3anc 1398	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾))
62	29, 4	lplnnlt 40716	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (LPlanes‘𝐾)) → ¬ 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅))
63	56, 57, 61, 62	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅))
64	2, 19	latjcl 18619	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
65	45, 35, 48, 64	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))
66	2, 18, 29	pltletr 18521	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
67	33, 24, 27, 65, 66	syl13anc 1399	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
68	31, 67	mpand 708	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
69	68	adantr 486	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅) → 𝑦(lt‘𝐾)((𝑃 ∨ 𝑄) ∨ 𝑅)))
70	63, 69	mtod 201	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
71	70	anassrs 473	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
72	55, 71	pm2.61dan 825	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) ∧ 𝑃 ≠ 𝑄) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
73		eqid 2760	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
74	73, 19, 20, 4	lplnnle2at 40692	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑦(le‘𝐾)(𝑄 ∨ 𝑅))
75	14, 15, 17, 46, 74	syl13anc 1399	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑦(le‘𝐾)(𝑄 ∨ 𝑅))
76	2, 19, 20	hlatjcl 40518	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
77	14, 17, 46, 76	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))
78	2, 18, 29	pltletr 18521	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Poset ∧ (𝑦 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑄 ∨ 𝑅)) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
79	33, 24, 27, 77, 78	syl13anc 1399	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑦(lt‘𝐾)𝑋 ∧ 𝑋 ≤ (𝑄 ∨ 𝑅)) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
80	31, 79	mpand 708	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑄 ∨ 𝑅) → 𝑦(lt‘𝐾)(𝑄 ∨ 𝑅)))
81	73, 29	pltle 18511	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ (LPlanes‘𝐾) ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) → (𝑦(lt‘𝐾)(𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
82	14, 15, 77, 81	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑦(lt‘𝐾)(𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
83	80, 82	syld 48	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ (𝑄 ∨ 𝑅) → 𝑦(le‘𝐾)(𝑄 ∨ 𝑅)))
84	75, 83	mtod 201	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ (𝑄 ∨ 𝑅))
85	19, 20	hlatjidm 40520	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑄 ∨ 𝑄) = 𝑄)
86	14, 17, 85	syl2anc 596	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑄 ∨ 𝑄) = 𝑄)
87	86	oveq1d 7436	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ((𝑄 ∨ 𝑄) ∨ 𝑅) = (𝑄 ∨ 𝑅))
88	87	breq2d 5114	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → (𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅) ↔ 𝑋 ≤ (𝑄 ∨ 𝑅)))
89	84, 88	mtbird 328	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ ((𝑄 ∨ 𝑄) ∨ 𝑅))
90	13, 72, 89	pm2.61ne 3040	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))
91	90	3expia 1139	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ 𝑦( ⋖ ‘𝐾)𝑋) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
92	91	expd 421	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑦 ∈ (LPlanes‘𝐾) → (𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))))
93	92	rexlimdv 3161	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (∃𝑦 ∈ (LPlanes‘𝐾)𝑦( ⋖ ‘𝐾)𝑋 → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))
94	9, 93	mpd 16	1 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∃wrex 3086   class class class wbr 5102  ‘cfv 6539  (class class class)co 7421  Basecbs 17393  lecple 17441  Posetcpo 18487  ltcplt 18488  joincjn 18491  Latclat 18611   ⋖ ccvr 40413  Atomscatm 40414  HLchlt 40501  LPlanesclpl 40643  LVolsclvol 40644

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-proset 18474  df-poset 18493  df-plt 18508  df-lub 18524  df-glb 18525  df-join 18526  df-meet 18527  df-p0 18603  df-lat 18612  df-clat 18679  df-oposet 40327  df-ol 40329  df-oml 40330  df-covers 40417  df-ats 40418  df-atl 40449  df-cvlat 40473  df-hlat 40502  df-llines 40649  df-lplanes 40650  df-lvols 40651

This theorem is used by:  lvolnleat  40734  lvolnlelln  40735  lvolnlelpln  40736  3atnelvolN  40737  4atlem3  40747  dalem39  40862