Metamath Proof Explorer

Theorem subgdisjb

Description: Vectors belonging to disjoint commuting subgroups are uniquely determined by their sum. Analogous to opth , this theorem shows a way of representing a pair of vectors. (Contributed by NM, 5-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 )
Assertion subgdisjb 
|- ( ph -> ( ( A .+ B ) = ( C .+ D ) <-> ( A = C /\ 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 4 adantr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> T e. ( SubGrp ` G ) )
13 5 adantr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> U e. ( SubGrp ` G ) )
14 6 adantr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> ( T i^i U ) = { .0. } )
15 7 adantr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> T C_ ( Z ` U ) )
16 8 adantr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> A e. T )
17 9 adantr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> C e. T )
18 10 adantr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> B e. U )
19 11 adantr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> D e. U )
20 simpr 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> ( A .+ B ) = ( C .+ D ) )
21 1 2 3 12 13 14 15 16 17 18 19 20 subgdisj1 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> A = C )
22 1 2 3 12 13 14 15 16 17 18 19 20 subgdisj2 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> B = D )
23 21 22 jca 
 |-  ( ( ph /\ ( A .+ B ) = ( C .+ D ) ) -> ( A = C /\ B = D ) )
24 23 ex 
 |-  ( ph -> ( ( A .+ B ) = ( C .+ D ) -> ( A = C /\ B = D ) ) )
25 oveq12 
 |-  ( ( A = C /\ B = D ) -> ( A .+ B ) = ( C .+ D ) )
26 24 25 impbid1 
 |-  ( ph -> ( ( A .+ B ) = ( C .+ D ) <-> ( A = C /\ B = D ) ) )