llnmod1i2

Description: Version of modular law pmod1i that holds in a Hilbert lattice, when one element is a lattice line (expressed as the join P .\/ Q ). (Contributed by NM, 16-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	llnmod1i2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} Y) = (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) \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		simpl1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to K \in HL$
7		simpl2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to X \in B$
8		simprl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to P \in A$
9		simprr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to Q \in A$
10		eqid	$⊢ pmap (K) = pmap (K)$
11		eqid	$⊢ +_{𝑃} (K) = +_{𝑃} (K)$
12	1 3 5 10 11	pmapjlln1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to pmap (K) (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) = pmap (K) (X) +_{𝑃} (K) pmap (K) (P \underset{˙}{\lor} Q)$
13	6 7 8 9 12	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to pmap (K) (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) = pmap (K) (X) +_{𝑃} (K) pmap (K) (P \underset{˙}{\lor} Q)$
14	6	hllatd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to K \in Lat$
15	1 5	atbase	$⊢ P \in A \to P \in B$
16	8 15	syl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to P \in B$
17	1 5	atbase	$⊢ Q \in A \to Q \in B$
18	9 17	syl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to Q \in B$
19	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q \in B$
20	14 16 18 19	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to P \underset{˙}{\lor} Q \in B$
21		simpl3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to Y \in B$
22	1 2 3 4 10 11	hlmod1i	$⊢ (K \in HL \land (X \in B \land P \underset{˙}{\lor} Q \in B \land Y \in B)) \to ((X \underset{˙}{\leq} Y \land pmap (K) (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) = pmap (K) (X) +_{𝑃} (K) pmap (K) (P \underset{˙}{\lor} Q)) \to (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) \underset{˙}{\land} Y = X \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} Y))$
23	6 7 20 21 22	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to ((X \underset{˙}{\leq} Y \land pmap (K) (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) = pmap (K) (X) +_{𝑃} (K) pmap (K) (P \underset{˙}{\lor} Q)) \to (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) \underset{˙}{\land} Y = X \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} Y))$
24	13 23	mpan2d	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) \underset{˙}{\land} Y = X \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} Y))$
25	24	3impia	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A) \land X \underset{˙}{\leq} Y) \to (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) \underset{˙}{\land} Y = X \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} Y)$
26	25	eqcomd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (P \in A \land Q \in A) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} Y) = (X \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) \underset{˙}{\land} Y$

Metamath Proof Explorer

Theorem llnmod1i2

Proof