This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dpjval

Description: Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
dpjfval.q ⊢ 𝑄 = ( proj1 ‘ 𝐺 )
dpjval.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion dpjval ( 𝜑 → ( 𝑃 ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4 dpjfval.q ⊢ 𝑄 = ( proj1 ‘ 𝐺 )
5 dpjval.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
6 1 2 3 4 dpjfval ⊢ ( 𝜑 → 𝑃 = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑥 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ) )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
8 7 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑋 ) )
9 7 sneqd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → { 𝑥 } = { 𝑋 } )
10 9 difeq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐼 ∖ { 𝑥 } ) = ( 𝐼 ∖ { 𝑋 } ) )
11 10 reseq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) )
12 11 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) = ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) )
13 8 12 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑆 ‘ 𝑥 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = ( ( 𝑆 ‘ 𝑋 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
14 ovexd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∈ V )
15 6 13 5 14 fvmptd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )