Theorem pjf

Description: A projection is a function on the base set. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	pjf.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
	pjf.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion	pjf	⊢ ( 𝑇 ∈ dom 𝐾 → ( 𝐾 ‘ 𝑇 ) : 𝑉 ⟶ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		pjf.k	⊢ 𝐾 = ( proj ‘ 𝑊 )
2		pjf.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
4		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
5		eqid	⊢ ( proj1 ‘ 𝑊 ) = ( proj1 ‘ 𝑊 )
6	2 3 4 5 1	pjdm	⊢ ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) )
7	6	simprbi	⊢ ( 𝑇 ∈ dom 𝐾 → ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 )
8	4 5 1	pjval	⊢ ( 𝑇 ∈ dom 𝐾 → ( 𝐾 ‘ 𝑇 ) = ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) )
9	8	feq1d	⊢ ( 𝑇 ∈ dom 𝐾 → ( ( 𝐾 ‘ 𝑇 ) : 𝑉 ⟶ 𝑉 ↔ ( 𝑇 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) )
10	7 9	mpbird	⊢ ( 𝑇 ∈ dom 𝐾 → ( 𝐾 ‘ 𝑇 ) : 𝑉 ⟶ 𝑉 )