Metamath Proof Explorer

Theorem pjfval

Description: The value of the projection function. (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 pjfval 𝐾 = ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) )

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 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = ( LSubSp ‘ 𝑊 ) )
7 6 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ 𝑤 ) = 𝐿 )
8 fveq2 ⊢ ( 𝑤 = 𝑊 → ( proj1 ‘ 𝑤 ) = ( proj1 ‘ 𝑊 ) )
9 8 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( proj1 ‘ 𝑤 ) = 𝑃 )
10 eqidd ⊢ ( 𝑤 = 𝑊 → 𝑥 = 𝑥 )
11 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ocv ‘ 𝑤 ) = ( ocv ‘ 𝑊 ) )
12 11 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ocv ‘ 𝑤 ) = ⊥ )
13 12 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( ocv ‘ 𝑤 ) ‘ 𝑥 ) = ( ⊥ ‘ 𝑥 ) )
14 9 10 13 oveq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ( proj1 ‘ 𝑤 ) ( ( ocv ‘ 𝑤 ) ‘ 𝑥 ) ) = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) )
15 7 14 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( LSubSp ‘ 𝑤 ) ↦ ( 𝑥 ( proj1 ‘ 𝑤 ) ( ( ocv ‘ 𝑤 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) )
16 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
17 16 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
18 17 17 oveq12d ⊢ ( 𝑤 = 𝑊 → ( ( Base ‘ 𝑤 ) ↑m ( Base ‘ 𝑤 ) ) = ( 𝑉 ↑m 𝑉 ) )
19 18 xpeq2d ⊢ ( 𝑤 = 𝑊 → ( V × ( ( Base ‘ 𝑤 ) ↑m ( Base ‘ 𝑤 ) ) ) = ( V × ( 𝑉 ↑m 𝑉 ) ) )
20 15 19 ineq12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ∈ ( LSubSp ‘ 𝑤 ) ↦ ( 𝑥 ( proj1 ‘ 𝑤 ) ( ( ocv ‘ 𝑤 ) ‘ 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ 𝑤 ) ↑m ( Base ‘ 𝑤 ) ) ) ) = ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) )
21 df-pj ⊢ proj = ( 𝑤 ∈ V ↦ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑤 ) ↦ ( 𝑥 ( proj1 ‘ 𝑤 ) ( ( ocv ‘ 𝑤 ) ‘ 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ 𝑤 ) ↑m ( Base ‘ 𝑤 ) ) ) ) )
22 2 fvexi ⊢ 𝐿 ∈ V
23 22 inex1 ⊢ ( 𝐿 ∩ V ) ∈ V
24 ovex ⊢ ( 𝑉 ↑m 𝑉 ) ∈ V
25 24 inex2 ⊢ ( V ∩ ( 𝑉 ↑m 𝑉 ) ) ∈ V
26 23 25 xpex ⊢ ( ( 𝐿 ∩ V ) × ( V ∩ ( 𝑉 ↑m 𝑉 ) ) ) ∈ V
27 eqid ⊢ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) )
28 ovexd ⊢ ( 𝑥 ∈ 𝐿 → ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ∈ V )
29 27 28 fmpti ⊢ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) : 𝐿 ⟶ V
30 fssxp ⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) : 𝐿 ⟶ V → ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ⊆ ( 𝐿 × V ) )
31 ssrin ⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ⊆ ( 𝐿 × V ) → ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ⊆ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) )
32 29 30 31 mp2b ⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ⊆ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) )
33 inxp ⊢ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) = ( ( 𝐿 ∩ V ) × ( V ∩ ( 𝑉 ↑m 𝑉 ) ) )
34 32 33 sseqtri ⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ⊆ ( ( 𝐿 ∩ V ) × ( V ∩ ( 𝑉 ↑m 𝑉 ) ) )
35 26 34 ssexi ⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ∈ V
36 20 21 35 fvmpt ⊢ ( 𝑊 ∈ V → ( proj ‘ 𝑊 ) = ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) )
37 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( proj ‘ 𝑊 ) = ∅ )
38 inss1 ⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ⊆ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) )
39 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( LSubSp ‘ 𝑊 ) = ∅ )
40 2 39 syl5eq ⊢ ( ¬ 𝑊 ∈ V → 𝐿 = ∅ )
41 40 mpteq1d ⊢ ( ¬ 𝑊 ∈ V → ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) )
42 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = ∅
43 41 42 eqtrdi ⊢ ( ¬ 𝑊 ∈ V → ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = ∅ )
44 sseq0 ⊢ ( ( ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ⊆ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = ∅ ) → ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) = ∅ )
45 38 43 44 sylancr ⊢ ( ¬ 𝑊 ∈ V → ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) = ∅ )
46 37 45 eqtr4d ⊢ ( ¬ 𝑊 ∈ V → ( proj ‘ 𝑊 ) = ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) )
47 36 46 pm2.61i ⊢ ( proj ‘ 𝑊 ) = ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) )
48 5 47 eqtri ⊢ 𝐾 = ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) )