1cvrjat

Description: An element covered by the lattice unit, when joined with an atom not under it, equals the lattice unit. (Contributed by NM, 30-Apr-2012)

	Ref	Expression
Hypotheses	1cvrjat.b	$⊢ B = {Base}_{K}$
	1cvrjat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	1cvrjat.j	$⊢ \underset{˙}{\lor} = join (K)$
	1cvrjat.u	$⊢ \underset{˙}{1} = 1. (K)$
	1cvrjat.c	$⊢ C = ⋖_{K}$
	1cvrjat.a	$⊢ A = Atoms (K)$
Assertion	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}$

Proof

Step	Hyp	Ref	Expression
1		1cvrjat.b	$⊢ B = {Base}_{K}$
2		1cvrjat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		1cvrjat.j	$⊢ \underset{˙}{\lor} = join (K)$
4		1cvrjat.u	$⊢ \underset{˙}{1} = 1. (K)$
5		1cvrjat.c	$⊢ C = ⋖_{K}$
6		1cvrjat.a	$⊢ A = Atoms (K)$
7		simprr	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to \neg P \underset{˙}{\leq} X$
8	1 2 3 5 6	cvr1	$⊢ (K \in HL \land X \in B \land P \in A) \to (\neg P \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} P))$
9	8	adantr	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (\neg P \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} P))$
10	7 9	mpbid	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to X C (X \underset{˙}{\lor} P)$
11		simpl1	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to K \in HL$
12		hlop	$⊢ K \in HL \to K \in OP$
13	11 12	syl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to K \in OP$
14		simpl2	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to X \in B$
15	11	hllatd	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to K \in Lat$
16		simpl3	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to P \in A$
17	1 6	atbase	$⊢ P \in A \to P \in B$
18	16 17	syl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to P \in B$
19	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land P \in B) \to X \underset{˙}{\lor} P \in B$
20	15 14 18 19	syl3anc	$⊢ ((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 \in B$
21		eqid	$⊢ oc (K) = oc (K)$
22	1 21 5	cvrcon3b	$⊢ (K \in OP \land X \in B \land X \underset{˙}{\lor} P \in B) \to (X C (X \underset{˙}{\lor} P) \leftrightarrow oc (K) (X \underset{˙}{\lor} P) C oc (K) (X))$
23	13 14 20 22	syl3anc	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (X C (X \underset{˙}{\lor} P) \leftrightarrow oc (K) (X \underset{˙}{\lor} P) C oc (K) (X))$
24	10 23	mpbid	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (X \underset{˙}{\lor} P) C oc (K) (X)$
25		hlatl	$⊢ K \in HL \to K \in AtLat$
26	11 25	syl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to K \in AtLat$
27	1 21	opoccl	$⊢ (K \in OP \land X \underset{˙}{\lor} P \in B) \to oc (K) (X \underset{˙}{\lor} P) \in B$
28	13 20 27	syl2anc	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (X \underset{˙}{\lor} P) \in B$
29	1 21	opoccl	$⊢ (K \in OP \land X \in B) \to oc (K) (X) \in B$
30	13 14 29	syl2anc	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (X) \in B$
31		eqid	$⊢ 0. (K) = 0. (K)$
32	31 4 21	opoc1	$⊢ K \in OP \to oc (K) (\underset{˙}{1}) = 0. (K)$
33	11 12 32	3syl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (\underset{˙}{1}) = 0. (K)$
34		simprl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to X C \underset{˙}{1}$
35	1 4	op1cl	$⊢ K \in OP \to \underset{˙}{1} \in B$
36	11 12 35	3syl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to \underset{˙}{1} \in B$
37	1 21 5	cvrcon3b	$⊢ (K \in OP \land X \in B \land \underset{˙}{1} \in B) \to (X C \underset{˙}{1} \leftrightarrow oc (K) (\underset{˙}{1}) C oc (K) (X))$
38	13 14 36 37	syl3anc	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (X C \underset{˙}{1} \leftrightarrow oc (K) (\underset{˙}{1}) C oc (K) (X))$
39	34 38	mpbid	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (\underset{˙}{1}) C oc (K) (X)$
40	33 39	eqbrtrrd	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to 0. (K) C oc (K) (X)$
41	1 31 5 6	isat	$⊢ K \in HL \to (oc (K) (X) \in A \leftrightarrow (oc (K) (X) \in B \land 0. (K) C oc (K) (X)))$
42	11 41	syl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (oc (K) (X) \in A \leftrightarrow (oc (K) (X) \in B \land 0. (K) C oc (K) (X)))$
43	30 40 42	mpbir2and	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (X) \in A$
44	1 2 31 5 6	atcvreq0	$⊢ (K \in AtLat \land oc (K) (X \underset{˙}{\lor} P) \in B \land oc (K) (X) \in A) \to (oc (K) (X \underset{˙}{\lor} P) C oc (K) (X) \leftrightarrow oc (K) (X \underset{˙}{\lor} P) = 0. (K))$
45	26 28 43 44	syl3anc	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to (oc (K) (X \underset{˙}{\lor} P) C oc (K) (X) \leftrightarrow oc (K) (X \underset{˙}{\lor} P) = 0. (K))$
46	24 45	mpbid	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (X \underset{˙}{\lor} P) = 0. (K)$
47	46	fveq2d	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (oc (K) (X \underset{˙}{\lor} P)) = oc (K) (0. (K))$
48	1 21	opococ	$⊢ (K \in OP \land X \underset{˙}{\lor} P \in B) \to oc (K) (oc (K) (X \underset{˙}{\lor} P)) = X \underset{˙}{\lor} P$
49	13 20 48	syl2anc	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (oc (K) (X \underset{˙}{\lor} P)) = X \underset{˙}{\lor} P$
50	31 4 21	opoc0	$⊢ K \in OP \to oc (K) (0. (K)) = \underset{˙}{1}$
51	11 12 50	3syl	$⊢ ((K \in HL \land X \in B \land P \in A) \land (X C \underset{˙}{1} \land \neg P \underset{˙}{\leq} X)) \to oc (K) (0. (K)) = \underset{˙}{1}$
52	47 49 51	3eqtr3d	$⊢ ((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}$

Metamath Proof Explorer

Theorem 1cvrjat

Proof