Theorem pjth2

Description: Projection Theorem with abbreviations: A topologically closed subspace is a projection subspace. (Contributed by Mario Carneiro, 17-Oct-2015)

	Ref	Expression
Hypotheses	pjth2.j	|- J = ( TopOpen ` W )
	pjth2.l	|- L = ( LSubSp ` W )
	pjth2.k	|- K = ( proj ` W )
Assertion	pjth2	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> U e. dom K )

Proof

Step	Hyp	Ref	Expression
1		pjth2.j	|- J = ( TopOpen ` W )
2		pjth2.l	|- L = ( LSubSp ` W )
3		pjth2.k	|- K = ( proj ` W )
4		simp2	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> U e. L )
5		eqid	|- ( Base ` W ) = ( Base ` W )
6		eqid	|- ( LSSum ` W ) = ( LSSum ` W )
7		eqid	|- ( ocv ` W ) = ( ocv ` W )
8	5 6 7 1 2	pjth	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> ( U ( LSSum ` W ) ( ( ocv ` W ) ` U ) ) = ( Base ` W ) )
9		hlphl	|- ( W e. CHil -> W e. PreHil )
10	9	3ad2ant1	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> W e. PreHil )
11	5 2 7 6 3	pjdm2	|- ( W e. PreHil -> ( U e. dom K <-> ( U e. L /\ ( U ( LSSum ` W ) ( ( ocv ` W ) ` U ) ) = ( Base ` W ) ) ) )
12	10 11	syl	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> ( U e. dom K <-> ( U e. L /\ ( U ( LSSum ` W ) ( ( ocv ` W ) ` U ) ) = ( Base ` W ) ) ) )
13	4 8 12	mpbir2and	|- ( ( W e. CHil /\ U e. L /\ U e. ( Clsd ` J ) ) -> U e. dom K )