Metamath Proof Explorer


Theorem pjdm

Description: A subspace is in the domain of the projection function iff the subspace admits a projection decomposition of the whole space. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjfval.v 𝑉 = ( Base ‘ 𝑊 )
pjfval.l 𝐿 = ( LSubSp ‘ 𝑊 )
pjfval.o = ( ocv ‘ 𝑊 )
pjfval.p 𝑃 = ( proj1𝑊 )
pjfval.k 𝐾 = ( proj ‘ 𝑊 )
Assertion pjdm ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇𝐿 ∧ ( 𝑇 𝑃 ( 𝑇 ) ) : 𝑉𝑉 ) )

Proof

Step Hyp Ref Expression
1 pjfval.v 𝑉 = ( Base ‘ 𝑊 )
2 pjfval.l 𝐿 = ( LSubSp ‘ 𝑊 )
3 pjfval.o = ( ocv ‘ 𝑊 )
4 pjfval.p 𝑃 = ( proj1𝑊 )
5 pjfval.k 𝐾 = ( proj ‘ 𝑊 )
6 id ( 𝑥 = 𝑇𝑥 = 𝑇 )
7 fveq2 ( 𝑥 = 𝑇 → ( 𝑥 ) = ( 𝑇 ) )
8 6 7 oveq12d ( 𝑥 = 𝑇 → ( 𝑥 𝑃 ( 𝑥 ) ) = ( 𝑇 𝑃 ( 𝑇 ) ) )
9 8 eleq1d ( 𝑥 = 𝑇 → ( ( 𝑥 𝑃 ( 𝑥 ) ) ∈ ( 𝑉m 𝑉 ) ↔ ( 𝑇 𝑃 ( 𝑇 ) ) ∈ ( 𝑉m 𝑉 ) ) )
10 1 fvexi 𝑉 ∈ V
11 10 10 elmap ( ( 𝑇 𝑃 ( 𝑇 ) ) ∈ ( 𝑉m 𝑉 ) ↔ ( 𝑇 𝑃 ( 𝑇 ) ) : 𝑉𝑉 )
12 9 11 bitrdi ( 𝑥 = 𝑇 → ( ( 𝑥 𝑃 ( 𝑥 ) ) ∈ ( 𝑉m 𝑉 ) ↔ ( 𝑇 𝑃 ( 𝑇 ) ) : 𝑉𝑉 ) )
13 cnvin ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) = ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) )
14 cnvxp ( V × ( 𝑉m 𝑉 ) ) = ( ( 𝑉m 𝑉 ) × V )
15 14 ineq2i ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) = ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( ( 𝑉m 𝑉 ) × V ) )
16 13 15 eqtri ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) ) = ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( ( 𝑉m 𝑉 ) × V ) )
17 1 2 3 4 5 pjfval 𝐾 = ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) )
18 17 cnveqi 𝐾 = ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( V × ( 𝑉m 𝑉 ) ) )
19 df-res ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ↾ ( 𝑉m 𝑉 ) ) = ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( ( 𝑉m 𝑉 ) × V ) )
20 16 18 19 3eqtr4i 𝐾 = ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ↾ ( 𝑉m 𝑉 ) )
21 20 rneqi ran 𝐾 = ran ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ↾ ( 𝑉m 𝑉 ) )
22 dfdm4 dom 𝐾 = ran 𝐾
23 df-ima ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) “ ( 𝑉m 𝑉 ) ) = ran ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ↾ ( 𝑉m 𝑉 ) )
24 21 22 23 3eqtr4i dom 𝐾 = ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) “ ( 𝑉m 𝑉 ) )
25 eqid ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) = ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) )
26 25 mptpreima ( ( 𝑥𝐿 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) “ ( 𝑉m 𝑉 ) ) = { 𝑥𝐿 ∣ ( 𝑥 𝑃 ( 𝑥 ) ) ∈ ( 𝑉m 𝑉 ) }
27 24 26 eqtri dom 𝐾 = { 𝑥𝐿 ∣ ( 𝑥 𝑃 ( 𝑥 ) ) ∈ ( 𝑉m 𝑉 ) }
28 12 27 elrab2 ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇𝐿 ∧ ( 𝑇 𝑃 ( 𝑇 ) ) : 𝑉𝑉 ) )