Theorem 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 e. SH
	shjshs.2	|- B e. SH
Assertion	shjshsi	|- ( A vH B ) = ( _|_ ` ( _|_ ` ( A +H B ) ) )

Proof

Step	Hyp	Ref	Expression
1		shjshs.1	|- A e. SH
2		shjshs.2	|- B e. SH
3		shjval	|- ( ( A e. SH /\ B e. SH ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) )
4	1 2 3	mp2an	|- ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) )
5	1 2	shunssi	|- ( A u. B ) C_ ( A +H B )
6	1	shssii	|- A C_ ~H
7	2	shssii	|- B C_ ~H
8	6 7	unssi	|- ( A u. B ) C_ ~H
9	1 2	shscli	|- ( A +H B ) e. SH
10	9	shssii	|- ( A +H B ) C_ ~H
11	8 10	occon2i	|- ( ( A u. B ) C_ ( A +H B ) -> ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) ) )
12	5 11	ax-mp	|- ( _|_ ` ( _|_ ` ( A u. B ) ) ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) )
13	4 12	eqsstri	|- ( A vH B ) C_ ( _|_ ` ( _|_ ` ( A +H B ) ) )
14	1 2	shsleji	|- ( A +H B ) C_ ( A vH B )
15	1 2	shjcli	|- ( A vH B ) e. CH
16	15	chssii	|- ( A vH B ) C_ ~H
17		occon	|- ( ( ( A +H B ) C_ ~H /\ ( A vH B ) C_ ~H ) -> ( ( A +H B ) C_ ( A vH B ) -> ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) ) )
18	10 16 17	mp2an	|- ( ( A +H B ) C_ ( A vH B ) -> ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) )
19	14 18	ax-mp	|- ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) )
20		occl	|- ( ( A +H B ) C_ ~H -> ( _|_ ` ( A +H B ) ) e. CH )
21	10 20	ax-mp	|- ( _|_ ` ( A +H B ) ) e. CH
22	15 21	chsscon1i	|- ( ( _|_ ` ( A vH B ) ) C_ ( _|_ ` ( A +H B ) ) <-> ( _|_ ` ( _|_ ` ( A +H B ) ) ) C_ ( A vH B ) )
23	19 22	mpbi	|- ( _|_ ` ( _|_ ` ( A +H B ) ) ) C_ ( A vH B )
24	13 23	eqssi	|- ( A vH B ) = ( _|_ ` ( _|_ ` ( A +H B ) ) )