atmod2i1

Description: Version of modular law pmod2iN that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012) (Revised by Mario Carneiro, 10-May-2013)

	Ref	Expression
Hypotheses	atmod.b	$⊢ B = {Base}_{K}$
	atmod.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atmod.j	$⊢ \underset{˙}{\lor} = join (K)$
	atmod.m	$⊢ \underset{˙}{\land} = meet (K)$
	atmod.a	$⊢ A = Atoms (K)$
Assertion	atmod2i1	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} P = X \underset{˙}{\land} (Y \underset{˙}{\lor} P)$

Proof

Step	Hyp	Ref	Expression
1		atmod.b	$⊢ B = {Base}_{K}$
2		atmod.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atmod.j	$⊢ \underset{˙}{\lor} = join (K)$
4		atmod.m	$⊢ \underset{˙}{\land} = meet (K)$
5		atmod.a	$⊢ A = Atoms (K)$
6		hllat	$⊢ K \in HL \to K \in Lat$
7	6	3ad2ant1	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to K \in Lat$
8		simp22	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to X \in B$
9		simp23	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to Y \in B$
10	1 4	latmcom	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
11	7 8 9 10	syl3anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to X \underset{˙}{\land} Y = Y \underset{˙}{\land} X$
12	11	oveq2d	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} (X \underset{˙}{\land} Y) = P \underset{˙}{\lor} (Y \underset{˙}{\land} X)$
13		simp21	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to P \in A$
14	1 5	atbase	$⊢ P \in A \to P \in B$
15	13 14	syl	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to P \in B$
16	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
17	7 8 9 16	syl3anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to X \underset{˙}{\land} Y \in B$
18	1 3	latjcom	$⊢ (K \in Lat \land P \in B \land X \underset{˙}{\land} Y \in B) \to P \underset{˙}{\lor} (X \underset{˙}{\land} Y) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} P$
19	7 15 17 18	syl3anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} (X \underset{˙}{\land} Y) = (X \underset{˙}{\land} Y) \underset{˙}{\lor} P$
20	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land Y \in B) \to P \underset{˙}{\lor} Y \in B$
21	7 15 9 20	syl3anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} Y \in B$
22	1 4	latmcom	$⊢ (K \in Lat \land P \underset{˙}{\lor} Y \in B \land X \in B) \to (P \underset{˙}{\lor} Y) \underset{˙}{\land} X = X \underset{˙}{\land} (P \underset{˙}{\lor} Y)$
23	7 21 8 22	syl3anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to (P \underset{˙}{\lor} Y) \underset{˙}{\land} X = X \underset{˙}{\land} (P \underset{˙}{\lor} Y)$
24		simp1	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to K \in HL$
25		simp3	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\leq} X$
26	1 2 3 4 5	atmod1i1	$⊢ (K \in HL \land (P \in A \land Y \in B \land X \in B) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} (Y \underset{˙}{\land} X) = (P \underset{˙}{\lor} Y) \underset{˙}{\land} X$
27	24 13 9 8 25 26	syl131anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} (Y \underset{˙}{\land} X) = (P \underset{˙}{\lor} Y) \underset{˙}{\land} X$
28	1 3	latjcom	$⊢ (K \in Lat \land Y \in B \land P \in B) \to Y \underset{˙}{\lor} P = P \underset{˙}{\lor} Y$
29	7 9 15 28	syl3anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to Y \underset{˙}{\lor} P = P \underset{˙}{\lor} Y$
30	29	oveq2d	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to X \underset{˙}{\land} (Y \underset{˙}{\lor} P) = X \underset{˙}{\land} (P \underset{˙}{\lor} Y)$
31	23 27 30	3eqtr4d	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\lor} (Y \underset{˙}{\land} X) = X \underset{˙}{\land} (Y \underset{˙}{\lor} P)$
32	12 19 31	3eqtr3d	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land P \underset{˙}{\leq} X) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} P = X \underset{˙}{\land} (Y \underset{˙}{\lor} P)$

Metamath Proof Explorer

Theorem atmod2i1

Proof