Theorem omlsilem

Description: Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	omlsilem.1	|- G e. SH
	omlsilem.2	|- H e. SH
	omlsilem.3	|- G C_ H
	omlsilem.4	|- ( H i^i ( _|_ ` G ) ) = 0H
	omlsilem.5	|- A e. H
	omlsilem.6	|- B e. G
	omlsilem.7	|- C e. ( _|_ ` G )
Assertion	omlsilem	|- ( A = ( B +h C ) -> A e. G )

Proof

Step	Hyp	Ref	Expression
1		omlsilem.1	|- G e. SH
2		omlsilem.2	|- H e. SH
3		omlsilem.3	|- G C_ H
4		omlsilem.4	|- ( H i^i ( _|_ ` G ) ) = 0H
5		omlsilem.5	|- A e. H
6		omlsilem.6	|- B e. G
7		omlsilem.7	|- C e. ( _|_ ` G )
8	2 5	shelii	|- A e. ~H
9	1 6	shelii	|- B e. ~H
10		shocss	|- ( G e. SH -> ( _|_ ` G ) C_ ~H )
11	1 10	ax-mp	|- ( _|_ ` G ) C_ ~H
12	11 7	sselii	|- C e. ~H
13	8 9 12	hvsubaddi	|- ( ( A -h B ) = C <-> ( B +h C ) = A )
14		eqcom	|- ( ( B +h C ) = A <-> A = ( B +h C ) )
15	13 14	bitri	|- ( ( A -h B ) = C <-> A = ( B +h C ) )
16	3 6	sselii	|- B e. H
17		shsubcl	|- ( ( H e. SH /\ A e. H /\ B e. H ) -> ( A -h B ) e. H )
18	2 5 16 17	mp3an	|- ( A -h B ) e. H
19		eleq1	|- ( ( A -h B ) = C -> ( ( A -h B ) e. H <-> C e. H ) )
20	18 19	mpbii	|- ( ( A -h B ) = C -> C e. H )
21	15 20	sylbir	|- ( A = ( B +h C ) -> C e. H )
22	4	eleq2i	|- ( C e. ( H i^i ( _|_ ` G ) ) <-> C e. 0H )
23		elin	|- ( C e. ( H i^i ( _|_ ` G ) ) <-> ( C e. H /\ C e. ( _|_ ` G ) ) )
24		elch0	|- ( C e. 0H <-> C = 0h )
25	22 23 24	3bitr3i	|- ( ( C e. H /\ C e. ( _|_ ` G ) ) <-> C = 0h )
26	21 7 25	sylanblc	|- ( A = ( B +h C ) -> C = 0h )
27	26	oveq2d	|- ( A = ( B +h C ) -> ( B +h C ) = ( B +h 0h ) )
28		ax-hvaddid	|- ( B e. ~H -> ( B +h 0h ) = B )
29	9 28	ax-mp	|- ( B +h 0h ) = B
30	27 29	eqtrdi	|- ( A = ( B +h C ) -> ( B +h C ) = B )
31	30 6	eqeltrdi	|- ( A = ( B +h C ) -> ( B +h C ) e. G )
32		eleq1	|- ( A = ( B +h C ) -> ( A e. G <-> ( B +h C ) e. G ) )
33	31 32	mpbird	|- ( A = ( B +h C ) -> A e. G )