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

Metamath Proof Explorer

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 𝑆 )