dprd2dlem2

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-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	dprd2dlem2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) ) )

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		df-ov	⊢ ( ( 1^st ‘ 𝑋 ) 𝑆 ( 2^nd ‘ 𝑋 ) ) = ( 𝑆 ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
8		1st2nd	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
9	1 8	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
11	9 10	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝐴 )
12		df-br	⊢ ( ( 1^st ‘ 𝑋 ) 𝐴 ( 2^nd ‘ 𝑋 ) ↔ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ∈ 𝐴 )
13	11 12	sylibr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 1^st ‘ 𝑋 ) 𝐴 ( 2^nd ‘ 𝑋 ) )
14	1	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → Rel 𝐴 )
15		elrelimasn	⊢ ( Rel 𝐴 → ( ( 2^nd ‘ 𝑋 ) ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↔ ( 1^st ‘ 𝑋 ) 𝐴 ( 2^nd ‘ 𝑋 ) ) )
16	14 15	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 2^nd ‘ 𝑋 ) ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↔ ( 1^st ‘ 𝑋 ) 𝐴 ( 2^nd ‘ 𝑋 ) ) )
17	13 16	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 2^nd ‘ 𝑋 ) ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) )
18		oveq2	⊢ ( 𝑗 = ( 2^nd ‘ 𝑋 ) → ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) = ( ( 1^st ‘ 𝑋 ) 𝑆 ( 2^nd ‘ 𝑋 ) ) )
19		eqid	⊢ ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) = ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) )
20		ovex	⊢ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ∈ V
21	18 19 20	fvmpt3i	⊢ ( ( 2^nd ‘ 𝑋 ) ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) → ( ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) ‘ ( 2^nd ‘ 𝑋 ) ) = ( ( 1^st ‘ 𝑋 ) 𝑆 ( 2^nd ‘ 𝑋 ) ) )
22	17 21	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) ‘ ( 2^nd ‘ 𝑋 ) ) = ( ( 1^st ‘ 𝑋 ) 𝑆 ( 2^nd ‘ 𝑋 ) ) )
23	9	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ ) )
24	7 22 23	3eqtr4a	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) ‘ ( 2^nd ‘ 𝑋 ) ) = ( 𝑆 ‘ 𝑋 ) )
25		sneq	⊢ ( 𝑖 = ( 1^st ‘ 𝑋 ) → { 𝑖 } = { ( 1^st ‘ 𝑋 ) } )
26	25	imaeq2d	⊢ ( 𝑖 = ( 1^st ‘ 𝑋 ) → ( 𝐴 “ { 𝑖 } ) = ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) )
27		oveq1	⊢ ( 𝑖 = ( 1^st ‘ 𝑋 ) → ( 𝑖 𝑆 𝑗 ) = ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) )
28	26 27	mpteq12dv	⊢ ( 𝑖 = ( 1^st ‘ 𝑋 ) → ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) = ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) )
29	28	breq2d	⊢ ( 𝑖 = ( 1^st ‘ 𝑋 ) → ( 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ↔ 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) ) )
30	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐼 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑖 ∈ 𝐼 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) )
32	3	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → dom 𝐴 ⊆ 𝐼 )
33		1stdm	⊢ ( ( Rel 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 1^st ‘ 𝑋 ) ∈ dom 𝐴 )
34	1 33	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 1^st ‘ 𝑋 ) ∈ dom 𝐴 )
35	32 34	sseldd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 1^st ‘ 𝑋 ) ∈ 𝐼 )
36	29 31 35	rspcdva	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) )
37	20 19	dmmpti	⊢ dom ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) = ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } )
38	37	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → dom ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) = ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) )
39	36 38 17	dprdub	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) ‘ ( 2^nd ‘ 𝑋 ) ) ⊆ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) ) )
40	24 39	eqsstrrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑋 ) ⊆ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑋 ) } ) ↦ ( ( 1^st ‘ 𝑋 ) 𝑆 𝑗 ) ) ) )

Metamath Proof Explorer

Theorem dprd2dlem2

Proof