lhpmod2i2

Description: Modular law for hyperplanes analogous to atmod2i2 for atoms. (Contributed by NM, 9-Feb-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	lhpmod2i2	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to (X \underset{˙}{\land} W) \underset{˙}{\lor} Y = X \underset{˙}{\land} (W \underset{˙}{\lor} Y)$

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 Y \underset{˙}{\leq} X) \to K \in HL$
7		simp1r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \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 Y \underset{˙}{\leq} X) \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 Y \underset{˙}{\leq} X) \to K \in OP$
14		simp2l	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \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 Y \underset{˙}{\leq} X) \to oc (K) (X) \in B$
17		simp2r	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \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 Y \underset{˙}{\leq} X) \to oc (K) (Y) \in B$
20		simp3	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to Y \underset{˙}{\leq} X$
21	1 2 8	oplecon3b	$⊢ (K \in OP \land Y \in B \land X \in B) \to (Y \underset{˙}{\leq} X \leftrightarrow oc (K) (X) \underset{˙}{\leq} oc (K) (Y))$
22	13 17 14 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to (Y \underset{˙}{\leq} X \leftrightarrow oc (K) (X) \underset{˙}{\leq} oc (K) (Y))$
23	20 22	mpbid	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) (X) \underset{˙}{\leq} oc (K) (Y)$
24	1 2 3 4 9	atmod1i2	$⊢ (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) (X) \underset{˙}{\leq} oc (K) (Y)) \to oc (K) (X) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\land} oc (K) (Y)) = (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\land} oc (K) (Y)$
25	6 11 16 19 23 24	syl131anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) (X) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\land} oc (K) (Y)) = (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\land} oc (K) (Y)$
26	6	hllatd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to K \in Lat$
27	1 5	lhpbase	$⊢ W \in H \to W \in B$
28	7 27	syl	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to W \in B$
29	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
30	26 14 28 29	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to X \underset{˙}{\land} W \in B$
31	1 3	latjcl	$⊢ (K \in Lat \land X \underset{˙}{\land} W \in B \land Y \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\lor} Y \in B$
32	26 30 17 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to (X \underset{˙}{\land} W) \underset{˙}{\lor} Y \in B$
33	1 3	latjcl	$⊢ (K \in Lat \land W \in B \land Y \in B) \to W \underset{˙}{\lor} Y \in B$
34	26 28 17 33	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to W \underset{˙}{\lor} Y \in B$
35	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \underset{˙}{\lor} Y \in B) \to X \underset{˙}{\land} (W \underset{˙}{\lor} Y) \in B$
36	26 14 34 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to X \underset{˙}{\land} (W \underset{˙}{\lor} Y) \in B$
37	1 8	opcon3b	$⊢ (K \in OP \land (X \underset{˙}{\land} W) \underset{˙}{\lor} Y \in B \land X \underset{˙}{\land} (W \underset{˙}{\lor} Y) \in B) \to ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y = X \underset{˙}{\land} (W \underset{˙}{\lor} Y) \leftrightarrow oc (K) (X \underset{˙}{\land} (W \underset{˙}{\lor} Y)) = oc (K) ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y))$
38	13 32 36 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y = X \underset{˙}{\land} (W \underset{˙}{\lor} Y) \leftrightarrow oc (K) (X \underset{˙}{\land} (W \underset{˙}{\lor} Y)) = oc (K) ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y))$
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 Y \underset{˙}{\leq} X) \to K \in OL$
41	1 3 4 8	oldmm1	$⊢ (K \in OL \land X \in B \land W \underset{˙}{\lor} Y \in B) \to oc (K) (X \underset{˙}{\land} (W \underset{˙}{\lor} Y)) = oc (K) (X) \underset{˙}{\lor} oc (K) (W \underset{˙}{\lor} Y)$
42	40 14 34 41	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) (X \underset{˙}{\land} (W \underset{˙}{\lor} Y)) = oc (K) (X) \underset{˙}{\lor} oc (K) (W \underset{˙}{\lor} Y)$
43	1 3 4 8	oldmj1	$⊢ (K \in OL \land W \in B \land Y \in B) \to oc (K) (W \underset{˙}{\lor} Y) = oc (K) (W) \underset{˙}{\land} oc (K) (Y)$
44	40 28 17 43	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) (W \underset{˙}{\lor} Y) = oc (K) (W) \underset{˙}{\land} oc (K) (Y)$
45	44	oveq2d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) (X) \underset{˙}{\lor} oc (K) (W \underset{˙}{\lor} Y) = oc (K) (X) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\land} oc (K) (Y))$
46	42 45	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) (X \underset{˙}{\land} (W \underset{˙}{\lor} Y)) = oc (K) (X) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\land} oc (K) (Y))$
47	1 3 4 8	oldmj1	$⊢ (K \in OL \land X \underset{˙}{\land} W \in B \land Y \in B) \to oc (K) ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y) = oc (K) (X \underset{˙}{\land} W) \underset{˙}{\land} oc (K) (Y)$
48	40 30 17 47	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y) = oc (K) (X \underset{˙}{\land} W) \underset{˙}{\land} oc (K) (Y)$
49	1 3 4 8	oldmm1	$⊢ (K \in OL \land X \in B \land W \in B) \to oc (K) (X \underset{˙}{\land} W) = oc (K) (X) \underset{˙}{\lor} oc (K) (W)$
50	40 14 28 49	syl3anc	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) (X \underset{˙}{\land} W) = oc (K) (X) \underset{˙}{\lor} oc (K) (W)$
51	50	oveq1d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) (X \underset{˙}{\land} W) \underset{˙}{\land} oc (K) (Y) = (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\land} oc (K) (Y)$
52	48 51	eqtrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to oc (K) ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y) = (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\land} oc (K) (Y)$
53	46 52	eqeq12d	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to (oc (K) (X \underset{˙}{\land} (W \underset{˙}{\lor} Y)) = oc (K) ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y) \leftrightarrow oc (K) (X) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\land} oc (K) (Y)) = (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\land} oc (K) (Y))$
54	38 53	bitrd	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to ((X \underset{˙}{\land} W) \underset{˙}{\lor} Y = X \underset{˙}{\land} (W \underset{˙}{\lor} Y) \leftrightarrow oc (K) (X) \underset{˙}{\lor} (oc (K) (W) \underset{˙}{\land} oc (K) (Y)) = (oc (K) (X) \underset{˙}{\lor} oc (K) (W)) \underset{˙}{\land} oc (K) (Y))$
55	25 54	mpbird	$⊢ ((K \in HL \land W \in H) \land (X \in B \land Y \in B) \land Y \underset{˙}{\leq} X) \to (X \underset{˙}{\land} W) \underset{˙}{\lor} Y = X \underset{˙}{\land} (W \underset{˙}{\lor} Y)$

Metamath Proof Explorer

Theorem lhpmod2i2

Proof