Metamath Proof Explorer

Theorem dprdsplit

Description: The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses dprdsplit.2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
dprdsplit.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
dprdsplit.u ⊢ ( 𝜑 → 𝐼 = ( 𝐶 ∪ 𝐷 ) )
dprdsplit.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
dprdsplit.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
Assertion dprdsplit ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 dprdsplit.2 ⊢ ( 𝜑 → 𝑆 : 𝐼 ⟶ ( SubGrp ‘ 𝐺 ) )
2 dprdsplit.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
3 dprdsplit.u ⊢ ( 𝜑 → 𝐼 = ( 𝐶 ∪ 𝐷 ) )
4 dprdsplit.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
5 dprdsplit.1 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
6 1 fdmd ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
7 ssun1 ⊢ 𝐶 ⊆ ( 𝐶 ∪ 𝐷 )
8 7 3 sseqtrrid ⊢ ( 𝜑 → 𝐶 ⊆ 𝐼 )
9 5 6 8 dprdres ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
10 9 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) )
11 dprdsubg ⊢ ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
12 10 11 syl ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
13 ssun2 ⊢ 𝐷 ⊆ ( 𝐶 ∪ 𝐷 )
14 13 3 sseqtrrid ⊢ ( 𝜑 → 𝐷 ⊆ 𝐼 )
15 5 6 14 dprdres ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
16 15 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) )
17 dprdsubg ⊢ ( 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
18 16 17 syl ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
19 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
20 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
21 1 2 3 19 20 dmdprdsplit ⊢ ( 𝜑 → ( 𝐺 dom DProd 𝑆 ↔ ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { ( 0g ‘ 𝐺 ) } ) ) )
22 5 21 mpbid ⊢ ( 𝜑 → ( ( 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) ∧ 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∧ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { ( 0g ‘ 𝐺 ) } ) )
23 22 simp2d ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
24 4 19 lsmsubg ⊢ ( ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ) → ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
25 12 18 23 24 syl3anc ⊢ ( 𝜑 → ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
26 3 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↔ 𝑥 ∈ ( 𝐶 ∪ 𝐷 ) ) )
27 elun ⊢ ( 𝑥 ∈ ( 𝐶 ∪ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) )
28 26 27 bitrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) ) )
29 28 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) )
30 fvres ⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝑆 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝑆 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
32 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐺 dom DProd ( 𝑆 ↾ 𝐶 ) )
33 1 8 fssresd ⊢ ( 𝜑 → ( 𝑆 ↾ 𝐶 ) : 𝐶 ⟶ ( SubGrp ‘ 𝐺 ) )
34 33 fdmd ⊢ ( 𝜑 → dom ( 𝑆 ↾ 𝐶 ) = 𝐶 )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → dom ( 𝑆 ↾ 𝐶 ) = 𝐶 )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
37 32 35 36 dprdub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝑆 ↾ 𝐶 ) ‘ 𝑥 ) ⊆ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) )
38 31 37 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) )
39 4 lsmub1 ⊢ ( ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
40 12 18 39 syl2anc ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
42 38 41 sstrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
43 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( 𝑆 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑆 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
45 16 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐺 dom DProd ( 𝑆 ↾ 𝐷 ) )
46 1 14 fssresd ⊢ ( 𝜑 → ( 𝑆 ↾ 𝐷 ) : 𝐷 ⟶ ( SubGrp ‘ 𝐺 ) )
47 46 fdmd ⊢ ( 𝜑 → dom ( 𝑆 ↾ 𝐷 ) = 𝐷 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → dom ( 𝑆 ↾ 𝐷 ) = 𝐷 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
50 45 48 49 dprdub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑆 ↾ 𝐷 ) ‘ 𝑥 ) ⊆ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) )
51 44 50 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) )
52 4 lsmub2 ⊢ ( ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
53 12 18 52 syl2anc ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
55 51 54 sstrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
56 42 55 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐷 ) ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
57 29 56 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ‘ 𝑥 ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
58 5 6 25 57 dprdlub ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) ⊆ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )
59 9 simprd ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝐺 DProd 𝑆 ) )
60 15 simprd ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( 𝐺 DProd 𝑆 ) )
61 dprdsubg ⊢ ( 𝐺 dom DProd 𝑆 → ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
62 5 61 syl ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) )
63 4 lsmlub ⊢ ( ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 DProd 𝑆 ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) ↔ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
64 12 18 62 63 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ∧ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) ↔ ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ⊆ ( 𝐺 DProd 𝑆 ) ) )
65 59 60 64 mpbi2and ⊢ ( 𝜑 → ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) ⊆ ( 𝐺 DProd 𝑆 ) )
66 58 65 eqssd ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ⊕ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) )