pmodlem2

	Ref	Expression
Hypotheses	pmodlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pmodlem.j	$⊢ \underset{˙}{\lor} = join (K)$
	pmodlem.a	$⊢ A = Atoms (K)$
	pmodlem.s	$⊢ S = PSubSp (K)$
	pmodlem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	pmodlem2	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to (X \underset{˙}{+} Y) \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$

Proof

Step	Hyp	Ref	Expression
1		pmodlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		pmodlem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		pmodlem.a	$⊢ A = Atoms (K)$
4		pmodlem.s	$⊢ S = PSubSp (K)$
5		pmodlem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
6		simpr	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to X = \emptyset$
7	6	oveq1d	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to X \underset{˙}{+} Y = \emptyset \underset{˙}{+} Y$
8		simpl1	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to K \in HL$
9		simpl22	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to Y \subseteq A$
10	3 5	padd02	$⊢ (K \in HL \land Y \subseteq A) \to \emptyset \underset{˙}{+} Y = Y$
11	8 9 10	syl2anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to \emptyset \underset{˙}{+} Y = Y$
12	7 11	eqtrd	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to X \underset{˙}{+} Y = Y$
13	12	ineq1d	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to (X \underset{˙}{+} Y) \cap Z = Y \cap Z$
14		ssinss1	$⊢ Y \subseteq A \to Y \cap Z \subseteq A$
15	9 14	syl	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to Y \cap Z \subseteq A$
16		simpl21	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to X \subseteq A$
17	3 5	sspadd2	$⊢ (K \in HL \land Y \cap Z \subseteq A \land X \subseteq A) \to Y \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$
18	8 15 16 17	syl3anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to Y \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$
19	13 18	eqsstrd	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land X = \emptyset) \to (X \underset{˙}{+} Y) \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$
20		oveq2	$⊢ Y = \emptyset \to X \underset{˙}{+} Y = X \underset{˙}{+} \emptyset$
21		simp1	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to K \in HL$
22		simp21	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to X \subseteq A$
23	3 5	padd01	$⊢ (K \in HL \land X \subseteq A) \to X \underset{˙}{+} \emptyset = X$
24	21 22 23	syl2anc	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to X \underset{˙}{+} \emptyset = X$
25	20 24	sylan9eqr	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to X \underset{˙}{+} Y = X$
26	25	ineq1d	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to (X \underset{˙}{+} Y) \cap Z = X \cap Z$
27		inss1	$⊢ X \cap Z \subseteq X$
28		simpl1	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to K \in HL$
29		simpl21	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to X \subseteq A$
30		simpl22	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to Y \subseteq A$
31	30 14	syl	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to Y \cap Z \subseteq A$
32	3 5	sspadd1	$⊢ (K \in HL \land X \subseteq A \land Y \cap Z \subseteq A) \to X \subseteq X \underset{˙}{+} (Y \cap Z)$
33	28 29 31 32	syl3anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to X \subseteq X \underset{˙}{+} (Y \cap Z)$
34	27 33	sstrid	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to X \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$
35	26 34	eqsstrd	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land Y = \emptyset) \to (X \underset{˙}{+} Y) \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$
36		elin	$⊢ p \in ((X \underset{˙}{+} Y) \cap Z) \leftrightarrow (p \in (X \underset{˙}{+} Y) \land p \in Z)$
37		simpl1	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land ((X \neq \emptyset \land Y \neq \emptyset) \land p \in Z)) \to K \in HL$
38	37	hllatd	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land ((X \neq \emptyset \land Y \neq \emptyset) \land p \in Z)) \to K \in Lat$
39		simpl21	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land ((X \neq \emptyset \land Y \neq \emptyset) \land p \in Z)) \to X \subseteq A$
40		simpl22	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land ((X \neq \emptyset \land Y \neq \emptyset) \land p \in Z)) \to Y \subseteq A$
41		simprl	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land ((X \neq \emptyset \land Y \neq \emptyset) \land p \in Z)) \to (X \neq \emptyset \land Y \neq \emptyset)$
42	1 2 3 5	elpaddn0	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (p \in (X \underset{˙}{+} Y) \leftrightarrow (p \in A \land \exists q \in X \exists r \in Y p \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
43	38 39 40 41 42	syl31anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land ((X \neq \emptyset \land Y \neq \emptyset) \land p \in Z)) \to (p \in (X \underset{˙}{+} Y) \leftrightarrow (p \in A \land \exists q \in X \exists r \in Y p \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
44		simpl1	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to K \in HL$
45		simpl21	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to X \subseteq A$
46		simpl22	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to Y \subseteq A$
47		simpl23	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to Z \in S$
48		simpl3	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to X \subseteq Z$
49		simpr1	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to p \in Z$
50		simpr2l	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to q \in X$
51		simpr2r	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to r \in Y$
52		simpr3	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to p \underset{˙}{\leq} (q \underset{˙}{\lor} r)$
53	1 2 3 4 5	pmodlem1	$⊢ ((K \in HL \land X \subseteq A \land Y \subseteq A) \land (Z \in S \land X \subseteq Z \land p \in Z) \land (q \in X \land r \in Y \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to p \in (X \underset{˙}{+} (Y \cap Z))$
54	44 45 46 47 48 49 50 51 52 53	syl333anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (p \in Z \land (q \in X \land r \in Y) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to p \in (X \underset{˙}{+} (Y \cap Z))$
55	54	3exp2	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to (p \in Z \to ((q \in X \land r \in Y) \to (p \underset{˙}{\leq} (q \underset{˙}{\lor} r) \to p \in (X \underset{˙}{+} (Y \cap Z)))))$
56	55	imp	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land p \in Z) \to ((q \in X \land r \in Y) \to (p \underset{˙}{\leq} (q \underset{˙}{\lor} r) \to p \in (X \underset{˙}{+} (Y \cap Z))))$
57	56	rexlimdvv	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land p \in Z) \to (\exists q \in X \exists r \in Y p \underset{˙}{\leq} (q \underset{˙}{\lor} r) \to p \in (X \underset{˙}{+} (Y \cap Z)))$
58	57	adantld	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land p \in Z) \to ((p \in A \land \exists q \in X \exists r \in Y p \underset{˙}{\leq} (q \underset{˙}{\lor} r)) \to p \in (X \underset{˙}{+} (Y \cap Z)))$
59	58	adantrl	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land ((X \neq \emptyset \land Y \neq \emptyset) \land p \in Z)) \to ((p \in A \land \exists q \in X \exists r \in Y p \underset{˙}{\leq} (q \underset{˙}{\lor} r)) \to p \in (X \underset{˙}{+} (Y \cap Z)))$
60	43 59	sylbid	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land ((X \neq \emptyset \land Y \neq \emptyset) \land p \in Z)) \to (p \in (X \underset{˙}{+} Y) \to p \in (X \underset{˙}{+} (Y \cap Z)))$
61	60	exp32	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to ((X \neq \emptyset \land Y \neq \emptyset) \to (p \in Z \to (p \in (X \underset{˙}{+} Y) \to p \in (X \underset{˙}{+} (Y \cap Z)))))$
62	61	com34	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to ((X \neq \emptyset \land Y \neq \emptyset) \to (p \in (X \underset{˙}{+} Y) \to (p \in Z \to p \in (X \underset{˙}{+} (Y \cap Z)))))$
63	62	imp4b	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (X \neq \emptyset \land Y \neq \emptyset)) \to ((p \in (X \underset{˙}{+} Y) \land p \in Z) \to p \in (X \underset{˙}{+} (Y \cap Z)))$
64	36 63	biimtrid	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (p \in ((X \underset{˙}{+} Y) \cap Z) \to p \in (X \underset{˙}{+} (Y \cap Z)))$
65	64	ssrdv	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (X \underset{˙}{+} Y) \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$
66	19 35 65	pm2.61da2ne	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \in S) \land X \subseteq Z) \to (X \underset{˙}{+} Y) \cap Z \subseteq X \underset{˙}{+} (Y \cap Z)$

Metamath Proof Explorer

Theorem pmodlem2

Proof