pmodlem1

	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	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))$

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		simpl11	$⊢ (((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))) \land p = q) \to K \in HL$
7		simpl12	$⊢ (((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))) \land p = q) \to X \subseteq A$
8		simpl13	$⊢ (((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))) \land p = q) \to Y \subseteq A$
9		ssinss1	$⊢ Y \subseteq A \to Y \cap Z \subseteq A$
10	8 9	syl	$⊢ (((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))) \land p = q) \to Y \cap Z \subseteq A$
11	3 5	sspadd1	$⊢ (K \in HL \land X \subseteq A \land Y \cap Z \subseteq A) \to X \subseteq X \underset{˙}{+} (Y \cap Z)$
12	6 7 10 11	syl3anc	$⊢ (((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))) \land p = q) \to X \subseteq X \underset{˙}{+} (Y \cap Z)$
13		simpr	$⊢ (((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))) \land p = q) \to p = q$
14		simpl31	$⊢ (((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))) \land p = q) \to q \in X$
15	13 14	eqeltrd	$⊢ (((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))) \land p = q) \to p \in X$
16	12 15	sseldd	$⊢ (((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))) \land p = q) \to p \in (X \underset{˙}{+} (Y \cap Z))$
17		simpl11	$⊢ (((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))) \land p \neq q) \to K \in HL$
18	17	hllatd	$⊢ (((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))) \land p \neq q) \to K \in Lat$
19		simpl12	$⊢ (((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))) \land p \neq q) \to X \subseteq A$
20		simpl13	$⊢ (((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))) \land p \neq q) \to Y \subseteq A$
21	20 9	syl	$⊢ (((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))) \land p \neq q) \to Y \cap Z \subseteq A$
22		simpl31	$⊢ (((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))) \land p \neq q) \to q \in X$
23		simpl32	$⊢ (((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))) \land p \neq q) \to r \in Y$
24		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))) \land p \neq q) \to Z \in S$
25		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))) \land p \neq q) \to X \subseteq Z$
26		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))) \land p \neq q) \to p \in Z$
27	3 4	psubssat	$⊢ (K \in HL \land Z \in S) \to Z \subseteq A$
28	17 24 27	syl2anc	$⊢ (((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))) \land p \neq q) \to Z \subseteq A$
29	28 26	sseldd	$⊢ (((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))) \land p \neq q) \to p \in A$
30	20 23	sseldd	$⊢ (((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))) \land p \neq q) \to r \in A$
31	19 22	sseldd	$⊢ (((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))) \land p \neq q) \to q \in A$
32	29 30 31	3jca	$⊢ (((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))) \land p \neq q) \to (p \in A \land r \in A \land q \in A)$
33		simpr	$⊢ (((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))) \land p \neq q) \to p \neq q$
34		simpl33	$⊢ (((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))) \land p \neq q) \to p \underset{˙}{\leq} (q \underset{˙}{\lor} r)$
35	1 2 3	hlatexch1	$⊢ (K \in HL \land (p \in A \land r \in A \land q \in A) \land p \neq q) \to (p \underset{˙}{\leq} (q \underset{˙}{\lor} r) \to r \underset{˙}{\leq} (q \underset{˙}{\lor} p))$
36	35	imp	$⊢ ((K \in HL \land (p \in A \land r \in A \land q \in A) \land p \neq q) \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r)) \to r \underset{˙}{\leq} (q \underset{˙}{\lor} p)$
37	17 32 33 34 36	syl31anc	$⊢ (((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))) \land p \neq q) \to r \underset{˙}{\leq} (q \underset{˙}{\lor} p)$
38		simp31	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to q \in X$
39	38	snssd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to \{q\} \subseteq X$
40		simp22	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to X \subseteq Z$
41	39 40	sstrd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to \{q\} \subseteq Z$
42		simp23	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to p \in Z$
43	42	snssd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to \{p\} \subseteq Z$
44		simp11	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to K \in HL$
45		simp12	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to X \subseteq A$
46	45 38	sseldd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to q \in A$
47	46	snssd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to \{q\} \subseteq A$
48		simp21	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to Z \in S$
49	44 48 27	syl2anc	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to Z \subseteq A$
50	49 42	sseldd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to p \in A$
51	50	snssd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to \{p\} \subseteq A$
52	3 4 5	paddss	$⊢ (K \in HL \land (\{q\} \subseteq A \land \{p\} \subseteq A \land Z \in S)) \to ((\{q\} \subseteq Z \land \{p\} \subseteq Z) \leftrightarrow \{q\} \underset{˙}{+} \{p\} \subseteq Z)$
53	44 47 51 48 52	syl13anc	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to ((\{q\} \subseteq Z \land \{p\} \subseteq Z) \leftrightarrow \{q\} \underset{˙}{+} \{p\} \subseteq Z)$
54	41 43 53	mpbi2and	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to \{q\} \underset{˙}{+} \{p\} \subseteq Z$
55		simp33	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to r \underset{˙}{\leq} (q \underset{˙}{\lor} p)$
56	44	hllatd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to K \in Lat$
57		simp13	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to Y \subseteq A$
58		simp32	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to r \in Y$
59	57 58	sseldd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to r \in A$
60	1 2 3 5	elpadd2at2	$⊢ (K \in Lat \land (q \in A \land p \in A \land r \in A)) \to (r \in (\{q\} \underset{˙}{+} \{p\}) \leftrightarrow r \underset{˙}{\leq} (q \underset{˙}{\lor} p))$
61	56 46 50 59 60	syl13anc	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to (r \in (\{q\} \underset{˙}{+} \{p\}) \leftrightarrow r \underset{˙}{\leq} (q \underset{˙}{\lor} p))$
62	55 61	mpbird	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to r \in (\{q\} \underset{˙}{+} \{p\})$
63	54 62	sseldd	$⊢ ((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 r \underset{˙}{\leq} (q \underset{˙}{\lor} p))) \to r \in Z$
64	17 19 20 24 25 26 22 23 37 63	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))) \land p \neq q) \to r \in Z$
65	23 64	elind	$⊢ (((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))) \land p \neq q) \to r \in (Y \cap Z)$
66	1 2 3 5	elpaddri	$⊢ ((K \in Lat \land X \subseteq A \land Y \cap Z \subseteq A) \land (q \in X \land r \in (Y \cap Z)) \land (p \in A \land p \underset{˙}{\leq} (q \underset{˙}{\lor} r))) \to p \in (X \underset{˙}{+} (Y \cap Z))$
67	18 19 21 22 65 29 34 66	syl322anc	$⊢ (((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))) \land p \neq q) \to p \in (X \underset{˙}{+} (Y \cap Z))$
68	16 67	pm2.61dane	$⊢ ((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))$

Metamath Proof Explorer

Theorem pmodlem1

Proof