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 ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )