sshhococi

Description: The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements). (Contributed by NM, 1-Jun-2004) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sshjococ.1	$⊢ A \subseteq ℋ$
	sshjococ.2	$⊢ B \subseteq ℋ$
Assertion	sshhococi	$⊢ A \lor_{ℋ} B = ⊥ (⊥ (A)) \lor_{ℋ} ⊥ (⊥ (B))$

Proof

Step	Hyp	Ref	Expression
1		sshjococ.1	$⊢ A \subseteq ℋ$
2		sshjococ.2	$⊢ B \subseteq ℋ$
3		ococss	$⊢ A \subseteq ℋ \to A \subseteq ⊥ (⊥ (A))$
4	1 3	ax-mp	$⊢ A \subseteq ⊥ (⊥ (A))$
5		ococss	$⊢ B \subseteq ℋ \to B \subseteq ⊥ (⊥ (B))$
6	2 5	ax-mp	$⊢ B \subseteq ⊥ (⊥ (B))$
7		unss12	$⊢ (A \subseteq ⊥ (⊥ (A)) \land B \subseteq ⊥ (⊥ (B))) \to A \cup B \subseteq ⊥ (⊥ (A)) \cup ⊥ (⊥ (B))$
8	4 6 7	mp2an	$⊢ A \cup B \subseteq ⊥ (⊥ (A)) \cup ⊥ (⊥ (B))$
9	1 2	unssi	$⊢ A \cup B \subseteq ℋ$
10		occl	$⊢ A \subseteq ℋ \to ⊥ (A) \in C_{ℋ}$
11	1 10	ax-mp	$⊢ ⊥ (A) \in C_{ℋ}$
12	11	choccli	$⊢ ⊥ (⊥ (A)) \in C_{ℋ}$
13	12	chssii	$⊢ ⊥ (⊥ (A)) \subseteq ℋ$
14		occl	$⊢ B \subseteq ℋ \to ⊥ (B) \in C_{ℋ}$
15	2 14	ax-mp	$⊢ ⊥ (B) \in C_{ℋ}$
16	15	choccli	$⊢ ⊥ (⊥ (B)) \in C_{ℋ}$
17	16	chssii	$⊢ ⊥ (⊥ (B)) \subseteq ℋ$
18	13 17	unssi	$⊢ ⊥ (⊥ (A)) \cup ⊥ (⊥ (B)) \subseteq ℋ$
19	9 18	occon2i	$⊢ A \cup B \subseteq ⊥ (⊥ (A)) \cup ⊥ (⊥ (B)) \to ⊥ (⊥ (A \cup B)) \subseteq ⊥ (⊥ (⊥ (⊥ (A)) \cup ⊥ (⊥ (B))))$
20	8 19	ax-mp	$⊢ ⊥ (⊥ (A \cup B)) \subseteq ⊥ (⊥ (⊥ (⊥ (A)) \cup ⊥ (⊥ (B))))$
21		sshjval	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to A \lor_{ℋ} B = ⊥ (⊥ (A \cup B))$
22	1 2 21	mp2an	$⊢ A \lor_{ℋ} B = ⊥ (⊥ (A \cup B))$
23	12 16	chjvali	$⊢ ⊥ (⊥ (A)) \lor_{ℋ} ⊥ (⊥ (B)) = ⊥ (⊥ (⊥ (⊥ (A)) \cup ⊥ (⊥ (B))))$
24	20 22 23	3sstr4i	$⊢ A \lor_{ℋ} B \subseteq ⊥ (⊥ (A)) \lor_{ℋ} ⊥ (⊥ (B))$
25		ssun1	$⊢ A \subseteq A \cup B$
26		ococss	$⊢ A \cup B \subseteq ℋ \to A \cup B \subseteq ⊥ (⊥ (A \cup B))$
27	9 26	ax-mp	$⊢ A \cup B \subseteq ⊥ (⊥ (A \cup B))$
28	25 27	sstri	$⊢ A \subseteq ⊥ (⊥ (A \cup B))$
29	28 22	sseqtrri	$⊢ A \subseteq A \lor_{ℋ} B$
30		sshjcl	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to A \lor_{ℋ} B \in C_{ℋ}$
31	1 2 30	mp2an	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
32	31	chssii	$⊢ A \lor_{ℋ} B \subseteq ℋ$
33	1 32	occon2i	$⊢ A \subseteq A \lor_{ℋ} B \to ⊥ (⊥ (A)) \subseteq ⊥ (⊥ (A \lor_{ℋ} B))$
34	29 33	ax-mp	$⊢ ⊥ (⊥ (A)) \subseteq ⊥ (⊥ (A \lor_{ℋ} B))$
35		ssun2	$⊢ B \subseteq A \cup B$
36	35 27	sstri	$⊢ B \subseteq ⊥ (⊥ (A \cup B))$
37	36 22	sseqtrri	$⊢ B \subseteq A \lor_{ℋ} B$
38	2 32	occon2i	$⊢ B \subseteq A \lor_{ℋ} B \to ⊥ (⊥ (B)) \subseteq ⊥ (⊥ (A \lor_{ℋ} B))$
39	37 38	ax-mp	$⊢ ⊥ (⊥ (B)) \subseteq ⊥ (⊥ (A \lor_{ℋ} B))$
40	31	choccli	$⊢ ⊥ (A \lor_{ℋ} B) \in C_{ℋ}$
41	40	choccli	$⊢ ⊥ (⊥ (A \lor_{ℋ} B)) \in C_{ℋ}$
42	12 16 41	chlubii	$⊢ (⊥ (⊥ (A)) \subseteq ⊥ (⊥ (A \lor_{ℋ} B)) \land ⊥ (⊥ (B)) \subseteq ⊥ (⊥ (A \lor_{ℋ} B))) \to ⊥ (⊥ (A)) \lor_{ℋ} ⊥ (⊥ (B)) \subseteq ⊥ (⊥ (A \lor_{ℋ} B))$
43	34 39 42	mp2an	$⊢ ⊥ (⊥ (A)) \lor_{ℋ} ⊥ (⊥ (B)) \subseteq ⊥ (⊥ (A \lor_{ℋ} B))$
44	31	ococi	$⊢ ⊥ (⊥ (A \lor_{ℋ} B)) = A \lor_{ℋ} B$
45	43 44	sseqtri	$⊢ ⊥ (⊥ (A)) \lor_{ℋ} ⊥ (⊥ (B)) \subseteq A \lor_{ℋ} B$
46	24 45	eqssi	$⊢ A \lor_{ℋ} B = ⊥ (⊥ (A)) \lor_{ℋ} ⊥ (⊥ (B))$

Metamath Proof Explorer

Theorem sshhococi

Proof