atmod1i2

Description: Version of modular law pmod1i 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	atmod1i2	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\lor} (P \underset{˙}{\land} Y) = (X \underset{˙}{\lor} P) \underset{˙}{\land} Y$

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		simpl	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B)) \to K \in HL$
7		simpr2	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B)) \to X \in B$
8		simpr1	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B)) \to P \in A$
9		eqid	$⊢ pmap (K) = pmap (K)$
10		eqid	$⊢ +_{𝑃} (K) = +_{𝑃} (K)$
11	1 3 5 9 10	pmapjat1	$⊢ (K \in HL \land X \in B \land P \in A) \to pmap (K) (X \underset{˙}{\lor} P) = pmap (K) (X) +_{𝑃} (K) pmap (K) (P)$
12	6 7 8 11	syl3anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B)) \to pmap (K) (X \underset{˙}{\lor} P) = pmap (K) (X) +_{𝑃} (K) pmap (K) (P)$
13	1 5	atbase	$⊢ P \in A \to P \in B$
14	8 13	syl	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B)) \to P \in B$
15		simpr3	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B)) \to Y \in B$
16	1 2 3 4 9 10	hlmod1i	$⊢ (K \in HL \land (X \in B \land P \in B \land Y \in B)) \to ((X \underset{˙}{\leq} Y \land pmap (K) (X \underset{˙}{\lor} P) = pmap (K) (X) +_{𝑃} (K) pmap (K) (P)) \to (X \underset{˙}{\lor} P) \underset{˙}{\land} Y = X \underset{˙}{\lor} (P \underset{˙}{\land} Y))$
17	6 7 14 15 16	syl13anc	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B)) \to ((X \underset{˙}{\leq} Y \land pmap (K) (X \underset{˙}{\lor} P) = pmap (K) (X) +_{𝑃} (K) pmap (K) (P)) \to (X \underset{˙}{\lor} P) \underset{˙}{\land} Y = X \underset{˙}{\lor} (P \underset{˙}{\land} Y))$
18	12 17	mpan2d	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\lor} P) \underset{˙}{\land} Y = X \underset{˙}{\lor} (P \underset{˙}{\land} Y))$
19	18	3impia	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (X \underset{˙}{\lor} P) \underset{˙}{\land} Y = X \underset{˙}{\lor} (P \underset{˙}{\land} Y)$
20	19	eqcomd	$⊢ (K \in HL \land (P \in A \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\lor} (P \underset{˙}{\land} Y) = (X \underset{˙}{\lor} P) \underset{˙}{\land} Y$

Metamath Proof Explorer

Theorem atmod1i2

Proof