Theorem dmdprdd

Description: Show that a given family is a direct product decomposition. (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

	Ref	Expression
Hypotheses	dmdprd.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	dmdprd.0	⊢ 0 = ( 0g ‘ 𝐺 )
	dmdprd.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
	dmdprdd.1	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	dmdprdd.2	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	dmdprdd.3	⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
	dmdprdd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) )
	dmdprdd.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } )
Assertion	dmdprdd	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		dmdprd.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
2		dmdprd.0	⊢ 0 = ( 0g ‘ 𝐺 )
3		dmdprd.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
4		dmdprdd.1	⊢ ( 𝜑 → 𝐺 ∈ Grp )
5		dmdprdd.2	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		dmdprdd.3	⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
7		dmdprdd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) )
8		dmdprdd.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ⊆ { 0 } )
9		eldifsn	⊢ ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↔ ( 𝑦 ∈ 𝐼 ∧ 𝑦 ≠ 𝑥 ) )
10		necom	⊢ ( 𝑦 ≠ 𝑥 ↔ 𝑥 ≠ 𝑦 )
11	10	anbi2i	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑦 ≠ 𝑥 ) ↔ ( 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) )
12	9 11	bitri	⊢ ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ↔ ( 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) )
13	7	3exp2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 → ( 𝑦 ∈ 𝐼 → ( 𝑥 ≠ 𝑦 → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) ) ) )
14	13	imp4b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
15	12 14	biimtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
16	15	ralrimiv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) )
17	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) )
18	2	subg0cl	⊢ ( ( 𝑆 ‘ 𝑥 ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝑆 ‘ 𝑥 ) )
19	17 18	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ ( 𝑆 ‘ 𝑥 ) )
20	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐺 ∈ Grp )
21		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
22	21	subgacs	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
23		acsmre	⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
24	20 22 23	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
25		imassrn	⊢ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ran 𝑆
26	6	frnd	⊢ ( 𝜑 → ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ran 𝑆 ⊆ ( SubGrp ‘ 𝐺 ) )
28	25 27	sstrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( SubGrp ‘ 𝐺 ) )
29		mresspw	⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
30	24 29	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
31	28 30	sstrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
32		sspwuni	⊢ ( ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) ↔ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) )
33	31 32	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) )
34	3	mrccl	⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ⊆ ( Base ‘ 𝐺 ) ) → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
35	24 33 34	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
36	2	subg0cl	⊢ ( ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
37	35 36	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
38	19 37	elind	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
39	38	snssd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → { 0 } ⊆ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
40	8 39	eqssd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } )
41	16 40	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) )
42	41	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) )
43	6	fdmd	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
44	1 2 3	dmdprd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼 ) → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
45	5 43 44	syl2anc	⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( 𝐺 ∈ Grp ∧ 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ ( 𝐼 ∖ { 𝑥 } ) ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝑍 ‘ ( 𝑆 ‘ 𝑦 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) ∩ ( 𝐾 ‘ ∪ ( 𝑆 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = { 0 } ) ) ) )
46	4 6 42 45	mpbir3and	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )