lvolnle3at

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

	Ref	Expression
Hypotheses	lvolnle3at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lvolnle3at.j	$⊢ \underset{˙}{\lor} = join (K)$
	lvolnle3at.a	$⊢ A = Atoms (K)$
	lvolnle3at.v	$⊢ V = LVols (K)$
Assertion	lvolnle3at	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$

Proof

Step	Hyp	Ref	Expression
1		lvolnle3at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lvolnle3at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lvolnle3at.a	$⊢ A = Atoms (K)$
4		lvolnle3at.v	$⊢ V = LVols (K)$
5		simplr	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to X \in V$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7		eqid	$⊢ ⋖_{K} = ⋖_{K}$
8		eqid	$⊢ LPlanes (K) = LPlanes (K)$
9	6 7 8 4	islvol	$⊢ K \in HL \to (X \in V \leftrightarrow (X \in {Base}_{K} \land \exists y \in LPlanes (K) y ⋖_{K} X))$
10	9	ad2antrr	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to (X \in V \leftrightarrow (X \in {Base}_{K} \land \exists y \in LPlanes (K) y ⋖_{K} X))$
11	5 10	mpbid	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to (X \in {Base}_{K} \land \exists y \in LPlanes (K) y ⋖_{K} X)$
12	11	simprd	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to \exists y \in LPlanes (K) y ⋖_{K} X$
13		oveq1	$⊢ P = Q \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q$
14	13	oveq1d	$⊢ P = Q \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
15	14	breq2d	$⊢ P = Q \to (X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow X \underset{˙}{\leq} ((Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
16	15	notbid	$⊢ P = Q \to (\neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow \neg X \underset{˙}{\leq} ((Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
17		simp1l	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to K \in HL$
18		simp3l	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to y \in LPlanes (K)$
19		simp21	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to P \in A$
20		simp22	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to Q \in A$
21	1 2 3 8	lplnnle2at	$⊢ (K \in HL \land (y \in LPlanes (K) \land P \in A \land Q \in A)) \to \neg y \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
22	17 18 19 20 21	syl13anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to \neg y \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
23	6 8	lplnbase	$⊢ y \in LPlanes (K) \to y \in {Base}_{K}$
24	18 23	syl	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to y \in {Base}_{K}$
25		simp1r	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to X \in V$
26	6 4	lvolbase	$⊢ X \in V \to X \in {Base}_{K}$
27	25 26	syl	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to X \in {Base}_{K}$
28		simp3r	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to y ⋖_{K} X$
29		eqid	$⊢ <_{K} = <_{K}$
30	6 29 7	cvrlt	$⊢ ((K \in HL \land y \in {Base}_{K} \land X \in {Base}_{K}) \land y ⋖_{K} X) \to y <_{K} X$
31	17 24 27 28 30	syl31anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to y <_{K} X$
32		hlpos	$⊢ K \in HL \to K \in Poset$
33	17 32	syl	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to K \in Poset$
34	6 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
35	17 19 20 34	syl3anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
36	6 1 29	pltletr	$⊢ (K \in Poset \land (y \in {Base}_{K} \land X \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((y <_{K} X \land X \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y <_{K} (P \underset{˙}{\lor} Q))$
37	33 24 27 35 36	syl13anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to ((y <_{K} X \land X \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to y <_{K} (P \underset{˙}{\lor} Q))$
38	31 37	mpand	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to y <_{K} (P \underset{˙}{\lor} Q))$
39	1 29	pltle	$⊢ (K \in HL \land y \in LPlanes (K) \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (y <_{K} (P \underset{˙}{\lor} Q) \to y \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
40	17 18 35 39	syl3anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (y <_{K} (P \underset{˙}{\lor} Q) \to y \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
41	38 40	syld	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to y \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
42	22 41	mtod	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to \neg X \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
43	42	adantr	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg X \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
44		simprr	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
45	17	hllatd	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to K \in Lat$
46		simp23	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to R \in A$
47	6 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
48	46 47	syl	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to R \in {Base}_{K}$
49	6 1 2	latleeqj2	$⊢ (K \in Lat \land R \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q)$
50	45 48 35 49	syl3anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q)$
51	50	adantr	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q)$
52	44 51	mpbid	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} Q$
53	52	breq2d	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow X \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
54	43 53	mtbird	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
55	54	anassrs	$⊢ ((((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land P \neq Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
56		simpl1l	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
57		simpl3l	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to y \in LPlanes (K)$
58		simpl2	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \in A \land Q \in A \land R \in A)$
59		simpr	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
60	1 2 3 8	lplni2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in LPlanes (K)$
61	56 58 59 60	syl3anc	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in LPlanes (K)$
62	29 8	lplnnlt	$⊢ (K \in HL \land y \in LPlanes (K) \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in LPlanes (K)) \to \neg y <_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
63	56 57 61 62	syl3anc	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg y <_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
64	6 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
65	45 35 48 64	syl3anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
66	6 1 29	pltletr	$⊢ (K \in Poset \land (y \in {Base}_{K} \land X \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K})) \to ((y <_{K} X \land X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to y <_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
67	33 24 27 65 66	syl13anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to ((y <_{K} X \land X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to y <_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
68	31 67	mpand	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \to y <_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
69	68	adantr	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \to y <_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
70	63 69	mtod	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
71	70	anassrs	$⊢ ((((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land P \neq Q) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
72	55 71	pm2.61dan	$⊢ (((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \land P \neq Q) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
73		eqid	$⊢ \leq_{K} = \leq_{K}$
74	73 2 3 8	lplnnle2at	$⊢ (K \in HL \land (y \in LPlanes (K) \land Q \in A \land R \in A)) \to \neg y \leq_{K} (Q \underset{˙}{\lor} R)$
75	17 18 20 46 74	syl13anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to \neg y \leq_{K} (Q \underset{˙}{\lor} R)$
76	6 2 3	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
77	17 20 46 76	syl3anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
78	6 1 29	pltletr	$⊢ (K \in Poset \land (y \in {Base}_{K} \land X \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K})) \to ((y <_{K} X \land X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to y <_{K} (Q \underset{˙}{\lor} R))$
79	33 24 27 77 78	syl13anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to ((y <_{K} X \land X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to y <_{K} (Q \underset{˙}{\lor} R))$
80	31 79	mpand	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to y <_{K} (Q \underset{˙}{\lor} R))$
81	73 29	pltle	$⊢ (K \in HL \land y \in LPlanes (K) \land Q \underset{˙}{\lor} R \in {Base}_{K}) \to (y <_{K} (Q \underset{˙}{\lor} R) \to y \leq_{K} (Q \underset{˙}{\lor} R))$
82	17 18 77 81	syl3anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (y <_{K} (Q \underset{˙}{\lor} R) \to y \leq_{K} (Q \underset{˙}{\lor} R))$
83	80 82	syld	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to y \leq_{K} (Q \underset{˙}{\lor} R))$
84	75 83	mtod	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to \neg X \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
85	2 3	hlatjidm	$⊢ (K \in HL \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
86	17 20 85	syl2anc	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to Q \underset{˙}{\lor} Q = Q$
87	86	oveq1d	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
88	87	breq2d	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to (X \underset{˙}{\leq} ((Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow X \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
89	84 88	mtbird	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to \neg X \underset{˙}{\leq} ((Q \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
90	16 72 89	pm2.61ne	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A) \land (y \in LPlanes (K) \land y ⋖_{K} X)) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
91	90	3expia	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to ((y \in LPlanes (K) \land y ⋖_{K} X) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
92	91	expd	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to (y \in LPlanes (K) \to (y ⋖_{K} X \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)))$
93	92	rexlimdv	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to (\exists y \in LPlanes (K) y ⋖_{K} X \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
94	12 93	mpd	$⊢ ((K \in HL \land X \in V) \land (P \in A \land Q \in A \land R \in A)) \to \neg X \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$

Metamath Proof Explorer

Theorem lvolnle3at

Proof