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 ⊢φ→Gdom⁡DProdS
dprdcntz2.2 ⊢φ→dom⁡S=I
dprdcntz2.c ⊢φ→C⊆I
dprdcntz2.d ⊢φ→D⊆I
dprdcntz2.i ⊢φ→C∩D=∅
dprddisj2.0 ⊢0˙=0G
Assertion dprddisj2 ⊢φ→GDProdS↾C∩GDProdS↾D=0˙

Proof

Step Hyp Ref Expression
1 dprdcntz2.1 ⊢φ→Gdom⁡DProdS
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˙=0G
7 inss1 ⊢GDProdS↾C∩GDProdS↾D⊆GDProdS↾C
8 1 2 3 dprdres ⊢φ→Gdom⁡DProdS↾C∧GDProdS↾C⊆GDProdS
9 8 simprd ⊢φ→GDProdS↾C⊆GDProdS
10 7 9 sstrid ⊢φ→GDProdS↾C∩GDProdS↾D⊆GDProdS
11 10 sseld ⊢φ→x∈GDProdS↾C∩GDProdS↾D→x∈GDProdS
12 eqid ⊢h∈⨉i∈IS⁡i|finSupp0˙⁡h=h∈⨉i∈IS⁡i|finSupp0˙⁡h
13 6 12 eldprd ⊢dom⁡S=I→x∈GDProdS↔Gdom⁡DProdS∧∃f∈h∈⨉i∈IS⁡i|finSupp0˙⁡hx=∑Gf
14 2 13 syl ⊢φ→x∈GDProdS↔Gdom⁡DProdS∧∃f∈h∈⨉i∈IS⁡i|finSupp0˙⁡hx=∑Gf
15 1 ad2antrr ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→Gdom⁡DProdS
16 2 ad2antrr ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→dom⁡S=I
17 simplr ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h
18 eqid ⊢BaseG=BaseG
19 12 15 16 17 18 dprdff ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→f:I⟶BaseG
20 19 feqmptd ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾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∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→I⊆I∖C∪I∖D
28 27 sselda ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾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∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D∧x∈I→x∈I∖C∨x∈I∖D
31 3 ad2antrr ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→C⊆I
32 simprl ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→∑Gf∈GDProdS↾C
33 6 12 15 16 31 17 32 dmdprdsplitlem ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D∧x∈I∖C→f⁡x=0˙
34 4 ad2antrr ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→D⊆I
35 simprr ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→∑Gf∈GDProdS↾D
36 6 12 15 16 34 17 35 dmdprdsplitlem ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D∧x∈I∖D→f⁡x=0˙
37 33 36 jaodan ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D∧x∈I∖C∨x∈I∖D→f⁡x=0˙
38 30 37 syldan ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D∧x∈I→f⁡x=0˙
39 38 mpteq2dva ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→x∈I⟼f⁡x=x∈I⟼0˙
40 20 39 eqtrd ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→f=x∈I⟼0˙
41 40 oveq2d ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→∑Gf=∑Gx∈I0˙
42 dprdgrp ⊢Gdom⁡DProdS→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→∑Gx∈I0˙=0˙
47 44 45 46 syl2anc ⊢φ→∑Gx∈I0˙=0˙
48 47 ad2antrr ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→∑Gx∈I0˙=0˙
49 41 48 eqtrd ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h∧∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→∑Gf=0˙
50 49 ex ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h→∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→∑Gf=0˙
51 eleq1 ⊢x=∑Gf→x∈GDProdS↾C∩GDProdS↾D↔∑Gf∈GDProdS↾C∩GDProdS↾D
52 elin ⊢∑Gf∈GDProdS↾C∩GDProdS↾D↔∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D
53 51 52 bitrdi ⊢x=∑Gf→x∈GDProdS↾C∩GDProdS↾D↔∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D
54 velsn ⊢x∈0˙↔x=0˙
55 eqeq1 ⊢x=∑Gf→x=0˙↔∑Gf=0˙
56 54 55 bitrid ⊢x=∑Gf→x∈0˙↔∑Gf=0˙
57 53 56 imbi12d ⊢x=∑Gf→x∈GDProdS↾C∩GDProdS↾D→x∈0˙↔∑Gf∈GDProdS↾C∧∑Gf∈GDProdS↾D→∑Gf=0˙
58 50 57 syl5ibrcom ⊢φ∧f∈h∈⨉i∈IS⁡i|finSupp0˙⁡h→x=∑Gf→x∈GDProdS↾C∩GDProdS↾D→x∈0˙
59 58 rexlimdva ⊢φ→∃f∈h∈⨉i∈IS⁡i|finSupp0˙⁡hx=∑Gf→x∈GDProdS↾C∩GDProdS↾D→x∈0˙
60 59 adantld ⊢φ→Gdom⁡DProdS∧∃f∈h∈⨉i∈IS⁡i|finSupp0˙⁡hx=∑Gf→x∈GDProdS↾C∩GDProdS↾D→x∈0˙
61 14 60 sylbid ⊢φ→x∈GDProdS→x∈GDProdS↾C∩GDProdS↾D→x∈0˙
62 61 com23 ⊢φ→x∈GDProdS↾C∩GDProdS↾D→x∈GDProdS→x∈0˙
63 11 62 mpdd ⊢φ→x∈GDProdS↾C∩GDProdS↾D→x∈0˙
64 63 ssrdv ⊢φ→GDProdS↾C∩GDProdS↾D⊆0˙
65 8 simpld ⊢φ→Gdom⁡DProdS↾C
66 dprdsubg ⊢Gdom⁡DProdS↾C→GDProdS↾C∈SubGrp⁡G
67 6 subg0cl ⊢GDProdS↾C∈SubGrp⁡G→0˙∈GDProdS↾C
68 65 66 67 3syl ⊢φ→0˙∈GDProdS↾C
69 1 2 4 dprdres ⊢φ→Gdom⁡DProdS↾D∧GDProdS↾D⊆GDProdS
70 69 simpld ⊢φ→Gdom⁡DProdS↾D
71 dprdsubg ⊢Gdom⁡DProdS↾D→GDProdS↾D∈SubGrp⁡G
72 6 subg0cl ⊢GDProdS↾D∈SubGrp⁡G→0˙∈GDProdS↾D
73 70 71 72 3syl ⊢φ→0˙∈GDProdS↾D
74 68 73 elind ⊢φ→0˙∈GDProdS↾C∩GDProdS↾D
75 74 snssd ⊢φ→0˙⊆GDProdS↾C∩GDProdS↾D
76 64 75 eqssd ⊢φ→GDProdS↾C∩GDProdS↾D=0˙