2lplnj

Description: The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012)

	Ref	Expression
Hypotheses	2lplnj.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2lplnj.j	$⊢ \underset{˙}{\lor} = join (K)$
	2lplnj.p	$⊢ P = LPlanes (K)$
	2lplnj.v	$⊢ V = LVols (K)$
Assertion	2lplnj	$⊢ (K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to X \underset{˙}{\lor} Y = W$

Proof

Step	Hyp	Ref	Expression
1		2lplnj.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2lplnj.j	$⊢ \underset{˙}{\lor} = join (K)$
3		2lplnj.p	$⊢ P = LPlanes (K)$
4		2lplnj.v	$⊢ V = LVols (K)$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ Atoms (K) = Atoms (K)$
7	5 1 2 6 3	islpln2	$⊢ K \in HL \to (X \in P \leftrightarrow (X \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)))$
8		simpr	$⊢ (X \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to \exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)$
9	7 8	biimtrdi	$⊢ K \in HL \to (X \in P \to \exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s))$
10	5 1 2 6 3	islpln2	$⊢ K \in HL \to (Y \in P \leftrightarrow (Y \in {Base}_{K} \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)))$
11		simpr	$⊢ (Y \in {Base}_{K} \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
12	10 11	biimtrdi	$⊢ K \in HL \to (Y \in P \to \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
13	9 12	anim12d	$⊢ K \in HL \to ((X \in P \land Y \in P) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)))$
14	13	imp	$⊢ (K \in HL \land (X \in P \land Y \in P)) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
15	14	3adantr3	$⊢ (K \in HL \land (X \in P \land Y \in P \land W \in V)) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
16	15	3adant3	$⊢ (K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
17		simpl33	$⊢ (((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \to X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s$
18	17	3ad2ant1	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s$
19		simp33	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v$
20	18 19	oveq12d	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to X \underset{˙}{\lor} Y = ((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\lor} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
21		simp11	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to K \in HL$
22		simp123	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to W \in V$
23	21 22	jca	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to (K \in HL \land W \in V)$
24	23	adantr	$⊢ (((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \to (K \in HL \land W \in V)$
25	24	3ad2ant1	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (K \in HL \land W \in V)$
26		simp2l	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to q \in Atoms (K)$
27		simp2rl	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to r \in Atoms (K)$
28		simp2rr	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to s \in Atoms (K)$
29	26 27 28	3jca	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to (q \in Atoms (K) \land r \in Atoms (K) \land s \in Atoms (K))$
30	29	adantr	$⊢ (((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \to (q \in Atoms (K) \land r \in Atoms (K) \land s \in Atoms (K))$
31	30	3ad2ant1	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (q \in Atoms (K) \land r \in Atoms (K) \land s \in Atoms (K))$
32		simpl31	$⊢ (((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \to q \neq r$
33	32	3ad2ant1	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to q \neq r$
34		simpl32	$⊢ (((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \to \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r)$
35	34	3ad2ant1	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r)$
36	33 35	jca	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r))$
37		simp1r	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to t \in Atoms (K)$
38		simp2l	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to u \in Atoms (K)$
39		simp2r	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to v \in Atoms (K)$
40	37 38 39	3jca	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (t \in Atoms (K) \land u \in Atoms (K) \land v \in Atoms (K))$
41		simp31	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to t \neq u$
42		simp32	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u)$
43	41 42	jca	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u))$
44		simpl13	$⊢ (((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \to (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)$
45	44	3ad2ant1	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)$
46		breq1	$⊢ X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \to (X \underset{˙}{\leq} W \leftrightarrow ((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\leq} W)$
47		neeq1	$⊢ X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \to (X \neq Y \leftrightarrow (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq Y)$
48	46 47	3anbi13d	$⊢ X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \to ((X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y) \leftrightarrow (((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq Y))$
49		breq1	$⊢ Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v \to (Y \underset{˙}{\leq} W \leftrightarrow ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \underset{˙}{\leq} W)$
50		neeq2	$⊢ Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v \to ((q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq Y \leftrightarrow (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
51	49 50	3anbi23d	$⊢ Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v \to ((((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq Y) \leftrightarrow (((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\leq} W \land ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \underset{˙}{\leq} W \land (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq (t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
52	48 51	sylan9bb	$⊢ (X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \to ((X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y) \leftrightarrow (((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\leq} W \land ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \underset{˙}{\leq} W \land (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq (t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
53	18 19 52	syl2anc	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to ((X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y) \leftrightarrow (((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\leq} W \land ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \underset{˙}{\leq} W \land (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq (t \underset{˙}{\lor} u) \underset{˙}{\lor} v))$
54	45 53	mpbid	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to (((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\leq} W \land ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \underset{˙}{\leq} W \land (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)$
55	1 2 6 4	2lplnja	$⊢ (((K \in HL \land W \in V) \land (q \in Atoms (K) \land r \in Atoms (K) \land s \in Atoms (K)) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \land ((t \in Atoms (K) \land u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u))) \land (((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\leq} W \land ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \underset{˙}{\leq} W \land (q \underset{˙}{\lor} r) \underset{˙}{\lor} s \neq (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to ((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\lor} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v) = W$
56	25 31 36 40 43 54 55	syl321anc	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to ((q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \underset{˙}{\lor} ((t \underset{˙}{\lor} u) \underset{˙}{\lor} v) = W$
57	20 56	eqtrd	$⊢ ((((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \land (u \in Atoms (K) \land v \in Atoms (K)) \land (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to X \underset{˙}{\lor} Y = W$
58	57	3exp	$⊢ (((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \to ((u \in Atoms (K) \land v \in Atoms (K)) \to ((t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \to X \underset{˙}{\lor} Y = W))$
59	58	rexlimdvv	$⊢ (((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \land t \in Atoms (K)) \to (\exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \to X \underset{˙}{\lor} Y = W)$
60	59	rexlimdva	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land (q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \land (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s)) \to (\exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \to X \underset{˙}{\lor} Y = W)$
61	60	3exp	$⊢ (K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to ((q \in Atoms (K) \land (r \in Atoms (K) \land s \in Atoms (K))) \to ((q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \to (\exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \to X \underset{˙}{\lor} Y = W)))$
62	61	expdimp	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land q \in Atoms (K)) \to ((r \in Atoms (K) \land s \in Atoms (K)) \to ((q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \to (\exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \to X \underset{˙}{\lor} Y = W)))$
63	62	rexlimdvv	$⊢ ((K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \land q \in Atoms (K)) \to (\exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \to (\exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \to X \underset{˙}{\lor} Y = W))$
64	63	rexlimdva	$⊢ (K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \to (\exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v) \to X \underset{˙}{\lor} Y = W))$
65	64	impd	$⊢ (K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to ((\exists q \in Atoms (K) \exists r \in Atoms (K) \exists s \in Atoms (K) (q \neq r \land \neg s \underset{˙}{\leq} (q \underset{˙}{\lor} r) \land X = (q \underset{˙}{\lor} r) \underset{˙}{\lor} s) \land \exists t \in Atoms (K) \exists u \in Atoms (K) \exists v \in Atoms (K) (t \neq u \land \neg v \underset{˙}{\leq} (t \underset{˙}{\lor} u) \land Y = (t \underset{˙}{\lor} u) \underset{˙}{\lor} v)) \to X \underset{˙}{\lor} Y = W)$
66	16 65	mpd	$⊢ (K \in HL \land (X \in P \land Y \in P \land W \in V) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to X \underset{˙}{\lor} Y = W$

Metamath Proof Explorer

Theorem 2lplnj

Proof