atmod1i1m

Description: Version of modular law pmod1i that holds in a Hilbert lattice, when an element meets an atom. (Contributed by NM, 2-Sep-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	atmod1i1m	$⊢ ((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = ((X \underset{˙}{\land} P) \underset{˙}{\lor} Y) \underset{˙}{\land} Z$

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		simpl1l	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P \in A) \to K \in HL$
7		simpr	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P \in A) \to X \underset{˙}{\land} P \in A$
8		simpl22	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P \in A) \to Y \in B$
9		simpl23	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P \in A) \to Z \in B$
10		simpl3	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P \in A) \to (X \underset{˙}{\land} P) \underset{˙}{\leq} Z$
11	1 2 3 4 5	atmod1i1	$⊢ (K \in HL \land (X \underset{˙}{\land} P \in A \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = ((X \underset{˙}{\land} P) \underset{˙}{\lor} Y) \underset{˙}{\land} Z$
12	6 7 8 9 10 11	syl131anc	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P \in A) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = ((X \underset{˙}{\land} P) \underset{˙}{\lor} Y) \underset{˙}{\land} Z$
13		simp1l	$⊢ ((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to K \in HL$
14		hlol	$⊢ K \in HL \to K \in OL$
15	13 14	syl	$⊢ ((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to K \in OL$
16	15	adantr	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to K \in OL$
17	13	hllatd	$⊢ ((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to K \in Lat$
18	17	adantr	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to K \in Lat$
19		simpl22	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to Y \in B$
20		simpl23	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to Z \in B$
21	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\land} Z \in B$
22	18 19 20 21	syl3anc	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to Y \underset{˙}{\land} Z \in B$
23		eqid	$⊢ 0. (K) = 0. (K)$
24	1 3 23	olj02	$⊢ (K \in OL \land Y \underset{˙}{\land} Z \in B) \to 0. (K) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = Y \underset{˙}{\land} Z$
25	16 22 24	syl2anc	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to 0. (K) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = Y \underset{˙}{\land} Z$
26		oveq1	$⊢ X \underset{˙}{\land} P = 0. (K) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = 0. (K) \underset{˙}{\lor} (Y \underset{˙}{\land} Z)$
27	26	adantl	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = 0. (K) \underset{˙}{\lor} (Y \underset{˙}{\land} Z)$
28		oveq1	$⊢ X \underset{˙}{\land} P = 0. (K) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} Y = 0. (K) \underset{˙}{\lor} Y$
29	28	adantl	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} Y = 0. (K) \underset{˙}{\lor} Y$
30	1 3 23	olj02	$⊢ (K \in OL \land Y \in B) \to 0. (K) \underset{˙}{\lor} Y = Y$
31	16 19 30	syl2anc	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to 0. (K) \underset{˙}{\lor} Y = Y$
32	29 31	eqtrd	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} Y = Y$
33	32	oveq1d	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to ((X \underset{˙}{\land} P) \underset{˙}{\lor} Y) \underset{˙}{\land} Z = Y \underset{˙}{\land} Z$
34	25 27 33	3eqtr4d	$⊢ (((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \land X \underset{˙}{\land} P = 0. (K)) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = ((X \underset{˙}{\land} P) \underset{˙}{\lor} Y) \underset{˙}{\land} Z$
35		simp21	$⊢ ((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to X \in B$
36		simp1r	$⊢ ((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to P \in A$
37	1 4 23 5	meetat2	$⊢ (K \in OL \land X \in B \land P \in A) \to (X \underset{˙}{\land} P \in A \lor X \underset{˙}{\land} P = 0. (K))$
38	15 35 36 37	syl3anc	$⊢ ((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to (X \underset{˙}{\land} P \in A \lor X \underset{˙}{\land} P = 0. (K))$
39	12 34 38	mpjaodan	$⊢ ((K \in HL \land P \in A) \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\land} P) \underset{˙}{\leq} Z) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = ((X \underset{˙}{\land} P) \underset{˙}{\lor} Y) \underset{˙}{\land} Z$

Metamath Proof Explorer

Theorem atmod1i1m

Proof