Metamath Proof Explorer

Theorem dprddisj2

Description: The function S is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016) (Revised by AV, 14-Jul-2019)

Ref Expression
Hypotheses dprdcntz2.1 ⊢ φ → G dom ⁡ DProd S
dprdcntz2.2 ⊢ φ → dom ⁡ S = I
dprdcntz2.c ⊢ φ → C ⊆ I
dprdcntz2.d ⊢ φ → D ⊆ I
dprdcntz2.i ⊢ φ → C ∩ D = ∅
dprddisj2.0 ⊢ 0 ˙ = 0 G
Assertion dprddisj2 ⊢ φ → G DProd S ↾ C ∩ G DProd S ↾ D = 0 ˙

Proof

Step Hyp Ref Expression
1 dprdcntz2.1 ⊢ φ → G dom ⁡ DProd S
2 dprdcntz2.2 ⊢ φ → dom ⁡ S = I
3 dprdcntz2.c ⊢ φ → C ⊆ I
4 dprdcntz2.d ⊢ φ → D ⊆ I
5 dprdcntz2.i ⊢ φ → C ∩ D = ∅
6 dprddisj2.0 ⊢ 0 ˙ = 0 G
7 inss1 ⊢ G DProd S ↾ C ∩ G DProd S ↾ D ⊆ G DProd S ↾ C
8 1 2 3 dprdres ⊢ φ → G dom ⁡ DProd S ↾ C ∧ G DProd S ↾ C ⊆ G DProd S
9 8 simprd ⊢ φ → G DProd S ↾ C ⊆ G DProd S
10 7 9 sstrid ⊢ φ → G DProd S ↾ C ∩ G DProd S ↾ D ⊆ G DProd S
11 10 sseld ⊢ φ → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D → x ∈ G DProd S
12 eqid ⊢ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h = h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
13 6 12 eldprd ⊢ dom ⁡ S = I → x ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h x = ∑ G f
14 2 13 syl ⊢ φ → x ∈ G DProd S ↔ G dom ⁡ DProd S ∧ ∃ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h x = ∑ G f
15 1 ad2antrr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → G dom ⁡ DProd S
16 2 ad2antrr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → dom ⁡ S = I
17 simplr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h
18 eqid ⊢ Base G = Base G
19 12 15 16 17 18 dprdff ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → f : I ⟶ Base G
20 19 feqmptd ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → f = x ∈ I ⟼ f ⁡ x
21 5 difeq2d ⊢ φ → I ∖ C ∩ D = I ∖ ∅
22 difindi ⊢ I ∖ C ∩ D = I ∖ C ∪ I ∖ D
23 dif0 ⊢ I ∖ ∅ = I
24 21 22 23 3eqtr3g ⊢ φ → I ∖ C ∪ I ∖ D = I
25 eqimss2 ⊢ I ∖ C ∪ I ∖ D = I → I ⊆ I ∖ C ∪ I ∖ D
26 24 25 syl ⊢ φ → I ⊆ I ∖ C ∪ I ∖ D
27 26 ad2antrr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → I ⊆ I ∖ C ∪ I ∖ D
28 27 sselda ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D ∧ x ∈ I → x ∈ I ∖ C ∪ I ∖ D
29 elun ⊢ x ∈ I ∖ C ∪ I ∖ D ↔ x ∈ I ∖ C ∨ x ∈ I ∖ D
30 28 29 sylib ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D ∧ x ∈ I → x ∈ I ∖ C ∨ x ∈ I ∖ D
31 3 ad2antrr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → C ⊆ I
32 simprl ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → ∑ G f ∈ G DProd S ↾ C
33 6 12 15 16 31 17 32 dmdprdsplitlem ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D ∧ x ∈ I ∖ C → f ⁡ x = 0 ˙
34 4 ad2antrr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → D ⊆ I
35 simprr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → ∑ G f ∈ G DProd S ↾ D
36 6 12 15 16 34 17 35 dmdprdsplitlem ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D ∧ x ∈ I ∖ D → f ⁡ x = 0 ˙
37 33 36 jaodan ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D ∧ x ∈ I ∖ C ∨ x ∈ I ∖ D → f ⁡ x = 0 ˙
38 30 37 syldan ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D ∧ x ∈ I → f ⁡ x = 0 ˙
39 38 mpteq2dva ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → x ∈ I ⟼ f ⁡ x = x ∈ I ⟼ 0 ˙
40 20 39 eqtrd ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → f = x ∈ I ⟼ 0 ˙
41 40 oveq2d ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → ∑ G f = ∑ G x ∈ I 0 ˙
42 dprdgrp ⊢ G dom ⁡ DProd S → G ∈ Grp
43 grpmnd ⊢ G ∈ Grp → G ∈ Mnd
44 1 42 43 3syl ⊢ φ → G ∈ Mnd
45 1 2 dprddomcld ⊢ φ → I ∈ V
46 6 gsumz ⊢ G ∈ Mnd ∧ I ∈ V → ∑ G x ∈ I 0 ˙ = 0 ˙
47 44 45 46 syl2anc ⊢ φ → ∑ G x ∈ I 0 ˙ = 0 ˙
48 47 ad2antrr ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → ∑ G x ∈ I 0 ˙ = 0 ˙
49 41 48 eqtrd ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h ∧ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → ∑ G f = 0 ˙
50 49 ex ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h → ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → ∑ G f = 0 ˙
51 eleq1 ⊢ x = ∑ G f → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D ↔ ∑ G f ∈ G DProd S ↾ C ∩ G DProd S ↾ D
52 elin ⊢ ∑ G f ∈ G DProd S ↾ C ∩ G DProd S ↾ D ↔ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D
53 51 52 bitrdi ⊢ x = ∑ G f → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D ↔ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D
54 velsn ⊢ x ∈ 0 ˙ ↔ x = 0 ˙
55 eqeq1 ⊢ x = ∑ G f → x = 0 ˙ ↔ ∑ G f = 0 ˙
56 54 55 syl5bb ⊢ x = ∑ G f → x ∈ 0 ˙ ↔ ∑ G f = 0 ˙
57 53 56 imbi12d ⊢ x = ∑ G f → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D → x ∈ 0 ˙ ↔ ∑ G f ∈ G DProd S ↾ C ∧ ∑ G f ∈ G DProd S ↾ D → ∑ G f = 0 ˙
58 50 57 syl5ibrcom ⊢ φ ∧ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h → x = ∑ G f → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D → x ∈ 0 ˙
59 58 rexlimdva ⊢ φ → ∃ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h x = ∑ G f → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D → x ∈ 0 ˙
60 59 adantld ⊢ φ → G dom ⁡ DProd S ∧ ∃ f ∈ h ∈ ⨉ i ∈ I S ⁡ i | finSupp 0 ˙⁡ h x = ∑ G f → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D → x ∈ 0 ˙
61 14 60 sylbid ⊢ φ → x ∈ G DProd S → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D → x ∈ 0 ˙
62 61 com23 ⊢ φ → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D → x ∈ G DProd S → x ∈ 0 ˙
63 11 62 mpdd ⊢ φ → x ∈ G DProd S ↾ C ∩ G DProd S ↾ D → x ∈ 0 ˙
64 63 ssrdv ⊢ φ → G DProd S ↾ C ∩ G DProd S ↾ D ⊆ 0 ˙
65 8 simpld ⊢ φ → G dom ⁡ DProd S ↾ C
66 dprdsubg ⊢ G dom ⁡ DProd S ↾ C → G DProd S ↾ C ∈ SubGrp ⁡ G
67 6 subg0cl ⊢ G DProd S ↾ C ∈ SubGrp ⁡ G → 0 ˙ ∈ G DProd S ↾ C
68 65 66 67 3syl ⊢ φ → 0 ˙ ∈ G DProd S ↾ C
69 1 2 4 dprdres ⊢ φ → G dom ⁡ DProd S ↾ D ∧ G DProd S ↾ D ⊆ G DProd S
70 69 simpld ⊢ φ → G dom ⁡ DProd S ↾ D
71 dprdsubg ⊢ G dom ⁡ DProd S ↾ D → G DProd S ↾ D ∈ SubGrp ⁡ G
72 6 subg0cl ⊢ G DProd S ↾ D ∈ SubGrp ⁡ G → 0 ˙ ∈ G DProd S ↾ D
73 70 71 72 3syl ⊢ φ → 0 ˙ ∈ G DProd S ↾ D
74 68 73 elind ⊢ φ → 0 ˙ ∈ G DProd S ↾ C ∩ G DProd S ↾ D
75 74 snssd ⊢ φ → 0 ˙ ⊆ G DProd S ↾ C ∩ G DProd S ↾ D
76 64 75 eqssd ⊢ φ → G DProd S ↾ C ∩ G DProd S ↾ D = 0 ˙