This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )