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 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
dprdcntz2.2 ⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
dprdcntz2.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐼 )
dprdcntz2.d ⊢ ( 𝜑 → 𝐷 ⊆ 𝐼 )
dprdcntz2.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
dprddisj2.0 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion dprddisj2 ( 𝜑 → ( ( 𝐺 DProd ( 𝑆 ↾ 𝐶 ) ) ∩ ( 𝐺 DProd ( 𝑆 ↾ 𝐷 ) ) ) = { 0 } )

Proof

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