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	⊢ 𝑃 = ( proj₁ ‘ 𝑊 )
	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	⊢ 𝑃 = ( proj₁ ‘ 𝑊 )
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 𝐾 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) )

Metamath Proof Explorer

Theorem pjdm

Proof