Metamath Proof Explorer

Theorem subgdisj1

Description: Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses subgdisj.p 
|- .+ = ( +g ` G )
subgdisj.o 
|- .0. = ( 0g ` G )
subgdisj.z 
|- Z = ( Cntz ` G )
subgdisj.t 
|- ( ph -> T e. ( SubGrp ` G ) )
subgdisj.u 
|- ( ph -> U e. ( SubGrp ` G ) )
subgdisj.i 
|- ( ph -> ( T i^i U ) = { .0. } )
subgdisj.s 
|- ( ph -> T C_ ( Z ` U ) )
subgdisj.a 
|- ( ph -> A e. T )
subgdisj.c 
|- ( ph -> C e. T )
subgdisj.b 
|- ( ph -> B e. U )
subgdisj.d 
|- ( ph -> D e. U )
subgdisj.j 
|- ( ph -> ( A .+ B ) = ( C .+ D ) )
Assertion subgdisj1 
|- ( ph -> A = C )

Proof

Step Hyp Ref Expression
1 subgdisj.p 
 |-  .+ = ( +g ` G )
2 subgdisj.o 
 |-  .0. = ( 0g ` G )
3 subgdisj.z 
 |-  Z = ( Cntz ` G )
4 subgdisj.t 
 |-  ( ph -> T e. ( SubGrp ` G ) )
5 subgdisj.u 
 |-  ( ph -> U e. ( SubGrp ` G ) )
6 subgdisj.i 
 |-  ( ph -> ( T i^i U ) = { .0. } )
7 subgdisj.s 
 |-  ( ph -> T C_ ( Z ` U ) )
8 subgdisj.a 
 |-  ( ph -> A e. T )
9 subgdisj.c 
 |-  ( ph -> C e. T )
10 subgdisj.b 
 |-  ( ph -> B e. U )
11 subgdisj.d 
 |-  ( ph -> D e. U )
12 subgdisj.j 
 |-  ( ph -> ( A .+ B ) = ( C .+ D ) )
13 eqid 
 |-  ( -g ` G ) = ( -g ` G )
14 13 subgsubcl 
 |-  ( ( T e. ( SubGrp ` G ) /\ A e. T /\ C e. T ) -> ( A ( -g ` G ) C ) e. T )
15 4 8 9 14 syl3anc 
 |-  ( ph -> ( A ( -g ` G ) C ) e. T )
16 7 9 sseldd 
 |-  ( ph -> C e. ( Z ` U ) )
17 1 3 cntzi 
 |-  ( ( C e. ( Z ` U ) /\ B e. U ) -> ( C .+ B ) = ( B .+ C ) )
18 16 10 17 syl2anc 
 |-  ( ph -> ( C .+ B ) = ( B .+ C ) )
19 12 18 oveq12d 
 |-  ( ph -> ( ( A .+ B ) ( -g ` G ) ( C .+ B ) ) = ( ( C .+ D ) ( -g ` G ) ( B .+ C ) ) )
20 subgrcl 
 |-  ( T e. ( SubGrp ` G ) -> G e. Grp )
21 4 20 syl 
 |-  ( ph -> G e. Grp )
22 eqid 
 |-  ( Base ` G ) = ( Base ` G )
23 22 subgss 
 |-  ( T e. ( SubGrp ` G ) -> T C_ ( Base ` G ) )
24 4 23 syl 
 |-  ( ph -> T C_ ( Base ` G ) )
25 24 8 sseldd 
 |-  ( ph -> A e. ( Base ` G ) )
26 22 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( Base ` G ) )
27 5 26 syl 
 |-  ( ph -> U C_ ( Base ` G ) )
28 27 10 sseldd 
 |-  ( ph -> B e. ( Base ` G ) )
29 22 1 grpcl 
 |-  ( ( G e. Grp /\ A e. ( Base ` G ) /\ B e. ( Base ` G ) ) -> ( A .+ B ) e. ( Base ` G ) )
30 21 25 28 29 syl3anc 
 |-  ( ph -> ( A .+ B ) e. ( Base ` G ) )
31 24 9 sseldd 
 |-  ( ph -> C e. ( Base ` G ) )
32 22 1 13 grpsubsub4 
 |-  ( ( G e. Grp /\ ( ( A .+ B ) e. ( Base ` G ) /\ B e. ( Base ` G ) /\ C e. ( Base ` G ) ) ) -> ( ( ( A .+ B ) ( -g ` G ) B ) ( -g ` G ) C ) = ( ( A .+ B ) ( -g ` G ) ( C .+ B ) ) )
33 21 30 28 31 32 syl13anc 
 |-  ( ph -> ( ( ( A .+ B ) ( -g ` G ) B ) ( -g ` G ) C ) = ( ( A .+ B ) ( -g ` G ) ( C .+ B ) ) )
34 12 30 eqeltrrd 
 |-  ( ph -> ( C .+ D ) e. ( Base ` G ) )
35 22 1 13 grpsubsub4 
 |-  ( ( G e. Grp /\ ( ( C .+ D ) e. ( Base ` G ) /\ C e. ( Base ` G ) /\ B e. ( Base ` G ) ) ) -> ( ( ( C .+ D ) ( -g ` G ) C ) ( -g ` G ) B ) = ( ( C .+ D ) ( -g ` G ) ( B .+ C ) ) )
36 21 34 31 28 35 syl13anc 
 |-  ( ph -> ( ( ( C .+ D ) ( -g ` G ) C ) ( -g ` G ) B ) = ( ( C .+ D ) ( -g ` G ) ( B .+ C ) ) )
37 19 33 36 3eqtr4d 
 |-  ( ph -> ( ( ( A .+ B ) ( -g ` G ) B ) ( -g ` G ) C ) = ( ( ( C .+ D ) ( -g ` G ) C ) ( -g ` G ) B ) )
38 22 1 13 grppncan 
 |-  ( ( G e. Grp /\ A e. ( Base ` G ) /\ B e. ( Base ` G ) ) -> ( ( A .+ B ) ( -g ` G ) B ) = A )
39 21 25 28 38 syl3anc 
 |-  ( ph -> ( ( A .+ B ) ( -g ` G ) B ) = A )
40 39 oveq1d 
 |-  ( ph -> ( ( ( A .+ B ) ( -g ` G ) B ) ( -g ` G ) C ) = ( A ( -g ` G ) C ) )
41 1 3 cntzi 
 |-  ( ( C e. ( Z ` U ) /\ D e. U ) -> ( C .+ D ) = ( D .+ C ) )
42 16 11 41 syl2anc 
 |-  ( ph -> ( C .+ D ) = ( D .+ C ) )
43 42 oveq1d 
 |-  ( ph -> ( ( C .+ D ) ( -g ` G ) C ) = ( ( D .+ C ) ( -g ` G ) C ) )
44 27 11 sseldd 
 |-  ( ph -> D e. ( Base ` G ) )
45 22 1 13 grppncan 
 |-  ( ( G e. Grp /\ D e. ( Base ` G ) /\ C e. ( Base ` G ) ) -> ( ( D .+ C ) ( -g ` G ) C ) = D )
46 21 44 31 45 syl3anc 
 |-  ( ph -> ( ( D .+ C ) ( -g ` G ) C ) = D )
47 43 46 eqtrd 
 |-  ( ph -> ( ( C .+ D ) ( -g ` G ) C ) = D )
48 47 oveq1d 
 |-  ( ph -> ( ( ( C .+ D ) ( -g ` G ) C ) ( -g ` G ) B ) = ( D ( -g ` G ) B ) )
49 37 40 48 3eqtr3d 
 |-  ( ph -> ( A ( -g ` G ) C ) = ( D ( -g ` G ) B ) )
50 13 subgsubcl 
 |-  ( ( U e. ( SubGrp ` G ) /\ D e. U /\ B e. U ) -> ( D ( -g ` G ) B ) e. U )
51 5 11 10 50 syl3anc 
 |-  ( ph -> ( D ( -g ` G ) B ) e. U )
52 49 51 eqeltrd 
 |-  ( ph -> ( A ( -g ` G ) C ) e. U )
53 15 52 elind 
 |-  ( ph -> ( A ( -g ` G ) C ) e. ( T i^i U ) )
54 53 6 eleqtrd 
 |-  ( ph -> ( A ( -g ` G ) C ) e. { .0. } )
55 elsni 
 |-  ( ( A ( -g ` G ) C ) e. { .0. } -> ( A ( -g ` G ) C ) = .0. )
56 54 55 syl 
 |-  ( ph -> ( A ( -g ` G ) C ) = .0. )
57 22 2 13 grpsubeq0 
 |-  ( ( G e. Grp /\ A e. ( Base ` G ) /\ C e. ( Base ` G ) ) -> ( ( A ( -g ` G ) C ) = .0. <-> A = C ) )
58 21 25 31 57 syl3anc 
 |-  ( ph -> ( ( A ( -g ` G ) C ) = .0. <-> A = C ) )
59 56 58 mpbid 
 |-  ( ph -> A = C )