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 bitrid ⊢ ( 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) → ( 𝑥 ∈ 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 𝐾 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) )