Theorem cssincl

Description: The zero subspace is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypothesis	css0.c	|- C = ( ClSubSp ` W )
Assertion	cssincl	|- ( ( W e. PreHil /\ A e. C /\ B e. C ) -> ( A i^i B ) e. C )

Proof

Step	Hyp	Ref	Expression
1		css0.c	|- C = ( ClSubSp ` W )
2		eqid	|- ( Base ` W ) = ( Base ` W )
3		eqid	|- ( ocv ` W ) = ( ocv ` W )
4	2 3	ocvss	|- ( ( ocv ` W ) ` A ) C_ ( Base ` W )
5	2 3	ocvss	|- ( ( ocv ` W ) ` B ) C_ ( Base ` W )
6	4 5	unssi	|- ( ( ( ocv ` W ) ` A ) u. ( ( ocv ` W ) ` B ) ) C_ ( Base ` W )
7	2 1 3	ocvcss	|- ( ( W e. PreHil /\ ( ( ( ocv ` W ) ` A ) u. ( ( ocv ` W ) ` B ) ) C_ ( Base ` W ) ) -> ( ( ocv ` W ) ` ( ( ( ocv ` W ) ` A ) u. ( ( ocv ` W ) ` B ) ) ) e. C )
8	6 7	mpan2	|- ( W e. PreHil -> ( ( ocv ` W ) ` ( ( ( ocv ` W ) ` A ) u. ( ( ocv ` W ) ` B ) ) ) e. C )
9	3 1	cssi	|- ( A e. C -> A = ( ( ocv ` W ) ` ( ( ocv ` W ) ` A ) ) )
10	3 1	cssi	|- ( B e. C -> B = ( ( ocv ` W ) ` ( ( ocv ` W ) ` B ) ) )
11	9 10	ineqan12d	|- ( ( A e. C /\ B e. C ) -> ( A i^i B ) = ( ( ( ocv ` W ) ` ( ( ocv ` W ) ` A ) ) i^i ( ( ocv ` W ) ` ( ( ocv ` W ) ` B ) ) ) )
12	3	unocv	|- ( ( ocv ` W ) ` ( ( ( ocv ` W ) ` A ) u. ( ( ocv ` W ) ` B ) ) ) = ( ( ( ocv ` W ) ` ( ( ocv ` W ) ` A ) ) i^i ( ( ocv ` W ) ` ( ( ocv ` W ) ` B ) ) )
13	11 12	eqtr4di	|- ( ( A e. C /\ B e. C ) -> ( A i^i B ) = ( ( ocv ` W ) ` ( ( ( ocv ` W ) ` A ) u. ( ( ocv ` W ) ` B ) ) ) )
14	13	eleq1d	|- ( ( A e. C /\ B e. C ) -> ( ( A i^i B ) e. C <-> ( ( ocv ` W ) ` ( ( ( ocv ` W ) ` A ) u. ( ( ocv ` W ) ` B ) ) ) e. C ) )
15	8 14	syl5ibrcom	|- ( W e. PreHil -> ( ( A e. C /\ B e. C ) -> ( A i^i B ) e. C ) )
16	15	3impib	|- ( ( W e. PreHil /\ A e. C /\ B e. C ) -> ( A i^i B ) e. C )