2llnjN

Description: The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	2llnj.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2llnj.j	$⊢ \underset{˙}{\lor} = join (K)$
	2llnj.n	$⊢ N = LLines (K)$
	2llnj.p	$⊢ P = LPlanes (K)$
Assertion	2llnjN	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \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		2llnj.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2llnj.j	$⊢ \underset{˙}{\lor} = join (K)$
3		2llnj.n	$⊢ N = LLines (K)$
4		2llnj.p	$⊢ P = LPlanes (K)$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ Atoms (K) = Atoms (K)$
7	5 2 6 3	islln2	$⊢ K \in HL \to (X \in N \leftrightarrow (X \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land X = q \underset{˙}{\lor} r)))$
8		simpr	$⊢ (X \in {Base}_{K} \land \exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land X = q \underset{˙}{\lor} r)) \to \exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land X = q \underset{˙}{\lor} r)$
9	7 8	syl6bi	$⊢ K \in HL \to (X \in N \to \exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land X = q \underset{˙}{\lor} r))$
10	5 2 6 3	islln2	$⊢ K \in HL \to (Y \in N \leftrightarrow (Y \in {Base}_{K} \land \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t)))$
11		simpr	$⊢ (Y \in {Base}_{K} \land \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t)) \to \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t)$
12	10 11	syl6bi	$⊢ K \in HL \to (Y \in N \to \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t))$
13	9 12	anim12d	$⊢ K \in HL \to ((X \in N \land Y \in N) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land X = q \underset{˙}{\lor} r) \land \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t)))$
14	13	imp	$⊢ (K \in HL \land (X \in N \land Y \in N)) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land X = q \underset{˙}{\lor} r) \land \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t))$
15	14	3adantr3	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P)) \to (\exists q \in Atoms (K) \exists r \in Atoms (K) (q \neq r \land X = q \underset{˙}{\lor} r) \land \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t))$
16	15	3adant3	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \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) (q \neq r \land X = q \underset{˙}{\lor} r) \land \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t))$
17		simp2rr	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to X = q \underset{˙}{\lor} r$
18		simp3rr	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to Y = s \underset{˙}{\lor} t$
19	17 18	oveq12d	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to X \underset{˙}{\lor} Y = (q \underset{˙}{\lor} r) \underset{˙}{\lor} (s \underset{˙}{\lor} t)$
20		simp13	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)$
21		breq1	$⊢ X = q \underset{˙}{\lor} r \to (X \underset{˙}{\leq} W \leftrightarrow (q \underset{˙}{\lor} r) \underset{˙}{\leq} W)$
22		neeq1	$⊢ X = q \underset{˙}{\lor} r \to (X \neq Y \leftrightarrow q \underset{˙}{\lor} r \neq Y)$
23	21 22	3anbi13d	$⊢ X = q \underset{˙}{\lor} r \to ((X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y) \leftrightarrow ((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq Y))$
24		breq1	$⊢ Y = s \underset{˙}{\lor} t \to (Y \underset{˙}{\leq} W \leftrightarrow (s \underset{˙}{\lor} t) \underset{˙}{\leq} W)$
25		neeq2	$⊢ Y = s \underset{˙}{\lor} t \to (q \underset{˙}{\lor} r \neq Y \leftrightarrow q \underset{˙}{\lor} r \neq s \underset{˙}{\lor} t)$
26	24 25	3anbi23d	$⊢ Y = s \underset{˙}{\lor} t \to (((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq Y) \leftrightarrow ((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land (s \underset{˙}{\lor} t) \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq s \underset{˙}{\lor} t))$
27	23 26	sylan9bb	$⊢ (X = q \underset{˙}{\lor} r \land Y = s \underset{˙}{\lor} t) \to ((X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y) \leftrightarrow ((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land (s \underset{˙}{\lor} t) \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq s \underset{˙}{\lor} t))$
28	17 18 27	syl2anc	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to ((X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y) \leftrightarrow ((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land (s \underset{˙}{\lor} t) \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq s \underset{˙}{\lor} t))$
29	20 28	mpbid	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to ((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land (s \underset{˙}{\lor} t) \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq s \underset{˙}{\lor} t)$
30		simp11	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to K \in HL$
31		simp123	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to W \in P$
32		simp2ll	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to q \in Atoms (K)$
33		simp2lr	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to r \in Atoms (K)$
34		simp2rl	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to q \neq r$
35		simp3ll	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to s \in Atoms (K)$
36		simp3lr	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to t \in Atoms (K)$
37		simp3rl	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to s \neq t$
38	1 2 6 3 4	2llnjaN	$⊢ (((K \in HL \land W \in P) \land (q \in Atoms (K) \land r \in Atoms (K) \land q \neq r) \land (s \in Atoms (K) \land t \in Atoms (K) \land s \neq t)) \land ((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land (s \underset{˙}{\lor} t) \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq s \underset{˙}{\lor} t)) \to (q \underset{˙}{\lor} r) \underset{˙}{\lor} (s \underset{˙}{\lor} t) = W$
39	38	ex	$⊢ ((K \in HL \land W \in P) \land (q \in Atoms (K) \land r \in Atoms (K) \land q \neq r) \land (s \in Atoms (K) \land t \in Atoms (K) \land s \neq t)) \to (((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land (s \underset{˙}{\lor} t) \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq s \underset{˙}{\lor} t) \to (q \underset{˙}{\lor} r) \underset{˙}{\lor} (s \underset{˙}{\lor} t) = W)$
40	30 31 32 33 34 35 36 37 39	syl233anc	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to (((q \underset{˙}{\lor} r) \underset{˙}{\leq} W \land (s \underset{˙}{\lor} t) \underset{˙}{\leq} W \land q \underset{˙}{\lor} r \neq s \underset{˙}{\lor} t) \to (q \underset{˙}{\lor} r) \underset{˙}{\lor} (s \underset{˙}{\lor} t) = W)$
41	29 40	mpd	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to (q \underset{˙}{\lor} r) \underset{˙}{\lor} (s \underset{˙}{\lor} t) = W$
42	19 41	eqtrd	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \land ((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t))) \to X \underset{˙}{\lor} Y = W$
43	42	3exp	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \to (((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t)) \to X \underset{˙}{\lor} Y = W))$
44	43	3impib	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \to (((s \in Atoms (K) \land t \in Atoms (K)) \land (s \neq t \land Y = s \underset{˙}{\lor} t)) \to X \underset{˙}{\lor} Y = W)$
45	44	expd	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \to ((s \in Atoms (K) \land t \in Atoms (K)) \to ((s \neq t \land Y = s \underset{˙}{\lor} t) \to X \underset{˙}{\lor} Y = W))$
46	45	rexlimdvv	$⊢ ((K \in HL \land (X \in N \land Y \in N \land W \in P) \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 (q \neq r \land X = q \underset{˙}{\lor} r)) \to (\exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t) \to X \underset{˙}{\lor} Y = W)$
47	46	3exp	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to ((q \in Atoms (K) \land r \in Atoms (K)) \to ((q \neq r \land X = q \underset{˙}{\lor} r) \to (\exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t) \to X \underset{˙}{\lor} Y = W)))$
48	47	rexlimdvv	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \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) (q \neq r \land X = q \underset{˙}{\lor} r) \to (\exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t) \to X \underset{˙}{\lor} Y = W))$
49	48	impd	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \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) (q \neq r \land X = q \underset{˙}{\lor} r) \land \exists s \in Atoms (K) \exists t \in Atoms (K) (s \neq t \land Y = s \underset{˙}{\lor} t)) \to X \underset{˙}{\lor} Y = W)$
50	16 49	mpd	$⊢ (K \in HL \land (X \in N \land Y \in N \land W \in P) \land (X \underset{˙}{\leq} W \land Y \underset{˙}{\leq} W \land X \neq Y)) \to X \underset{˙}{\lor} Y = W$

Metamath Proof Explorer

Theorem 2llnjN

Proof