osumcllem11N

Description: Lemma for osumclN . (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	osumcl.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	osumcl.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	osumcl.c	$⊢ C = PSubCl (K)$
Assertion	osumcllem11N	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to X \underset{˙}{+} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$

Proof

Step	Hyp	Ref	Expression
1		osumcl.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
2		osumcl.o	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3		osumcl.c	$⊢ C = PSubCl (K)$
4		nonconne	$⊢ \neg (X = X \land X \neq X)$
5		simpl1	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to K \in HL$
6		simpl2	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to X \in C$
7		eqid	$⊢ Atoms (K) = Atoms (K)$
8	7 3	psubclssatN	$⊢ (K \in HL \land X \in C) \to X \subseteq Atoms (K)$
9	5 6 8	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to X \subseteq Atoms (K)$
10		simpl3	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to Y \in C$
11	7 3	psubclssatN	$⊢ (K \in HL \land Y \in C) \to Y \subseteq Atoms (K)$
12	5 10 11	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to Y \subseteq Atoms (K)$
13	7 1	paddssat	$⊢ (K \in HL \land X \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \to X \underset{˙}{+} Y \subseteq Atoms (K)$
14	5 9 12 13	syl3anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to X \underset{˙}{+} Y \subseteq Atoms (K)$
15	7 2	2polssN	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq Atoms (K)) \to X \underset{˙}{+} Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
16	5 14 15	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to X \underset{˙}{+} Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
17		df-pss	$⊢ X \underset{˙}{+} Y \subset \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \leftrightarrow (X \underset{˙}{+} Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \land X \underset{˙}{+} Y \neq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)))$
18		pssnel	$⊢ X \underset{˙}{+} Y \subset \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \to \exists p (p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \land \neg p \in (X \underset{˙}{+} Y))$
19	17 18	sylbir	$⊢ (X \underset{˙}{+} Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \land X \underset{˙}{+} Y \neq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \to \exists p (p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \land \neg p \in (X \underset{˙}{+} Y))$
20		df-rex	$⊢ \exists p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \neg p \in (X \underset{˙}{+} Y) \leftrightarrow \exists p (p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \land \neg p \in (X \underset{˙}{+} Y))$
21	19 20	sylibr	$⊢ (X \underset{˙}{+} Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \land X \underset{˙}{+} Y \neq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \to \exists p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \neg p \in (X \underset{˙}{+} Y)$
22		eqid	$⊢ \leq_{K} = \leq_{K}$
23		eqid	$⊢ join (K) = join (K)$
24		eqid	$⊢ X \underset{˙}{+} \{p\} = X \underset{˙}{+} \{p\}$
25		eqid	$⊢ \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
26	22 23 7 1 2 3 24 25	osumcllem9N	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to X \underset{˙}{+} \{p\} = X$
27		simp11	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to K \in HL$
28		simp12	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to X \in C$
29	27 28 8	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to X \subseteq Atoms (K)$
30		simp13	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to Y \in C$
31	27 30 11	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to Y \subseteq Atoms (K)$
32	14	3adantr3	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)))) \to X \underset{˙}{+} Y \subseteq Atoms (K)$
33	32	3adant3	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to X \underset{˙}{+} Y \subseteq Atoms (K)$
34	7 2	polssatN	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq Atoms (K)) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq Atoms (K)$
35	27 33 34	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq Atoms (K)$
36	7 2	polssatN	$⊢ (K \in HL \land \underset{˙}{⊥} (X \underset{˙}{+} Y) \subseteq Atoms (K)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \subseteq Atoms (K)$
37	27 35 36	syl2anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \subseteq Atoms (K)$
38		simp23	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$
39	37 38	sseldd	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to p \in Atoms (K)$
40		simp3	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to \neg p \in (X \underset{˙}{+} Y)$
41	22 23 7 1 2 3 24 25	osumcllem10N	$⊢ ((K \in HL \land X \subseteq Atoms (K) \land Y \subseteq Atoms (K)) \land p \in Atoms (K) \land \neg p \in (X \underset{˙}{+} Y)) \to X \underset{˙}{+} \{p\} \neq X$
42	27 29 31 39 40 41	syl311anc	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to X \underset{˙}{+} \{p\} \neq X$
43	26 42	pm2.21ddne	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \land \neg p \in (X \underset{˙}{+} Y)) \to (X = X \land X \neq X)$
44	43	3exp	$⊢ (K \in HL \land X \in C \land Y \in C) \to ((X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset \land p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \to (\neg p \in (X \underset{˙}{+} Y) \to (X = X \land X \neq X)))$
45	44	3expd	$⊢ (K \in HL \land X \in C \land Y \in C) \to (X \subseteq \underset{˙}{⊥} (Y) \to (X \neq \emptyset \to (p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \to (\neg p \in (X \underset{˙}{+} Y) \to (X = X \land X \neq X)))))$
46	45	imp32	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to (p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \to (\neg p \in (X \underset{˙}{+} Y) \to (X = X \land X \neq X)))$
47	46	rexlimdv	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to (\exists p \in \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \neg p \in (X \underset{˙}{+} Y) \to (X = X \land X \neq X))$
48	21 47	syl5	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to ((X \underset{˙}{+} Y \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \land X \underset{˙}{+} Y \neq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))) \to (X = X \land X \neq X))$
49	16 48	mpand	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to (X \underset{˙}{+} Y \neq \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)) \to (X = X \land X \neq X))$
50	49	necon1bd	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to (\neg (X = X \land X \neq X) \to X \underset{˙}{+} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y)))$
51	4 50	mpi	$⊢ ((K \in HL \land X \in C \land Y \in C) \land (X \subseteq \underset{˙}{⊥} (Y) \land X \neq \emptyset)) \to X \underset{˙}{+} Y = \underset{˙}{⊥} (\underset{˙}{⊥} (X \underset{˙}{+} Y))$

Metamath Proof Explorer

Theorem osumcllem11N

Proof