1cvrat

Description: Create an atom under an element covered by the lattice unity. Part of proof of Lemma B in Crawley p. 112. (Contributed by NM, 30-Apr-2012)

	Ref	Expression
Hypotheses	1cvrat.b	$⊢ B = {Base}_{K}$
	1cvrat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	1cvrat.j	$⊢ \underset{˙}{\lor} = join (K)$
	1cvrat.m	$⊢ \underset{˙}{\land} = meet (K)$
	1cvrat.u	$⊢ \underset{˙}{1} = 1. (K)$
	1cvrat.c	$⊢ C = ⋖_{K}$
	1cvrat.a	$⊢ A = Atoms (K)$
Assertion	1cvrat	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X \in A$

Proof

Step	Hyp	Ref	Expression
1		1cvrat.b	$⊢ B = {Base}_{K}$
2		1cvrat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		1cvrat.j	$⊢ \underset{˙}{\lor} = join (K)$
4		1cvrat.m	$⊢ \underset{˙}{\land} = meet (K)$
5		1cvrat.u	$⊢ \underset{˙}{1} = 1. (K)$
6		1cvrat.c	$⊢ C = ⋖_{K}$
7		1cvrat.a	$⊢ A = Atoms (K)$
8		hllat	$⊢ K \in HL \to K \in Lat$
9	8	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to K \in Lat$
10		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to P \in A$
11	1 7	atbase	$⊢ P \in A \to P \in B$
12	10 11	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to P \in B$
13		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to Q \in A$
14	1 7	atbase	$⊢ Q \in A \to Q \in B$
15	13 14	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to Q \in B$
16	1 3	latjcom	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
17	9 12 15 16	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
18	17	oveq1d	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X = (Q \underset{˙}{\lor} P) \underset{˙}{\land} X$
19	1 3	latjcl	$⊢ (K \in Lat \land Q \in B \land P \in B) \to Q \underset{˙}{\lor} P \in B$
20	9 15 12 19	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to Q \underset{˙}{\lor} P \in B$
21		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to X \in B$
22	1 4	latmcom	$⊢ (K \in Lat \land Q \underset{˙}{\lor} P \in B \land X \in B) \to (Q \underset{˙}{\lor} P) \underset{˙}{\land} X = X \underset{˙}{\land} (Q \underset{˙}{\lor} P)$
23	9 20 21 22	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (Q \underset{˙}{\lor} P) \underset{˙}{\land} X = X \underset{˙}{\land} (Q \underset{˙}{\lor} P)$
24	18 23	eqtrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X = X \underset{˙}{\land} (Q \underset{˙}{\lor} P)$
25		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to K \in HL$
26	21 13 10	3jca	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (X \in B \land Q \in A \land P \in A)$
27		simp31	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to P \neq Q$
28	27	necomd	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to Q \neq P$
29		simp33	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to \neg P \underset{˙}{\leq} X$
30		hlop	$⊢ K \in HL \to K \in OP$
31	30	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to K \in OP$
32	1 2 5	ople1	$⊢ (K \in OP \land Q \in B) \to Q \underset{˙}{\leq} \underset{˙}{1}$
33	31 15 32	syl2anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to Q \underset{˙}{\leq} \underset{˙}{1}$
34		simp32	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to X C \underset{˙}{1}$
35	1 2 3 5 6 7	1cvrjat	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to X \underset{˙}{\lor} P = \underset{˙}{1}$
36	25 21 10 34 29 35	syl32anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to X \underset{˙}{\lor} P = \underset{˙}{1}$
37	33 36	breqtrrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to Q \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
38	1 2 3 4 7	cvrat3	$⊢ (K \in HL \land (X \in B \land Q \in A \land P \in A)) \to ((Q \neq P \land \neg P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \to X \underset{˙}{\land} (Q \underset{˙}{\lor} P) \in A)$
39	38	imp	$⊢ ((K \in HL \land (X \in B \land Q \in A \land P \in A)) \land (Q \neq P \land \neg P \underset{˙}{\leq} X \land Q \underset{˙}{\leq} (X \underset{˙}{\lor} P))) \to X \underset{˙}{\land} (Q \underset{˙}{\lor} P) \in A$
40	25 26 28 29 37 39	syl23anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to X \underset{˙}{\land} (Q \underset{˙}{\lor} P) \in A$
41	24 40	eqeltrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land (P \neq Q \land X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} X \in A$

Metamath Proof Explorer

Theorem 1cvrat

Proof