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

Metamath Proof Explorer

Theorem dprd2db

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprd2d.1 ⊢ ( 𝜑 → Rel 𝐴 )
dprd2d.2 ⊢ ( 𝜑 → 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
dprd2d.3 ⊢ ( 𝜑 → dom 𝐴 ⊆ 𝐼 )
dprd2d.4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) )
dprd2d.5 ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
dprd2d.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion dprd2db ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( 𝐺 DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dprd2d.1 ⊢ ( 𝜑 → Rel 𝐴 )
2 dprd2d.2 ⊢ ( 𝜑 → 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
3 dprd2d.3 ⊢ ( 𝜑 → dom 𝐴 ⊆ 𝐼 )
4 dprd2d.4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) )
5 dprd2d.5 ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
6 dprd2d.k ⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
7 1 2 3 4 5 6 dprd2da ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
8 6 dprdspan ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) = ( 𝐾 ‘ ∪ ran 𝑆 ) )
9 7 8 syl ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( 𝐾 ‘ ∪ ran 𝑆 ) )
10 relssres ⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ 𝐼 ) → ( 𝐴 ↾ 𝐼 ) = 𝐴 )
11 1 3 10 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↾ 𝐼 ) = 𝐴 )
12 11 imaeq2d ⊢ ( 𝜑 → ( 𝑆 “ ( 𝐴 ↾ 𝐼 ) ) = ( 𝑆 “ 𝐴 ) )
13 ffn ⊢ ( 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) → 𝑆 Fn 𝐴 )
14 fnima ⊢ ( 𝑆 Fn 𝐴 → ( 𝑆 “ 𝐴 ) = ran 𝑆 )
15 2 13 14 3syl ⊢ ( 𝜑 → ( 𝑆 “ 𝐴 ) = ran 𝑆 )
16 12 15 eqtr2d ⊢ ( 𝜑 → ran 𝑆 = ( 𝑆 “ ( 𝐴 ↾ 𝐼 ) ) )
17 16 unieqd ⊢ ( 𝜑 → ∪ ran 𝑆 = ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐼 ) ) )
18 17 fveq2d ⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ran 𝑆 ) = ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐼 ) ) ) )
19 ssidd ⊢ ( 𝜑 → 𝐼 ⊆ 𝐼 )
20 1 2 3 4 5 6 19 dprd2dlem1 ⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐼 ) ) ) = ( 𝐺 DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )
21 9 18 20 3eqtrd ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( 𝐺 DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )