Metamath Proof Explorer


Theorem pjfval2

Description: Value of the projection map with implicit domain. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses pjfval2.o = ( ocv ‘ 𝑊 )
pjfval2.p 𝑃 = ( proj1𝑊 )
pjfval2.k 𝐾 = ( proj ‘ 𝑊 )
Assertion pjfval2 𝐾 = ( 𝑥 ∈ dom 𝐾 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 pjfval2.o = ( ocv ‘ 𝑊 )
2 pjfval2.p 𝑃 = ( proj1𝑊 )
3 pjfval2.k 𝐾 = ( proj ‘ 𝑊 )
4 df-mpt ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) }
5 df-xp ( V × ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) }
6 4 5 ineq12i ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) } )
7 eqid ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
8 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 7 8 1 2 3 pjfval 𝐾 = ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) )
10 7 8 1 2 3 pjdm ( 𝑥 ∈ dom 𝐾 ↔ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑥 𝑃 ( 𝑥 ) ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ) )
11 eleq1 ( 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) → ( 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ↔ ( 𝑥 𝑃 ( 𝑥 ) ) ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) )
12 fvex ( Base ‘ 𝑊 ) ∈ V
13 12 12 elmap ( ( 𝑥 𝑃 ( 𝑥 ) ) ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ↔ ( 𝑥 𝑃 ( 𝑥 ) ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) )
14 11 13 bitr2di ( 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) → ( ( 𝑥 𝑃 ( 𝑥 ) ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ↔ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) )
15 14 anbi2d ( 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) → ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑥 𝑃 ( 𝑥 ) ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ) ↔ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) )
16 10 15 syl5bb ( 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) → ( 𝑥 ∈ dom 𝐾 ↔ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) )
17 16 pm5.32ri ( ( 𝑥 ∈ dom 𝐾𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) )
18 an32 ( ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) )
19 vex 𝑥 ∈ V
20 19 biantrur ( 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ↔ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) )
21 20 anbi2i ( ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ↔ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) )
22 17 18 21 3bitri ( ( 𝑥 ∈ dom 𝐾𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) )
23 22 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ dom 𝐾𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) }
24 df-mpt ( 𝑥 ∈ dom 𝐾 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ dom 𝐾𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) }
25 inopab ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) }
26 23 24 25 3eqtr4i ( 𝑥 ∈ dom 𝐾 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( 𝑥 ) ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) } )
27 6 9 26 3eqtr4i 𝐾 = ( 𝑥 ∈ dom 𝐾 ↦ ( 𝑥 𝑃 ( 𝑥 ) ) )