Metamath Proof Explorer

Theorem dpjfval

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 ‘ 𝐺 )
Assertion dpjfval ( 𝜑 → 𝑃 = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dpjfval.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2 dpjfval.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3 dpjfval.p ⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4 dpjfval.q ⊢ 𝑄 = ( proj1 ‘ 𝐺 )
5 df-dpj ⊢ dProj = ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj1 ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) )
6 5 a1i ⊢ ( 𝜑 → dProj = ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj1 ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) ) )
7 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → 𝑠 = 𝑆 )
8 7 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → dom 𝑠 = dom 𝑆 )
9 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → dom 𝑆 = 𝐼 )
10 8 9 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → dom 𝑠 = 𝐼 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → 𝑔 = 𝐺 )
12 11 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( proj1 ‘ 𝑔 ) = ( proj1 ‘ 𝐺 ) )
13 12 4 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( proj1 ‘ 𝑔 ) = 𝑄 )
14 7 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( 𝑠 ‘ 𝑖 ) = ( 𝑆 ‘ 𝑖 ) )
15 10 difeq1d ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( dom 𝑠 ∖ { 𝑖 } ) = ( 𝐼 ∖ { 𝑖 } ) )
16 7 15 reseq12d ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) = ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) )
17 11 16 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) = ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) )
18 13 14 17 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( ( 𝑠 ‘ 𝑖 ) ( proj1 ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) = ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) )
19 10 18 mpteq12dv ⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj1 ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) )
20 simpr ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
21 20 sneqd ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → { 𝑔 } = { 𝐺 } )
22 21 imaeq2d ⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( dom DProd “ { 𝑔 } ) = ( dom DProd “ { 𝐺 } ) )
23 dprdgrp ⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
24 1 23 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
25 reldmdprd ⊢ Rel dom DProd
26 elrelimasn ⊢ ( Rel dom DProd → ( 𝑆 ∈ ( dom DProd “ { 𝐺 } ) ↔ 𝐺 dom DProd 𝑆 ) )
27 25 26 ax-mp ⊢ ( 𝑆 ∈ ( dom DProd “ { 𝐺 } ) ↔ 𝐺 dom DProd 𝑆 )
28 1 27 sylibr ⊢ ( 𝜑 → 𝑆 ∈ ( dom DProd “ { 𝐺 } ) )
29 1 2 dprddomcld ⊢ ( 𝜑 → 𝐼 ∈ V )
30 29 mptexd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) ∈ V )
31 6 19 22 24 28 30 ovmpodx ⊢ ( 𝜑 → ( 𝐺 dProj 𝑆 ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) )
32 3 31 eqtrid ⊢ ( 𝜑 → 𝑃 = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) )