lplncvrlvol2

Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012)

	Ref	Expression
Hypotheses	lplncvrlvol2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lplncvrlvol2.c	$⊢ C = ⋖_{K}$
	lplncvrlvol2.p	$⊢ P = LPlanes (K)$
	lplncvrlvol2.v	$⊢ V = LVols (K)$
Assertion	lplncvrlvol2	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to X C Y$

Proof

Step	Hyp	Ref	Expression
1		lplncvrlvol2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lplncvrlvol2.c	$⊢ C = ⋖_{K}$
3		lplncvrlvol2.p	$⊢ P = LPlanes (K)$
4		lplncvrlvol2.v	$⊢ V = LVols (K)$
5		simpr	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y$
6		simpl1	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to K \in HL$
7		simpl3	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to Y \in V$
8	3 4	lvolnelpln	$⊢ (K \in HL \land Y \in V) \to \neg Y \in P$
9	6 7 8	syl2anc	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to \neg Y \in P$
10		simpl2	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to X \in P$
11		eleq1	$⊢ X = Y \to (X \in P \leftrightarrow Y \in P)$
12	10 11	syl5ibcom	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to (X = Y \to Y \in P)$
13	12	necon3bd	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to (\neg Y \in P \to X \neq Y)$
14	9 13	mpd	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to X \neq Y$
15		eqid	$⊢ <_{K} = <_{K}$
16	1 15	pltval	$⊢ (K \in HL \land X \in P \land Y \in V) \to (X <_{K} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
17	16	adantr	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to (X <_{K} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
18	5 14 17	mpbir2and	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to X <_{K} Y$
19		simpl1	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X <_{K} Y) \to K \in HL$
20		simpl2	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X <_{K} Y) \to X \in P$
21		eqid	$⊢ {Base}_{K} = {Base}_{K}$
22	21 3	lplnbase	$⊢ X \in P \to X \in {Base}_{K}$
23	20 22	syl	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X <_{K} Y) \to X \in {Base}_{K}$
24		simpl3	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X <_{K} Y) \to Y \in V$
25	21 4	lvolbase	$⊢ Y \in V \to Y \in {Base}_{K}$
26	24 25	syl	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X <_{K} Y) \to Y \in {Base}_{K}$
27		simpr	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X <_{K} Y) \to X <_{K} Y$
28		eqid	$⊢ join (K) = join (K)$
29		eqid	$⊢ Atoms (K) = Atoms (K)$
30	21 1 15 28 2 29	hlrelat3	$⊢ ((K \in HL \land X \in {Base}_{K} \land Y \in {Base}_{K}) \land X <_{K} Y) \to \exists s \in Atoms (K) (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y)$
31	19 23 26 27 30	syl31anc	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X <_{K} Y) \to \exists s \in Atoms (K) (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y)$
32	21 1 28 29 4	islvol2	$⊢ K \in HL \to (Y \in V \leftrightarrow (Y \in {Base}_{K} \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) \exists w \in Atoms (K) ((t \neq u \land \neg v \underset{˙}{\leq} (t join (K) u) \land \neg w \underset{˙}{\leq} ((t join (K) u) join (K) v)) \land Y = ((t join (K) u) join (K) v) join (K) w)))$
33	32	adantr	$⊢ (K \in HL \land X \in P) \to (Y \in V \leftrightarrow (Y \in {Base}_{K} \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) \exists w \in Atoms (K) ((t \neq u \land \neg v \underset{˙}{\leq} (t join (K) u) \land \neg w \underset{˙}{\leq} ((t join (K) u) join (K) v)) \land Y = ((t join (K) u) join (K) v) join (K) w)))$
34		simpr	$⊢ ((t \neq u \land \neg v \underset{˙}{\leq} (t join (K) u) \land \neg w \underset{˙}{\leq} ((t join (K) u) join (K) v)) \land Y = ((t join (K) u) join (K) v) join (K) w) \to Y = ((t join (K) u) join (K) v) join (K) w$
35	21 1 28 29 3	islpln2	$⊢ K \in HL \to (X \in P \leftrightarrow (X \in {Base}_{K} \land \exists p \in Atoms (K) \exists q \in Atoms (K) \exists r \in Atoms (K) (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)))$
36		simp3rl	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to X C (X join (K) s)$
37		simp3rr	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to (X join (K) s) \underset{˙}{\leq} Y$
38		simp133	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to X = (p join (K) q) join (K) r$
39	38	oveq1d	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to X join (K) s = ((p join (K) q) join (K) r) join (K) s$
40		simp23	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to Y = ((t join (K) u) join (K) v) join (K) w$
41	37 39 40	3brtr3d	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to (((p join (K) q) join (K) r) join (K) s) \underset{˙}{\leq} (((t join (K) u) join (K) v) join (K) w)$
42		simp11	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to (K \in HL \land p \in Atoms (K) \land q \in Atoms (K))$
43		simp12	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to r \in Atoms (K)$
44		simp3l	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to s \in Atoms (K)$
45		simp21l	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to t \in Atoms (K)$
46	43 44 45	3jca	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to (r \in Atoms (K) \land s \in Atoms (K) \land t \in Atoms (K))$
47		simp21r	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to u \in Atoms (K)$
48		simp22l	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to v \in Atoms (K)$
49		simp22r	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to w \in Atoms (K)$
50	47 48 49	3jca	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to (u \in Atoms (K) \land v \in Atoms (K) \land w \in Atoms (K))$
51		simp131	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to p \neq q$
52		simp132	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to \neg r \underset{˙}{\leq} (p join (K) q)$
53	36 38 39	3brtr3d	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to ((p join (K) q) join (K) r) C (((p join (K) q) join (K) r) join (K) s)$
54		simp111	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to K \in HL$
55	54	hllatd	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to K \in Lat$
56	21 28 29	hlatjcl	$⊢ (K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \to p join (K) q \in {Base}_{K}$
57	42 56	syl	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to p join (K) q \in {Base}_{K}$
58	21 29	atbase	$⊢ r \in Atoms (K) \to r \in {Base}_{K}$
59	43 58	syl	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to r \in {Base}_{K}$
60	21 28	latjcl	$⊢ (K \in Lat \land p join (K) q \in {Base}_{K} \land r \in {Base}_{K}) \to (p join (K) q) join (K) r \in {Base}_{K}$
61	55 57 59 60	syl3anc	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to (p join (K) q) join (K) r \in {Base}_{K}$
62	21 1 28 2 29	cvr1	$⊢ (K \in HL \land (p join (K) q) join (K) r \in {Base}_{K} \land s \in Atoms (K)) \to (\neg s \underset{˙}{\leq} ((p join (K) q) join (K) r) \leftrightarrow ((p join (K) q) join (K) r) C (((p join (K) q) join (K) r) join (K) s))$
63	54 61 44 62	syl3anc	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to (\neg s \underset{˙}{\leq} ((p join (K) q) join (K) r) \leftrightarrow ((p join (K) q) join (K) r) C (((p join (K) q) join (K) r) join (K) s))$
64	53 63	mpbird	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to \neg s \underset{˙}{\leq} ((p join (K) q) join (K) r)$
65	1 28 29	4at2	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (r \in Atoms (K) \land s \in Atoms (K) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K) \land w \in Atoms (K))) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land \neg s \underset{˙}{\leq} ((p join (K) q) join (K) r))) \to ((((p join (K) q) join (K) r) join (K) s) \underset{˙}{\leq} (((t join (K) u) join (K) v) join (K) w) \leftrightarrow ((p join (K) q) join (K) r) join (K) s = ((t join (K) u) join (K) v) join (K) w)$
66	42 46 50 51 52 64 65	syl33anc	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to ((((p join (K) q) join (K) r) join (K) s) \underset{˙}{\leq} (((t join (K) u) join (K) v) join (K) w) \leftrightarrow ((p join (K) q) join (K) r) join (K) s = ((t join (K) u) join (K) v) join (K) w)$
67	41 66	mpbid	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to ((p join (K) q) join (K) r) join (K) s = ((t join (K) u) join (K) v) join (K) w$
68	67 39 40	3eqtr4d	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to X join (K) s = Y$
69	36 68	breqtrd	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \land ((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \land (s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y))) \to X C Y$
70	69	3exp	$⊢ ((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \to (((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \to ((s \in Atoms (K) \land (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y)) \to X C Y))$
71	70	exp4a	$⊢ ((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \to (((t \in Atoms (K) \land u \in Atoms (K)) \land (v \in Atoms (K) \land w \in Atoms (K)) \land Y = ((t join (K) u) join (K) v) join (K) w) \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y)))$
72	71	3expd	$⊢ ((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land r \in Atoms (K) \land (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \to ((t \in Atoms (K) \land u \in Atoms (K)) \to ((v \in Atoms (K) \land w \in Atoms (K)) \to (Y = ((t join (K) u) join (K) v) join (K) w \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y)))))$
73	72	rexlimdv3a	$⊢ (K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \to (\exists r \in Atoms (K) (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r) \to ((t \in Atoms (K) \land u \in Atoms (K)) \to ((v \in Atoms (K) \land w \in Atoms (K)) \to (Y = ((t join (K) u) join (K) v) join (K) w \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y))))))$
74	73	3expib	$⊢ K \in HL \to ((p \in Atoms (K) \land q \in Atoms (K)) \to (\exists r \in Atoms (K) (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r) \to ((t \in Atoms (K) \land u \in Atoms (K)) \to ((v \in Atoms (K) \land w \in Atoms (K)) \to (Y = ((t join (K) u) join (K) v) join (K) w \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y)))))))$
75	74	rexlimdvv	$⊢ K \in HL \to (\exists p \in Atoms (K) \exists q \in Atoms (K) \exists r \in Atoms (K) (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r) \to ((t \in Atoms (K) \land u \in Atoms (K)) \to ((v \in Atoms (K) \land w \in Atoms (K)) \to (Y = ((t join (K) u) join (K) v) join (K) w \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y))))))$
76	75	adantld	$⊢ K \in HL \to ((X \in {Base}_{K} \land \exists p \in Atoms (K) \exists q \in Atoms (K) \exists r \in Atoms (K) (p \neq q \land \neg r \underset{˙}{\leq} (p join (K) q) \land X = (p join (K) q) join (K) r)) \to ((t \in Atoms (K) \land u \in Atoms (K)) \to ((v \in Atoms (K) \land w \in Atoms (K)) \to (Y = ((t join (K) u) join (K) v) join (K) w \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y))))))$
77	35 76	sylbid	$⊢ K \in HL \to (X \in P \to ((t \in Atoms (K) \land u \in Atoms (K)) \to ((v \in Atoms (K) \land w \in Atoms (K)) \to (Y = ((t join (K) u) join (K) v) join (K) w \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y))))))$
78	77	imp31	$⊢ ((K \in HL \land X \in P) \land (t \in Atoms (K) \land u \in Atoms (K))) \to ((v \in Atoms (K) \land w \in Atoms (K)) \to (Y = ((t join (K) u) join (K) v) join (K) w \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y))))$
79	34 78	syl7	$⊢ ((K \in HL \land X \in P) \land (t \in Atoms (K) \land u \in Atoms (K))) \to ((v \in Atoms (K) \land w \in Atoms (K)) \to (((t \neq u \land \neg v \underset{˙}{\leq} (t join (K) u) \land \neg w \underset{˙}{\leq} ((t join (K) u) join (K) v)) \land Y = ((t join (K) u) join (K) v) join (K) w) \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y))))$
80	79	rexlimdvv	$⊢ ((K \in HL \land X \in P) \land (t \in Atoms (K) \land u \in Atoms (K))) \to (\exists v \in Atoms (K) \exists w \in Atoms (K) ((t \neq u \land \neg v \underset{˙}{\leq} (t join (K) u) \land \neg w \underset{˙}{\leq} ((t join (K) u) join (K) v)) \land Y = ((t join (K) u) join (K) v) join (K) w) \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y)))$
81	80	rexlimdvva	$⊢ (K \in HL \land X \in P) \to (\exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) \exists w \in Atoms (K) ((t \neq u \land \neg v \underset{˙}{\leq} (t join (K) u) \land \neg w \underset{˙}{\leq} ((t join (K) u) join (K) v)) \land Y = ((t join (K) u) join (K) v) join (K) w) \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y)))$
82	81	adantld	$⊢ (K \in HL \land X \in P) \to ((Y \in {Base}_{K} \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) \exists w \in Atoms (K) ((t \neq u \land \neg v \underset{˙}{\leq} (t join (K) u) \land \neg w \underset{˙}{\leq} ((t join (K) u) join (K) v)) \land Y = ((t join (K) u) join (K) v) join (K) w)) \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y)))$
83	33 82	sylbid	$⊢ (K \in HL \land X \in P) \to (Y \in V \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y)))$
84	83	3impia	$⊢ (K \in HL \land X \in P \land Y \in V) \to (s \in Atoms (K) \to ((X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y))$
85	84	rexlimdv	$⊢ (K \in HL \land X \in P \land Y \in V) \to (\exists s \in Atoms (K) (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y) \to X C Y)$
86	85	imp	$⊢ ((K \in HL \land X \in P \land Y \in V) \land \exists s \in Atoms (K) (X C (X join (K) s) \land (X join (K) s) \underset{˙}{\leq} Y)) \to X C Y$
87	31 86	syldan	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X <_{K} Y) \to X C Y$
88	18 87	syldan	$⊢ ((K \in HL \land X \in P \land Y \in V) \land X \underset{˙}{\leq} Y) \to X C Y$

Metamath Proof Explorer

Theorem lplncvrlvol2

Proof