shjshsi

Description: Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shjshs.1	$⊢ A \in S_{ℋ}$
	shjshs.2	$⊢ B \in S_{ℋ}$
Assertion	shjshsi	$⊢ A \lor_{ℋ} B = ⊥ (⊥ (A +_{ℋ} B))$

Proof

Step	Hyp	Ref	Expression
1		shjshs.1	$⊢ A \in S_{ℋ}$
2		shjshs.2	$⊢ B \in S_{ℋ}$
3		shjval	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A \lor_{ℋ} B = ⊥ (⊥ (A \cup B))$
4	1 2 3	mp2an	$⊢ A \lor_{ℋ} B = ⊥ (⊥ (A \cup B))$
5	1 2	shunssi	$⊢ A \cup B \subseteq A +_{ℋ} B$
6	1	shssii	$⊢ A \subseteq ℋ$
7	2	shssii	$⊢ B \subseteq ℋ$
8	6 7	unssi	$⊢ A \cup B \subseteq ℋ$
9	1 2	shscli	$⊢ A +_{ℋ} B \in S_{ℋ}$
10	9	shssii	$⊢ A +_{ℋ} B \subseteq ℋ$
11	8 10	occon2i	$⊢ A \cup B \subseteq A +_{ℋ} B \to ⊥ (⊥ (A \cup B)) \subseteq ⊥ (⊥ (A +_{ℋ} B))$
12	5 11	ax-mp	$⊢ ⊥ (⊥ (A \cup B)) \subseteq ⊥ (⊥ (A +_{ℋ} B))$
13	4 12	eqsstri	$⊢ A \lor_{ℋ} B \subseteq ⊥ (⊥ (A +_{ℋ} B))$
14	1 2	shsleji	$⊢ A +_{ℋ} B \subseteq A \lor_{ℋ} B$
15	1 2	shjcli	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
16	15	chssii	$⊢ A \lor_{ℋ} B \subseteq ℋ$
17		occon	$⊢ (A +_{ℋ} B \subseteq ℋ \land A \lor_{ℋ} B \subseteq ℋ) \to (A +_{ℋ} B \subseteq A \lor_{ℋ} B \to ⊥ (A \lor_{ℋ} B) \subseteq ⊥ (A +_{ℋ} B))$
18	10 16 17	mp2an	$⊢ A +_{ℋ} B \subseteq A \lor_{ℋ} B \to ⊥ (A \lor_{ℋ} B) \subseteq ⊥ (A +_{ℋ} B)$
19	14 18	ax-mp	$⊢ ⊥ (A \lor_{ℋ} B) \subseteq ⊥ (A +_{ℋ} B)$
20		occl	$⊢ A +_{ℋ} B \subseteq ℋ \to ⊥ (A +_{ℋ} B) \in C_{ℋ}$
21	10 20	ax-mp	$⊢ ⊥ (A +_{ℋ} B) \in C_{ℋ}$
22	15 21	chsscon1i	$⊢ ⊥ (A \lor_{ℋ} B) \subseteq ⊥ (A +_{ℋ} B) \leftrightarrow ⊥ (⊥ (A +_{ℋ} B)) \subseteq A \lor_{ℋ} B$
23	19 22	mpbi	$⊢ ⊥ (⊥ (A +_{ℋ} B)) \subseteq A \lor_{ℋ} B$
24	13 23	eqssi	$⊢ A \lor_{ℋ} B = ⊥ (⊥ (A +_{ℋ} B))$

Metamath Proof Explorer

Theorem shjshsi

Proof