lplnexllnN

Description: Given an atom on a lattice plane, there is a lattice line whose join with the atom equals the plane. (Contributed by NM, 26-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lplnexat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lplnexat.j	$⊢ \underset{˙}{\lor} = join (K)$
	lplnexat.a	$⊢ A = Atoms (K)$
	lplnexat.n	$⊢ N = LLines (K)$
	lplnexat.p	$⊢ P = LPlanes (K)$
Assertion	lplnexllnN	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)$

Proof

Step	Hyp	Ref	Expression
1		lplnexat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lplnexat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		lplnexat.a	$⊢ A = Atoms (K)$
4		lplnexat.n	$⊢ N = LLines (K)$
5		lplnexat.p	$⊢ P = LPlanes (K)$
6		simpl2	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to X \in P$
7		simpl1	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to K \in HL$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 5	lplnbase	$⊢ X \in P \to X \in {Base}_{K}$
10	6 9	syl	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to X \in {Base}_{K}$
11	8 1 2 3 4 5	islpln3	$⊢ (K \in HL \land X \in {Base}_{K}) \to (X \in P \leftrightarrow \exists z \in N \exists r \in A (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))$
12	7 10 11	syl2anc	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to (X \in P \leftrightarrow \exists z \in N \exists r \in A (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))$
13	6 12	mpbid	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to \exists z \in N \exists r \in A (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)$
14		simpll1	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to K \in HL$
15		simpr2l	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z \in N$
16		simpll3	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to Q \in A$
17		simpr1	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to Q \underset{˙}{\leq} z$
18	1 2 3 4	llnexatN	$⊢ ((K \in HL \land z \in N \land Q \in A) \land Q \underset{˙}{\leq} z) \to \exists s \in A (Q \neq s \land z = Q \underset{˙}{\lor} s)$
19	14 15 16 17 18	syl31anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to \exists s \in A (Q \neq s \land z = Q \underset{˙}{\lor} s)$
20		simp1l1	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to K \in HL$
21		simp22r	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to r \in A$
22		simp3l	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to s \in A$
23		simp1l3	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to Q \in A$
24		simp23l	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to \neg r \underset{˙}{\leq} z$
25		simp3rr	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to z = Q \underset{˙}{\lor} s$
26	25	breq2d	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to (r \underset{˙}{\leq} z \leftrightarrow r \underset{˙}{\leq} (Q \underset{˙}{\lor} s))$
27	24 26	mtbid	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to \neg r \underset{˙}{\leq} (Q \underset{˙}{\lor} s)$
28	1 2 3	atnlej2	$⊢ (K \in HL \land (r \in A \land Q \in A \land s \in A) \land \neg r \underset{˙}{\leq} (Q \underset{˙}{\lor} s)) \to r \neq s$
29	20 21 23 22 27 28	syl131anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to r \neq s$
30	2 3 4	llni2	$⊢ ((K \in HL \land r \in A \land s \in A) \land r \neq s) \to r \underset{˙}{\lor} s \in N$
31	20 21 22 29 30	syl31anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to r \underset{˙}{\lor} s \in N$
32		simp3rl	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to Q \neq s$
33	1 2 3	hlatcon2	$⊢ (K \in HL \land (Q \in A \land s \in A \land r \in A) \land (Q \neq s \land \neg r \underset{˙}{\leq} (Q \underset{˙}{\lor} s))) \to \neg Q \underset{˙}{\leq} (r \underset{˙}{\lor} s)$
34	20 23 22 21 32 27 33	syl132anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to \neg Q \underset{˙}{\leq} (r \underset{˙}{\lor} s)$
35		simp23r	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to X = z \underset{˙}{\lor} r$
36	25	oveq1d	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to z \underset{˙}{\lor} r = (Q \underset{˙}{\lor} s) \underset{˙}{\lor} r$
37	20	hllatd	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to K \in Lat$
38	8 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
39	23 38	syl	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to Q \in {Base}_{K}$
40	8 3	atbase	$⊢ s \in A \to s \in {Base}_{K}$
41	22 40	syl	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to s \in {Base}_{K}$
42	8 3	atbase	$⊢ r \in A \to r \in {Base}_{K}$
43	21 42	syl	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to r \in {Base}_{K}$
44	8 2	latj31	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land s \in {Base}_{K} \land r \in {Base}_{K})) \to (Q \underset{˙}{\lor} s) \underset{˙}{\lor} r = (r \underset{˙}{\lor} s) \underset{˙}{\lor} Q$
45	37 39 41 43 44	syl13anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to (Q \underset{˙}{\lor} s) \underset{˙}{\lor} r = (r \underset{˙}{\lor} s) \underset{˙}{\lor} Q$
46	35 36 45	3eqtrd	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to X = (r \underset{˙}{\lor} s) \underset{˙}{\lor} Q$
47		breq2	$⊢ y = r \underset{˙}{\lor} s \to (Q \underset{˙}{\leq} y \leftrightarrow Q \underset{˙}{\leq} (r \underset{˙}{\lor} s))$
48	47	notbid	$⊢ y = r \underset{˙}{\lor} s \to (\neg Q \underset{˙}{\leq} y \leftrightarrow \neg Q \underset{˙}{\leq} (r \underset{˙}{\lor} s))$
49		oveq1	$⊢ y = r \underset{˙}{\lor} s \to y \underset{˙}{\lor} Q = (r \underset{˙}{\lor} s) \underset{˙}{\lor} Q$
50	49	eqeq2d	$⊢ y = r \underset{˙}{\lor} s \to (X = y \underset{˙}{\lor} Q \leftrightarrow X = (r \underset{˙}{\lor} s) \underset{˙}{\lor} Q)$
51	48 50	anbi12d	$⊢ y = r \underset{˙}{\lor} s \to ((\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q) \leftrightarrow (\neg Q \underset{˙}{\leq} (r \underset{˙}{\lor} s) \land X = (r \underset{˙}{\lor} s) \underset{˙}{\lor} Q))$
52	51	rspcev	$⊢ (r \underset{˙}{\lor} s \in N \land (\neg Q \underset{˙}{\leq} (r \underset{˙}{\lor} s) \land X = (r \underset{˙}{\lor} s) \underset{˙}{\lor} Q)) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)$
53	31 34 46 52	syl12anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r)) \land (s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s))) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)$
54	53	3expia	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to ((s \in A \land (Q \neq s \land z = Q \underset{˙}{\lor} s)) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q))$
55	54	expd	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to (s \in A \to ((Q \neq s \land z = Q \underset{˙}{\lor} s) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)))$
56	55	rexlimdv	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to (\exists s \in A (Q \neq s \land z = Q \underset{˙}{\lor} s) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q))$
57	19 56	mpd	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)$
58	57	3exp2	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to (Q \underset{˙}{\leq} z \to ((z \in N \land r \in A) \to ((\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q))))$
59		simpr2l	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z \in N$
60		simpr1	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to \neg Q \underset{˙}{\leq} z$
61		simpll1	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to K \in HL$
62	61	hllatd	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to K \in Lat$
63	8 4	llnbase	$⊢ z \in N \to z \in {Base}_{K}$
64	59 63	syl	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z \in {Base}_{K}$
65		simpr2r	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to r \in A$
66	65 42	syl	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to r \in {Base}_{K}$
67	8 1 2	latlej1	$⊢ (K \in Lat \land z \in {Base}_{K} \land r \in {Base}_{K}) \to z \underset{˙}{\leq} (z \underset{˙}{\lor} r)$
68	62 64 66 67	syl3anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z \underset{˙}{\leq} (z \underset{˙}{\lor} r)$
69		simpr3r	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to X = z \underset{˙}{\lor} r$
70	68 69	breqtrrd	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z \underset{˙}{\leq} X$
71		simplr	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to Q \underset{˙}{\leq} X$
72		simpll3	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to Q \in A$
73	72 38	syl	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to Q \in {Base}_{K}$
74		simpll2	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to X \in P$
75	74 9	syl	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to X \in {Base}_{K}$
76	8 1 2	latjle12	$⊢ (K \in Lat \land (z \in {Base}_{K} \land Q \in {Base}_{K} \land X \in {Base}_{K})) \to ((z \underset{˙}{\leq} X \land Q \underset{˙}{\leq} X) \leftrightarrow (z \underset{˙}{\lor} Q) \underset{˙}{\leq} X)$
77	62 64 73 75 76	syl13anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to ((z \underset{˙}{\leq} X \land Q \underset{˙}{\leq} X) \leftrightarrow (z \underset{˙}{\lor} Q) \underset{˙}{\leq} X)$
78	70 71 77	mpbi2and	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to (z \underset{˙}{\lor} Q) \underset{˙}{\leq} X$
79	8 2	latjcl	$⊢ (K \in Lat \land z \in {Base}_{K} \land Q \in {Base}_{K}) \to z \underset{˙}{\lor} Q \in {Base}_{K}$
80	62 64 73 79	syl3anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z \underset{˙}{\lor} Q \in {Base}_{K}$
81		eqid	$⊢ ⋖_{K} = ⋖_{K}$
82	8 1 2 81 3	cvr1	$⊢ (K \in HL \land z \in {Base}_{K} \land Q \in A) \to (\neg Q \underset{˙}{\leq} z \leftrightarrow z ⋖_{K} (z \underset{˙}{\lor} Q))$
83	61 64 72 82	syl3anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to (\neg Q \underset{˙}{\leq} z \leftrightarrow z ⋖_{K} (z \underset{˙}{\lor} Q))$
84	60 83	mpbid	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z ⋖_{K} (z \underset{˙}{\lor} Q)$
85	8 81 4 5	lplni	$⊢ ((K \in HL \land z \underset{˙}{\lor} Q \in {Base}_{K} \land z \in N) \land z ⋖_{K} (z \underset{˙}{\lor} Q)) \to z \underset{˙}{\lor} Q \in P$
86	61 80 59 84 85	syl31anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z \underset{˙}{\lor} Q \in P$
87	1 5	lplncmp	$⊢ (K \in HL \land z \underset{˙}{\lor} Q \in P \land X \in P) \to ((z \underset{˙}{\lor} Q) \underset{˙}{\leq} X \leftrightarrow z \underset{˙}{\lor} Q = X)$
88	61 86 74 87	syl3anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to ((z \underset{˙}{\lor} Q) \underset{˙}{\leq} X \leftrightarrow z \underset{˙}{\lor} Q = X)$
89	78 88	mpbid	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to z \underset{˙}{\lor} Q = X$
90	89	eqcomd	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to X = z \underset{˙}{\lor} Q$
91		breq2	$⊢ y = z \to (Q \underset{˙}{\leq} y \leftrightarrow Q \underset{˙}{\leq} z)$
92	91	notbid	$⊢ y = z \to (\neg Q \underset{˙}{\leq} y \leftrightarrow \neg Q \underset{˙}{\leq} z)$
93		oveq1	$⊢ y = z \to y \underset{˙}{\lor} Q = z \underset{˙}{\lor} Q$
94	93	eqeq2d	$⊢ y = z \to (X = y \underset{˙}{\lor} Q \leftrightarrow X = z \underset{˙}{\lor} Q)$
95	92 94	anbi12d	$⊢ y = z \to ((\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q) \leftrightarrow (\neg Q \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} Q))$
96	95	rspcev	$⊢ (z \in N \land (\neg Q \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} Q)) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)$
97	59 60 90 96	syl12anc	$⊢ (((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \land (\neg Q \underset{˙}{\leq} z \land (z \in N \land r \in A) \land (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r))) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)$
98	97	3exp2	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to (\neg Q \underset{˙}{\leq} z \to ((z \in N \land r \in A) \to ((\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q))))$
99	58 98	pm2.61d	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to ((z \in N \land r \in A) \to ((\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)))$
100	99	rexlimdvv	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to (\exists z \in N \exists r \in A (\neg r \underset{˙}{\leq} z \land X = z \underset{˙}{\lor} r) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q))$
101	13 100	mpd	$⊢ ((K \in HL \land X \in P \land Q \in A) \land Q \underset{˙}{\leq} X) \to \exists y \in N (\neg Q \underset{˙}{\leq} y \land X = y \underset{˙}{\lor} Q)$

Metamath Proof Explorer

Theorem lplnexllnN

Proof