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 ‘ 𝐺 )
subgdisj.o ⊢ 0 = ( 0g ‘ 𝐺 )
subgdisj.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
subgdisj.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
subgdisj.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
subgdisj.i ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
subgdisj.s ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
subgdisj.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
subgdisj.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
subgdisj.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
subgdisj.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
Assertion subgdisjb ( 𝜑 → ( ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 subgdisj.p ⊢ + = ( +g ‘ 𝐺 )
2 subgdisj.o ⊢ 0 = ( 0g ‘ 𝐺 )
3 subgdisj.z ⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4 subgdisj.t ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
5 subgdisj.u ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
6 subgdisj.i ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
7 subgdisj.s ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
8 subgdisj.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
9 subgdisj.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
10 subgdisj.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
11 subgdisj.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
12 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
13 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
14 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → ( 𝑇 ∩ 𝑈 ) = { 0 } )
15 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
16 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝐴 ∈ 𝑇 )
17 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝐶 ∈ 𝑇 )
18 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝐵 ∈ 𝑈 )
19 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝐷 ∈ 𝑈 )
20 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
21 1 2 3 12 13 14 15 16 17 18 19 20 subgdisj1 ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝐴 = 𝐶 )
22 1 2 3 12 13 14 15 16 17 18 19 20 subgdisj2 ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → 𝐵 = 𝐷 )
23 21 22 jca ⊢ ( ( 𝜑 ∧ ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
24 23 ex ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
25 oveq12 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
26 24 25 impbid1 ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )