Metamath Proof Explorer

Theorem dpjrid

Description: The Y -th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
dpjlid.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
dpjlid.4 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) )
dpjrid.0 ⊢ 0 = ( 0g ‘ 𝐺 )
dpjrid.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
dpjrid.6 ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
Assertion dpjrid ( 𝜑 → ( ( 𝑃 ‘ 𝑌 ) ‘ 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4 dpjlid.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5 dpjlid.4 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 ‘ 𝑋 ) )
6 dpjrid.0 ⊢ 0 = ( 0g ‘ 𝐺 )
7 dpjrid.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
8 dpjrid.6 ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
9 fveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝑃 ‘ 𝑥 ) = ( 𝑃 ‘ 𝑌 ) )
10 9 fveq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = ( ( 𝑃 ‘ 𝑌 ) ‘ 𝐴 ) )
11 eqeq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 = 𝑋 ↔ 𝑌 = 𝑋 ) )
12 11 ifbid ⊢ ( 𝑥 = 𝑌 → if ( 𝑥 = 𝑋 , 𝐴 , 0 ) = if ( 𝑌 = 𝑋 , 𝐴 , 0 ) )
13 10 12 eqeq12d ⊢ ( 𝑥 = 𝑌 → ( ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ↔ ( ( 𝑃 ‘ 𝑌 ) ‘ 𝐴 ) = if ( 𝑌 = 𝑋 , 𝐴 , 0 ) ) )
14 eqid ⊢ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 } = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
15 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) )
16 6 14 1 2 4 5 15 dprdfid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 } ∧ ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ) = 𝐴 ) )
17 16 simprd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ) = 𝐴 )
18 17 eqcomd ⊢ ( 𝜑 → 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ) )
19 1 2 4 dprdub ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝐺 DProd 𝑆 ) )
20 19 5 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 DProd 𝑆 ) )
21 16 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ∈ { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 } )
22 1 2 3 20 6 14 21 dpjeq ⊢ ( 𝜑 → ( 𝐴 = ( 𝐺 Σg ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = if ( 𝑥 = 𝑋 , 𝐴 , 0 ) ) )
23 18 22 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ( 𝑃 ‘ 𝑥 ) ‘ 𝐴 ) = if ( 𝑥 = 𝑋 , 𝐴 , 0 ) )
24 13 23 7 rspcdva ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑌 ) ‘ 𝐴 ) = if ( 𝑌 = 𝑋 , 𝐴 , 0 ) )
25 ifnefalse ⊢ ( 𝑌 ≠ 𝑋 → if ( 𝑌 = 𝑋 , 𝐴 , 0 ) = 0 )
26 8 25 syl ⊢ ( 𝜑 → if ( 𝑌 = 𝑋 , 𝐴 , 0 ) = 0 )
27 24 26 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝑌 ) ‘ 𝐴 ) = 0 )