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 
|- ( ph -> G dom DProd S )
dprdcntz2.2 
|- ( ph -> dom S = I )
dprdcntz2.c 
|- ( ph -> C C_ I )
dprdcntz2.d 
|- ( ph -> D C_ I )
dprdcntz2.i 
|- ( ph -> ( C i^i D ) = (/) )
dprddisj2.0 
|- .0. = ( 0g ` G )
Assertion dprddisj2 
|- ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )

Proof

Step Hyp Ref Expression
1 dprdcntz2.1 
 |-  ( ph -> G dom DProd S )
2 dprdcntz2.2 
 |-  ( ph -> dom S = I )
3 dprdcntz2.c 
 |-  ( ph -> C C_ I )
4 dprdcntz2.d 
 |-  ( ph -> D C_ I )
5 dprdcntz2.i 
 |-  ( ph -> ( C i^i D ) = (/) )
6 dprddisj2.0 
 |-  .0. = ( 0g ` G )
7 inss1 
 |-  ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) C_ ( G DProd ( S |` C ) )
8 1 2 3 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` C ) /\ ( G DProd ( S |` C ) ) C_ ( G DProd S ) ) )
9 8 simprd 
 |-  ( ph -> ( G DProd ( S |` C ) ) C_ ( G DProd S ) )
10 7 9 sstrid 
 |-  ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) C_ ( G DProd S ) )
11 10 sseld 
 |-  ( ph -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) -> x e. ( G DProd S ) ) )
12 eqid 
 |-  { h e. X_ i e. I ( S ` i ) | h finSupp .0. } = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
13 6 12 eldprd 
 |-  ( dom S = I -> ( x e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } x = ( G gsum f ) ) ) )
14 2 13 syl 
 |-  ( ph -> ( x e. ( G DProd S ) <-> ( G dom DProd S /\ E. f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } x = ( G gsum f ) ) ) )
15 1 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> G dom DProd S )
16 2 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> dom S = I )
17 simplr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } )
18 eqid 
 |-  ( Base ` G ) = ( Base ` G )
19 12 15 16 17 18 dprdff 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> f : I --> ( Base ` G ) )
20 19 feqmptd 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> f = ( x e. I |-> ( f ` x ) ) )
21 5 difeq2d 
 |-  ( ph -> ( I \ ( C i^i D ) ) = ( I \ (/) ) )
22 difindi 
 |-  ( I \ ( C i^i D ) ) = ( ( I \ C ) u. ( I \ D ) )
23 dif0 
 |-  ( I \ (/) ) = I
24 21 22 23 3eqtr3g 
 |-  ( ph -> ( ( I \ C ) u. ( I \ D ) ) = I )
25 eqimss2 
 |-  ( ( ( I \ C ) u. ( I \ D ) ) = I -> I C_ ( ( I \ C ) u. ( I \ D ) ) )
26 24 25 syl 
 |-  ( ph -> I C_ ( ( I \ C ) u. ( I \ D ) ) )
27 26 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> I C_ ( ( I \ C ) u. ( I \ D ) ) )
28 27 sselda 
 |-  ( ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) /\ x e. I ) -> x e. ( ( I \ C ) u. ( I \ D ) ) )
29 elun 
 |-  ( x e. ( ( I \ C ) u. ( I \ D ) ) <-> ( x e. ( I \ C ) \/ x e. ( I \ D ) ) )
30 28 29 sylib 
 |-  ( ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) /\ x e. I ) -> ( x e. ( I \ C ) \/ x e. ( I \ D ) ) )
31 3 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> C C_ I )
32 simprl 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> ( G gsum f ) e. ( G DProd ( S |` C ) ) )
33 6 12 15 16 31 17 32 dmdprdsplitlem 
 |-  ( ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) /\ x e. ( I \ C ) ) -> ( f ` x ) = .0. )
34 4 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> D C_ I )
35 simprr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> ( G gsum f ) e. ( G DProd ( S |` D ) ) )
36 6 12 15 16 34 17 35 dmdprdsplitlem 
 |-  ( ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) /\ x e. ( I \ D ) ) -> ( f ` x ) = .0. )
37 33 36 jaodan 
 |-  ( ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) /\ ( x e. ( I \ C ) \/ x e. ( I \ D ) ) ) -> ( f ` x ) = .0. )
38 30 37 syldan 
 |-  ( ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) /\ x e. I ) -> ( f ` x ) = .0. )
39 38 mpteq2dva 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> ( x e. I |-> ( f ` x ) ) = ( x e. I |-> .0. ) )
40 20 39 eqtrd 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> f = ( x e. I |-> .0. ) )
41 40 oveq2d 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> ( G gsum f ) = ( G gsum ( x e. I |-> .0. ) ) )
42 dprdgrp 
 |-  ( G dom DProd S -> G e. Grp )
43 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
44 1 42 43 3syl 
 |-  ( ph -> G e. Mnd )
45 1 2 dprddomcld 
 |-  ( ph -> I e. _V )
46 6 gsumz 
 |-  ( ( G e. Mnd /\ I e. _V ) -> ( G gsum ( x e. I |-> .0. ) ) = .0. )
47 44 45 46 syl2anc 
 |-  ( ph -> ( G gsum ( x e. I |-> .0. ) ) = .0. )
48 47 ad2antrr 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> ( G gsum ( x e. I |-> .0. ) ) = .0. )
49 41 48 eqtrd 
 |-  ( ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) /\ ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) -> ( G gsum f ) = .0. )
50 49 ex 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) -> ( ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) -> ( G gsum f ) = .0. ) )
51 eleq1 
 |-  ( x = ( G gsum f ) -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) <-> ( G gsum f ) e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) ) )
52 elin 
 |-  ( ( G gsum f ) e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) <-> ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) )
53 51 52 bitrdi 
 |-  ( x = ( G gsum f ) -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) <-> ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) ) )
54 velsn 
 |-  ( x e. { .0. } <-> x = .0. )
55 eqeq1 
 |-  ( x = ( G gsum f ) -> ( x = .0. <-> ( G gsum f ) = .0. ) )
56 54 55 syl5bb 
 |-  ( x = ( G gsum f ) -> ( x e. { .0. } <-> ( G gsum f ) = .0. ) )
57 53 56 imbi12d 
 |-  ( x = ( G gsum f ) -> ( ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) -> x e. { .0. } ) <-> ( ( ( G gsum f ) e. ( G DProd ( S |` C ) ) /\ ( G gsum f ) e. ( G DProd ( S |` D ) ) ) -> ( G gsum f ) = .0. ) ) )
58 50 57 syl5ibrcom 
 |-  ( ( ph /\ f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } ) -> ( x = ( G gsum f ) -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) -> x e. { .0. } ) ) )
59 58 rexlimdva 
 |-  ( ph -> ( E. f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } x = ( G gsum f ) -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) -> x e. { .0. } ) ) )
60 59 adantld 
 |-  ( ph -> ( ( G dom DProd S /\ E. f e. { h e. X_ i e. I ( S ` i ) | h finSupp .0. } x = ( G gsum f ) ) -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) -> x e. { .0. } ) ) )
61 14 60 sylbid 
 |-  ( ph -> ( x e. ( G DProd S ) -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) -> x e. { .0. } ) ) )
62 61 com23 
 |-  ( ph -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) -> ( x e. ( G DProd S ) -> x e. { .0. } ) ) )
63 11 62 mpdd 
 |-  ( ph -> ( x e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) -> x e. { .0. } ) )
64 63 ssrdv 
 |-  ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) C_ { .0. } )
65 8 simpld 
 |-  ( ph -> G dom DProd ( S |` C ) )
66 dprdsubg 
 |-  ( G dom DProd ( S |` C ) -> ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) )
67 6 subg0cl 
 |-  ( ( G DProd ( S |` C ) ) e. ( SubGrp ` G ) -> .0. e. ( G DProd ( S |` C ) ) )
68 65 66 67 3syl 
 |-  ( ph -> .0. e. ( G DProd ( S |` C ) ) )
69 1 2 4 dprdres 
 |-  ( ph -> ( G dom DProd ( S |` D ) /\ ( G DProd ( S |` D ) ) C_ ( G DProd S ) ) )
70 69 simpld 
 |-  ( ph -> G dom DProd ( S |` D ) )
71 dprdsubg 
 |-  ( G dom DProd ( S |` D ) -> ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) )
72 6 subg0cl 
 |-  ( ( G DProd ( S |` D ) ) e. ( SubGrp ` G ) -> .0. e. ( G DProd ( S |` D ) ) )
73 70 71 72 3syl 
 |-  ( ph -> .0. e. ( G DProd ( S |` D ) ) )
74 68 73 elind 
 |-  ( ph -> .0. e. ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) )
75 74 snssd 
 |-  ( ph -> { .0. } C_ ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) )
76 64 75 eqssd 
 |-  ( ph -> ( ( G DProd ( S |` C ) ) i^i ( G DProd ( S |` D ) ) ) = { .0. } )