This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subgdisj2

Description: Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. (Contributed by NM, 12-Jul-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 subgdisj2 
|- ( ph -> B = D )

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 incom 
 |-  ( T i^i U ) = ( U i^i T )
14 13 6 eqtr3id 
 |-  ( ph -> ( U i^i T ) = { .0. } )
15 3 4 5 7 cntzrecd 
 |-  ( ph -> U C_ ( Z ` T ) )
16 7 8 sseldd 
 |-  ( ph -> A e. ( Z ` U ) )
17 1 3 cntzi 
 |-  ( ( A e. ( Z ` U ) /\ B e. U ) -> ( A .+ B ) = ( B .+ A ) )
18 16 10 17 syl2anc 
 |-  ( ph -> ( A .+ B ) = ( B .+ A ) )
19 7 9 sseldd 
 |-  ( ph -> C e. ( Z ` U ) )
20 1 3 cntzi 
 |-  ( ( C e. ( Z ` U ) /\ D e. U ) -> ( C .+ D ) = ( D .+ C ) )
21 19 11 20 syl2anc 
 |-  ( ph -> ( C .+ D ) = ( D .+ C ) )
22 12 18 21 3eqtr3d 
 |-  ( ph -> ( B .+ A ) = ( D .+ C ) )
23 1 2 3 5 4 14 15 10 11 8 9 22 subgdisj1 
 |-  ( ph -> B = D )