dprd2dlem1

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 ‘ 𝐺 ) )
	dprd2d.6	⊢ ( 𝜑 → 𝐶 ⊆ 𝐼 )
Assertion	dprd2dlem1	⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) = ( 𝐺 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		dprd2d.6	⊢ ( 𝜑 → 𝐶 ⊆ 𝐼 )
8		dprdgrp	⊢ ( 𝐺 dom DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) → 𝐺 ∈ Grp )
9	5 8	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
10		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
11	10	subgacs	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
12		acsmre	⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
13	9 11 12	3syl	⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
14		ffun	⊢ ( 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) → Fun 𝑆 )
15		funiunfv	⊢ ( Fun 𝑆 → ∪ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ( 𝑆 ‘ 𝑥 ) = ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) )
16	2 14 15	3syl	⊢ ( 𝜑 → ∪ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ( 𝑆 ‘ 𝑥 ) = ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) )
17		resss	⊢ ( 𝐴 ↾ 𝐶 ) ⊆ 𝐴
18	17	sseli	⊢ ( 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) → 𝑥 ∈ 𝐴 )
19	1 2 3 4 5 6	dprd2dlem2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) )
20	18 19	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) )
21		1st2nd	⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
22	1 18 21	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ) → 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) )
24	22 23	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ) → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( 𝐴 ↾ 𝐶 ) )
25		fvex	⊢ ( 2^nd ‘ 𝑥 ) ∈ V
26	25	opelresi	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( 𝐴 ↾ 𝐶 ) ↔ ( ( 1^st ‘ 𝑥 ) ∈ 𝐶 ∧ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ 𝐴 ) )
27	26	simplbi	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( 𝐴 ↾ 𝐶 ) → ( 1^st ‘ 𝑥 ) ∈ 𝐶 )
28	24 27	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ) → ( 1^st ‘ 𝑥 ) ∈ 𝐶 )
29		ovex	⊢ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) ∈ V
30		eqid	⊢ ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) = ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) )
31		sneq	⊢ ( 𝑖 = ( 1^st ‘ 𝑥 ) → { 𝑖 } = { ( 1^st ‘ 𝑥 ) } )
32	31	imaeq2d	⊢ ( 𝑖 = ( 1^st ‘ 𝑥 ) → ( 𝐴 “ { 𝑖 } ) = ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) )
33		oveq1	⊢ ( 𝑖 = ( 1^st ‘ 𝑥 ) → ( 𝑖 𝑆 𝑗 ) = ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) )
34	32 33	mpteq12dv	⊢ ( 𝑖 = ( 1^st ‘ 𝑥 ) → ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) = ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) )
35	34	oveq2d	⊢ ( 𝑖 = ( 1^st ‘ 𝑥 ) → ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) = ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) )
36	30 35	elrnmpt1s	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ 𝐶 ∧ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) ∈ V ) → ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) ∈ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
37	28 29 36	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ) → ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) ∈ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
38		elssuni	⊢ ( ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) ∈ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) → ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) ⊆ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
39	37 38	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ) → ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { ( 1^st ‘ 𝑥 ) } ) ↦ ( ( 1^st ‘ 𝑥 ) 𝑆 𝑗 ) ) ) ⊆ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
40	20 39	sstrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
41	40	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ( 𝑆 ‘ 𝑥 ) ⊆ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
42		iunss	⊢ ( ∪ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ( 𝑆 ‘ 𝑥 ) ⊆ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ↔ ∀ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ( 𝑆 ‘ 𝑥 ) ⊆ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
43	41 42	sylibr	⊢ ( 𝜑 → ∪ 𝑥 ∈ ( 𝐴 ↾ 𝐶 ) ( 𝑆 ‘ 𝑥 ) ⊆ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
44	16 43	eqsstrrd	⊢ ( 𝜑 → ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
45	7	sselda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) → 𝑖 ∈ 𝐼 )
46	45 4	syldan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) → 𝐺 dom DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) )
47		ovex	⊢ ( 𝑖 𝑆 𝑗 ) ∈ V
48		eqid	⊢ ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) = ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) )
49	47 48	dmmpti	⊢ dom ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) = ( 𝐴 “ { 𝑖 } )
50	49	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) → dom ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) = ( 𝐴 “ { 𝑖 } ) )
51		imassrn	⊢ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ ran 𝑆
52	2	frnd	⊢ ( 𝜑 → ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
53		mresspw	⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
54	13 53	syl	⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
55	52 54	sstrd	⊢ ( 𝜑 → ran 𝑆 ⊆ 𝒫 ( Base ‘ 𝐺 ) )
56	51 55	sstrid	⊢ ( 𝜑 → ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
57		sspwuni	⊢ ( ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) ↔ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ ( Base ‘ 𝐺 ) )
58	56 57	sylib	⊢ ( 𝜑 → ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ ( Base ‘ 𝐺 ) )
59	6	mrccl	⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ ( Base ‘ 𝐺 ) ) → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
60	13 58 59	syl2anc	⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
61	60	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
62		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑖 𝑆 𝑗 ) = ( 𝑖 𝑆 𝑘 ) )
63	62 48 47	fvmpt3i	⊢ ( 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) → ( ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ‘ 𝑘 ) = ( 𝑖 𝑆 𝑘 ) )
64	63	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ( ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ‘ 𝑘 ) = ( 𝑖 𝑆 𝑘 ) )
65		df-ov	⊢ ( 𝑖 𝑆 𝑘 ) = ( 𝑆 ‘ ⟨ 𝑖 , 𝑘 ⟩ )
66	2	ffnd	⊢ ( 𝜑 → 𝑆 Fn 𝐴 )
67	66	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → 𝑆 Fn 𝐴 )
68	17	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ( 𝐴 ↾ 𝐶 ) ⊆ 𝐴 )
69		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → 𝑖 ∈ 𝐶 )
70		elrelimasn	⊢ ( Rel 𝐴 → ( 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ↔ 𝑖 𝐴 𝑘 ) )
71	1 70	syl	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ↔ 𝑖 𝐴 𝑘 ) )
72	71	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) → ( 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ↔ 𝑖 𝐴 𝑘 ) )
73	72	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → 𝑖 𝐴 𝑘 )
74		df-br	⊢ ( 𝑖 𝐴 𝑘 ↔ ⟨ 𝑖 , 𝑘 ⟩ ∈ 𝐴 )
75	73 74	sylib	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ⟨ 𝑖 , 𝑘 ⟩ ∈ 𝐴 )
76		vex	⊢ 𝑘 ∈ V
77	76	opelresi	⊢ ( ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝐴 ↾ 𝐶 ) ↔ ( 𝑖 ∈ 𝐶 ∧ ⟨ 𝑖 , 𝑘 ⟩ ∈ 𝐴 ) )
78	69 75 77	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝐴 ↾ 𝐶 ) )
79		fnfvima	⊢ ( ( 𝑆 Fn 𝐴 ∧ ( 𝐴 ↾ 𝐶 ) ⊆ 𝐴 ∧ ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝐴 ↾ 𝐶 ) ) → ( 𝑆 ‘ ⟨ 𝑖 , 𝑘 ⟩ ) ∈ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) )
80	67 68 78 79	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ( 𝑆 ‘ ⟨ 𝑖 , 𝑘 ⟩ ) ∈ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) )
81	65 80	eqeltrid	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ( 𝑖 𝑆 𝑘 ) ∈ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) )
82		elssuni	⊢ ( ( 𝑖 𝑆 𝑘 ) ∈ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) → ( 𝑖 𝑆 𝑘 ) ⊆ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) )
83	81 82	syl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ( 𝑖 𝑆 𝑘 ) ⊆ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) )
84	13 6 58	mrcssidd	⊢ ( 𝜑 → ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
85	84	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
86	83 85	sstrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ( 𝑖 𝑆 𝑘 ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
87	64 86	eqsstrd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) ∧ 𝑘 ∈ ( 𝐴 “ { 𝑖 } ) ) → ( ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ‘ 𝑘 ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
88	46 50 61 87	dprdlub	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) → ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
89		ovex	⊢ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ∈ V
90	89	elpw	⊢ ( ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ∈ 𝒫 ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ↔ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
91	88 90	sylibr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐶 ) → ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ∈ 𝒫 ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
92	91	fmpttd	⊢ ( 𝜑 → ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) : 𝐶 ⟶ 𝒫 ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
93	92	frnd	⊢ ( 𝜑 → ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ⊆ 𝒫 ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
94		sspwuni	⊢ ( ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ⊆ 𝒫 ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ↔ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
95	93 94	sylib	⊢ ( 𝜑 → ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
96	13 6	mrcssvd	⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ⊆ ( Base ‘ 𝐺 ) )
97	95 96	sstrd	⊢ ( 𝜑 → ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ⊆ ( Base ‘ 𝐺 ) )
98	13 6 44 97	mrcssd	⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ⊆ ( 𝐾 ‘ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )
99	6	mrcsscl	⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ∧ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐾 ‘ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
100	13 95 60 99	syl3anc	⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) ⊆ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) )
101	98 100	eqssd	⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) = ( 𝐾 ‘ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )
102		eqid	⊢ ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) )
103	89 102	dmmpti	⊢ dom ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) = 𝐼
104	103	a1i	⊢ ( 𝜑 → dom ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) = 𝐼 )
105	5 104 7	dprdres	⊢ ( 𝜑 → ( 𝐺 dom DProd ( ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ↾ 𝐶 ) ∧ ( 𝐺 DProd ( ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ↾ 𝐶 ) ) ⊆ ( 𝐺 DProd ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) ) )
106	105	simpld	⊢ ( 𝜑 → 𝐺 dom DProd ( ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ↾ 𝐶 ) )
107	7	resmptd	⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝐼 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ↾ 𝐶 ) = ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
108	106 107	breqtrd	⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) )
109	6	dprdspan	⊢ ( 𝐺 dom DProd ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) → ( 𝐺 DProd ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) = ( 𝐾 ‘ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )
110	108 109	syl	⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) = ( 𝐾 ‘ ∪ ran ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )
111	101 110	eqtr4d	⊢ ( 𝜑 → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐴 ↾ 𝐶 ) ) ) = ( 𝐺 DProd ( 𝑖 ∈ 𝐶 ↦ ( 𝐺 DProd ( 𝑗 ∈ ( 𝐴 “ { 𝑖 } ) ↦ ( 𝑖 𝑆 𝑗 ) ) ) ) ) )

Metamath Proof Explorer

Theorem dprd2dlem1

Proof