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 ⊢ φ → G dom ⁡ DProd S
dpjfval.2 ⊢ φ → dom ⁡ S = I
dpjfval.p ⊢ P = G dProj S
dpjfval.q ⊢ Q = proj 1 ⁡ G
dpjval.3 ⊢ φ → X ∈ I
Assertion dpjval ⊢ φ → P ⁡ X = S ⁡ X Q G DProd S ↾ I ∖ X

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ φ → G dom ⁡ DProd S
2 dpjfval.2 ⊢ φ → dom ⁡ S = I
3 dpjfval.p ⊢ P = G dProj S
4 dpjfval.q ⊢ Q = proj 1 ⁡ G
5 dpjval.3 ⊢ φ → X ∈ I
6 1 2 3 4 dpjfval ⊢ φ → P = x ∈ I ⟼ S ⁡ x Q G DProd S ↾ I ∖ x
7 simpr ⊢ φ ∧ x = X → x = X
8 7 fveq2d ⊢ φ ∧ x = X → S ⁡ x = S ⁡ X
9 7 sneqd ⊢ φ ∧ x = X → x = X
10 9 difeq2d ⊢ φ ∧ x = X → I ∖ x = I ∖ X
11 10 reseq2d ⊢ φ ∧ x = X → S ↾ I ∖ x = S ↾ I ∖ X
12 11 oveq2d ⊢ φ ∧ x = X → G DProd S ↾ I ∖ x = G DProd S ↾ I ∖ X
13 8 12 oveq12d ⊢ φ ∧ x = X → S ⁡ x Q G DProd S ↾ I ∖ x = S ⁡ X Q G DProd S ↾ I ∖ X
14 ovexd ⊢ φ → S ⁡ X Q G DProd S ↾ I ∖ X ∈ V
15 6 13 5 14 fvmptd ⊢ φ → P ⁡ X = S ⁡ X Q G DProd S ↾ I ∖ X