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

Metamath Proof Explorer

Theorem dprdz

Description: A family consisting entirely of trivial groups is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypothesis dprd0.0 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion dprdz ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( 𝐺 dom DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) = { 0 } ) )

Proof

Step Hyp Ref Expression
1 dprd0.0 ⊢ 0 = ( 0g ‘ 𝐺 )
2 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
3 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
4 simpl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝐺 ∈ Grp )
5 simpr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
6 1 0subg ⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
7 6 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐼 ) → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
8 7 fmpttd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐼 ↦ { 0 } ) : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
9 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10 9 1 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
11 10 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 0 ∈ ( Base ‘ 𝐺 ) )
12 11 snssd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → { 0 } ⊆ ( Base ‘ 𝐺 ) )
13 9 2 cntzsubg ⊢ ( ( 𝐺 ∈ Grp ∧ { 0 } ⊆ ( Base ‘ 𝐺 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ { 0 } ) ∈ ( SubGrp ‘ 𝐺 ) )
14 12 13 syldan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( ( Cntz ‘ 𝐺 ) ‘ { 0 } ) ∈ ( SubGrp ‘ 𝐺 ) )
15 1 subg0cl ⊢ ( ( ( Cntz ‘ 𝐺 ) ‘ { 0 } ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( ( Cntz ‘ 𝐺 ) ‘ { 0 } ) )
16 14 15 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 0 ∈ ( ( Cntz ‘ 𝐺 ) ‘ { 0 } ) )
17 16 snssd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → { 0 } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { 0 } ) )
18 17 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧 ) ) → { 0 } ⊆ ( ( Cntz ‘ 𝐺 ) ‘ { 0 } ) )
19 simpr1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑦 ∈ 𝐼 )
20 eqidd ⊢ ( 𝑥 = 𝑦 → { 0 } = { 0 } )
21 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ { 0 } ) = ( 𝑥 ∈ 𝐼 ↦ { 0 } )
22 snex ⊢ { 0 } ∈ V
23 20 21 22 fvmpt3i ⊢ ( 𝑦 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) = { 0 } )
24 19 23 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) = { 0 } )
25 simpr2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑧 ∈ 𝐼 )
26 eqidd ⊢ ( 𝑥 = 𝑧 → { 0 } = { 0 } )
27 26 21 22 fvmpt3i ⊢ ( 𝑧 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑧 ) = { 0 } )
28 25 27 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑧 ) = { 0 } )
29 28 fveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧 ) ) → ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑧 ) ) = ( ( Cntz ‘ 𝐺 ) ‘ { 0 } ) )
30 18 24 29 3sstr4d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ∧ 𝑦 ≠ 𝑧 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑧 ) ) )
31 23 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) = { 0 } )
32 31 ineq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ) = ( { 0 } ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ) )
33 9 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
34 33 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
35 34 acsmred ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
36 imassrn ⊢ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ⊆ ran ( 𝑥 ∈ 𝐼 ↦ { 0 } )
37 8 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ↦ { 0 } ) : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
38 37 frnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ran ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ⊆ ( SubGrp ‘ 𝐺 ) )
39 mresspw ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
40 35 39 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( SubGrp ‘ 𝐺 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
41 38 40 sstrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ran ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
42 36 41 sstrid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
43 sspwuni ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) ↔ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ⊆ ( Base ‘ 𝐺 ) )
44 42 43 sylib ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ⊆ ( Base ‘ 𝐺 ) )
45 3 mrccl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ⊆ ( Base ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
46 35 44 45 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
47 1 subg0cl ⊢ ( ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) )
48 46 47 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → 0 ∈ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) )
49 48 snssd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → { 0 } ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) )
50 dfss2 ⊢ ( { 0 } ⊆ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ↔ ( { 0 } ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ) = { 0 } )
51 49 50 sylib ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( { 0 } ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ) = { 0 } )
52 32 51 eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ) = { 0 } )
53 eqimss ⊢ ( ( ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ) = { 0 } → ( ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ) ⊆ { 0 } )
54 52 53 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) “ ( 𝐼 ∖ { 𝑦 } ) ) ) ) ⊆ { 0 } )
55 2 1 3 4 5 8 30 54 dmdprdd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 𝐺 dom DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) )
56 21 7 dmmptd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → dom ( 𝑥 ∈ 𝐼 ↦ { 0 } ) = 𝐼 )
57 6 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
58 eqimss ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) = { 0 } → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) ⊆ { 0 } )
59 31 58 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ‘ 𝑦 ) ⊆ { 0 } )
60 55 56 57 59 dprdlub ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) ⊆ { 0 } )
61 dprdsubg ⊢ ( 𝐺 dom DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) → ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
62 1 subg0cl ⊢ ( ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) )
63 55 61 62 3syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → 0 ∈ ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) )
64 63 snssd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → { 0 } ⊆ ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) )
65 60 64 eqssd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) = { 0 } )
66 55 65 jca ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉 ) → ( 𝐺 dom DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ∧ ( 𝐺 DProd ( 𝑥 ∈ 𝐼 ↦ { 0 } ) ) = { 0 } ) )