hlmod1i

Description: A version of the modular law pmod1i that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012)

	Ref	Expression
Hypotheses	hlmod.b	$⊢ B = {Base}_{K}$
	hlmod.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	hlmod.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlmod.m	$⊢ \underset{˙}{\land} = meet (K)$
	hlmod.f	$⊢ F = pmap (K)$
	hlmod.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	hlmod1i	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z = X \underset{˙}{\lor} (Y \underset{˙}{\land} Z))$

Proof

Step	Hyp	Ref	Expression
1		hlmod.b	$⊢ B = {Base}_{K}$
2		hlmod.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		hlmod.j	$⊢ \underset{˙}{\lor} = join (K)$
4		hlmod.m	$⊢ \underset{˙}{\land} = meet (K)$
5		hlmod.f	$⊢ F = pmap (K)$
6		hlmod.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
7		hllat	$⊢ K \in HL \to K \in Lat$
8	7	3ad2ant1	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to K \in Lat$
9		simp21	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to X \in B$
10		simp22	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to Y \in B$
11	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y \in B$
12	8 9 10 11	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to X \underset{˙}{\lor} Y \in B$
13		simp23	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to Z \in B$
14	1 4	latmcl	$⊢ (K \in Lat \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B$
15	8 12 13 14	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B$
16	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land Z \in B) \to Y \underset{˙}{\land} Z \in B$
17	8 10 13 16	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to Y \underset{˙}{\land} Z \in B$
18	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Y \underset{˙}{\land} Z \in B) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} Z) \in B$
19	8 9 17 18	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} Z) \in B$
20		simp1	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to K \in HL$
21		eqid	$⊢ Atoms (K) = Atoms (K)$
22	1 21 5	pmapssat	$⊢ (K \in HL \land X \in B) \to F (X) \subseteq Atoms (K)$
23	20 9 22	syl2anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (X) \subseteq Atoms (K)$
24	1 21 5	pmapssat	$⊢ (K \in HL \land Y \in B) \to F (Y) \subseteq Atoms (K)$
25	20 10 24	syl2anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (Y) \subseteq Atoms (K)$
26		eqid	$⊢ PSubSp (K) = PSubSp (K)$
27	1 26 5	pmapsub	$⊢ (K \in Lat \land Z \in B) \to F (Z) \in PSubSp (K)$
28	8 13 27	syl2anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (Z) \in PSubSp (K)$
29		simp3l	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to X \underset{˙}{\leq} Z$
30	1 2 5	pmaple	$⊢ (K \in HL \land X \in B \land Z \in B) \to (X \underset{˙}{\leq} Z \leftrightarrow F (X) \subseteq F (Z))$
31	20 9 13 30	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to (X \underset{˙}{\leq} Z \leftrightarrow F (X) \subseteq F (Z))$
32	29 31	mpbid	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (X) \subseteq F (Z)$
33	21 26 6	pmod1i	$⊢ (K \in HL \land (F (X) \subseteq Atoms (K) \land F (Y) \subseteq Atoms (K) \land F (Z) \in PSubSp (K))) \to (F (X) \subseteq F (Z) \to (F (X) \underset{˙}{+} F (Y)) \cap F (Z) = F (X) \underset{˙}{+} (F (Y) \cap F (Z)))$
34	33	3impia	$⊢ (K \in HL \land (F (X) \subseteq Atoms (K) \land F (Y) \subseteq Atoms (K) \land F (Z) \in PSubSp (K)) \land F (X) \subseteq F (Z)) \to (F (X) \underset{˙}{+} F (Y)) \cap F (Z) = F (X) \underset{˙}{+} (F (Y) \cap F (Z))$
35	20 23 25 28 32 34	syl131anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to (F (X) \underset{˙}{+} F (Y)) \cap F (Z) = F (X) \underset{˙}{+} (F (Y) \cap F (Z))$
36	1 4 21 5	pmapmeet	$⊢ (K \in HL \land X \underset{˙}{\lor} Y \in B \land Z \in B) \to F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) = F (X \underset{˙}{\lor} Y) \cap F (Z)$
37	20 12 13 36	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) = F (X \underset{˙}{\lor} Y) \cap F (Z)$
38		simp3r	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y)$
39	38	ineq1d	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (X \underset{˙}{\lor} Y) \cap F (Z) = (F (X) \underset{˙}{+} F (Y)) \cap F (Z)$
40	37 39	eqtrd	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) = (F (X) \underset{˙}{+} F (Y)) \cap F (Z)$
41	1 4 21 5	pmapmeet	$⊢ (K \in HL \land Y \in B \land Z \in B) \to F (Y \underset{˙}{\land} Z) = F (Y) \cap F (Z)$
42	20 10 13 41	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (Y \underset{˙}{\land} Z) = F (Y) \cap F (Z)$
43	42	oveq2d	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (X) \underset{˙}{+} F (Y \underset{˙}{\land} Z) = F (X) \underset{˙}{+} (F (Y) \cap F (Z))$
44	35 40 43	3eqtr4d	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) = F (X) \underset{˙}{+} F (Y \underset{˙}{\land} Z)$
45	1 3 5 6	pmapjoin	$⊢ (K \in Lat \land X \in B \land Y \underset{˙}{\land} Z \in B) \to F (X) \underset{˙}{+} F (Y \underset{˙}{\land} Z) \subseteq F (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z))$
46	8 9 17 45	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F (X) \underset{˙}{+} F (Y \underset{˙}{\land} Z) \subseteq F (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z))$
47	44 46	eqsstrd	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \subseteq F (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z))$
48	1 2 5	pmaple	$⊢ (K \in HL \land (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z \in B \land X \underset{˙}{\lor} (Y \underset{˙}{\land} Z) \in B) \to (((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\leq} (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \leftrightarrow F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \subseteq F (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)))$
49	20 15 19 48	syl3anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to (((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\leq} (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \leftrightarrow F ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \subseteq F (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)))$
50	47 49	mpbird	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z) \underset{˙}{\leq} (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z))$
51	1 2 3 4	mod1ile	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\leq} Z \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z))$
52	51	3impia	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B) \land X \underset{˙}{\leq} Z) \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z)$
53	8 9 10 13 29 52	syl131anc	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to (X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)) \underset{˙}{\leq} ((X \underset{˙}{\lor} Y) \underset{˙}{\land} Z)$
54	1 2 8 15 19 50 53	latasymd	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B) \land (X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y))) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z = X \underset{˙}{\lor} (Y \underset{˙}{\land} Z)$
55	54	3expia	$⊢ (K \in HL \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{\leq} Z \land F (X \underset{˙}{\lor} Y) = F (X) \underset{˙}{+} F (Y)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\land} Z = X \underset{˙}{\lor} (Y \underset{˙}{\land} Z))$

Metamath Proof Explorer

Theorem hlmod1i

Proof