lhpmod6i1

Description: Modular law for hyperplanes analogous to complement of atmod2i1 for atoms. (Contributed by NM, 1-Jun-2013)

	Ref	Expression
Hypotheses	lhpmod.b	$⊢ B = {Base}_{K}$
	lhpmod.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lhpmod.j	$⊢ \underset{˙}{\lor} = join (K)$
	lhpmod.m	$⊢ \underset{˙}{\land} = meet (K)$
	lhpmod.h	$⊢ H = LHyp (K)$
Assertion	lhpmod6i1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} W) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} W$

Proof

Step	Hyp	Ref	Expression
1		lhpmod.b	$⊢ B = {Base}_{K}$
2		lhpmod.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lhpmod.j	$⊢ \underset{˙}{\lor} = join (K)$
4		lhpmod.m	$⊢ \underset{˙}{\land} = meet (K)$
5		lhpmod.h	$⊢ H = LHyp (K)$
6		simp1l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to K \in HL$
7		simp1r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to W \in H$
8		eqid	$⊢ oc (K) = oc (K)$
9		eqid	$⊢ Atoms (K) = Atoms (K)$
10	8 9 5	lhpocat	$⊢ (K \in HL \land W \in H) \to oc (K) (W) \in Atoms (K)$
11	6 7 10	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (W) \in Atoms (K)$
12		hlop	$⊢ K \in HL \to K \in OP$
13	6 12	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to K \in OP$
14		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to X \in B$
15	1 8	opoccl	$⊢ (K \in OP \land X \in B) \to oc (K) (X) \in B$
16	13 14 15	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (X) \in B$
17		simp2r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to Y \in B$
18	1 8	opoccl	$⊢ (K \in OP \land Y \in B) \to oc (K) (Y) \in B$
19	13 17 18	syl2anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (Y) \in B$
20		simp3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to X \underset{˙}{\leq} W$
21	1 5	lhpbase	$⊢ W \in H \to W \in B$
22	7 21	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to W \in B$
23	1 2 8	oplecon3b	$⊢ (K \in OP \land X \in B \land W \in B) \to (X \underset{˙}{\leq} W \leftrightarrow oc (K) (W) \underset{˙}{\leq} oc (K) (X))$
24	13 14 22 23	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to (X \underset{˙}{\leq} W \leftrightarrow oc (K) (W) \underset{˙}{\leq} oc (K) (X))$
25	20 24	mpbid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (W) \underset{˙}{\leq} oc (K) (X)$
26	1 2 3 4 9	atmod2i1	$⊢ (K \in HL \land (oc (K) (W) \in Atoms (K) \land oc (K) (X) \in B \land oc (K) (Y) \in B) \land oc (K) (W) \underset{˙}{\leq} oc (K) (X)) \to (oc (K) (X) \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\lor} oc (K) (W) = oc (K) (X) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))$
27	6 11 16 19 25 26	syl131anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to (oc (K) (X) \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\lor} oc (K) (W) = oc (K) (X) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))$
28	6	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to K \in Lat$
29	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
30	28 17 22 29	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to Y \underset{˙}{\land} W \in B$
31	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \underset{˙}{\land} W \in B) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} W) \in B$
32	28 14 30 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} W) \in B$
33	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
34	28 14 17 33	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to X \underset{˙}{\lor} Y \in B$
35	1 4	latmcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land W \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} W \in B$
36	28 34 22 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} W \in B$
37	1 8	opcon3b	$⊢ (K \in OP \land X \underset{˙}{\lor} (Y \underset{˙}{\land} W) \in B \land (X \underset{˙}{\lor} Y) \underset{˙}{\land} W \in B) \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} W) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} W \leftrightarrow oc (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\land} W) = oc (K) (X \underset{˙}{\lor} (Y \underset{˙}{\land} W)))$
38	13 32 36 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} W) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} W \leftrightarrow oc (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\land} W) = oc (K) (X \underset{˙}{\lor} (Y \underset{˙}{\land} W)))$
39		hlol	$⊢ K \in HL \to K \in OL$
40	6 39	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to K \in OL$
41	1 3 4 8	oldmm1	$⊢ (K \in OL \land X \underset{˙}{\lor} Y \in B \land W \in B) \to oc (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\land} W) = oc (K) (X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)$
42	40 34 22 41	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\land} W) = oc (K) (X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W)$
43	1 3 4 8	oldmj1	$⊢ (K \in OL \land X \in B \land Y \in B) \to oc (K) (X \underset{˙}{\lor} Y) = oc (K) (X) \underset{˙}{\land} oc (K) (Y)$
44	40 14 17 43	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (X \underset{˙}{\lor} Y) = oc (K) (X) \underset{˙}{\land} oc (K) (Y)$
45	44	oveq1d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (X \underset{˙}{\lor} Y) \underset{˙}{\lor} oc (K) (W) = (oc (K) (X) \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\lor} oc (K) (W)$
46	42 45	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\land} W) = (oc (K) (X) \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\lor} oc (K) (W)$
47	1 3 4 8	oldmj1	$⊢ (K \in OL \land X \in B \land Y \underset{˙}{\land} W \in B) \to oc (K) (X \underset{˙}{\lor} (Y \underset{˙}{\land} W)) = oc (K) (X) \underset{˙}{\land} oc (K) (Y \underset{˙}{\land} W)$
48	40 14 30 47	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (X \underset{˙}{\lor} (Y \underset{˙}{\land} W)) = oc (K) (X) \underset{˙}{\land} oc (K) (Y \underset{˙}{\land} W)$
49	1 3 4 8	oldmm1	$⊢ (K \in OL \land Y \in B \land W \in B) \to oc (K) (Y \underset{˙}{\land} W) = oc (K) (Y) \underset{˙}{\lor} oc (K) (W)$
50	40 17 22 49	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (Y \underset{˙}{\land} W) = oc (K) (Y) \underset{˙}{\lor} oc (K) (W)$
51	50	oveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (X) \underset{˙}{\land} oc (K) (Y \underset{˙}{\land} W) = oc (K) (X) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))$
52	48 51	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to oc (K) (X \underset{˙}{\lor} (Y \underset{˙}{\land} W)) = oc (K) (X) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\lor} oc (K) (W))$
53	46 52	eqeq12d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to (oc (K) ((X \underset{˙}{\lor} Y) \underset{˙}{\land} W) = oc (K) (X \underset{˙}{\lor} (Y \underset{˙}{\land} W)) \leftrightarrow (oc (K) (X) \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\lor} oc (K) (W) = oc (K) (X) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\lor} oc (K) (W)))$
54	38 53	bitrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} W) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} W \leftrightarrow (oc (K) (X) \underset{˙}{\land} oc (K) (Y)) \underset{˙}{\lor} oc (K) (W) = oc (K) (X) \underset{˙}{\land} (oc (K) (Y) \underset{˙}{\lor} oc (K) (W)))$
55	27 54	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land X \underset{˙}{\leq} W) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} W) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem lhpmod6i1

Proof