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

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 ‘ 𝐺 )
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 ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
subgdisj.j ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
Assertion subgdisj1 ( 𝜑 → 𝐴 = 𝐶 )

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 subgdisj.j ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐶 + 𝐷 ) )
13 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
14 13 subgsubcl ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑇 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) ∈ 𝑇 )
15 4 8 9 14 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) ∈ 𝑇 )
16 7 9 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑍 ‘ 𝑈 ) )
17 1 3 cntzi ⊢ ( ( 𝐶 ∈ ( 𝑍 ‘ 𝑈 ) ∧ 𝐵 ∈ 𝑈 ) → ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 ) )
18 16 10 17 syl2anc ⊢ ( 𝜑 → ( 𝐶 + 𝐵 ) = ( 𝐵 + 𝐶 ) )
19 12 18 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) ( 𝐶 + 𝐵 ) ) = ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) ( 𝐵 + 𝐶 ) ) )
20 subgrcl ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
21 4 20 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
22 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
23 22 subgss ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
24 4 23 syl ⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝐺 ) )
25 24 8 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐺 ) )
26 22 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
27 5 26 syl ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ 𝐺 ) )
28 27 10 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ 𝐺 ) )
29 22 1 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ ( Base ‘ 𝐺 ) ∧ 𝐵 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐴 + 𝐵 ) ∈ ( Base ‘ 𝐺 ) )
30 21 25 28 29 syl3anc ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ( Base ‘ 𝐺 ) )
31 24 9 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐺 ) )
32 22 1 13 grpsubsub4 ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝐴 + 𝐵 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝐵 ∈ ( Base ‘ 𝐺 ) ∧ 𝐶 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) 𝐵 ) ( -g ‘ 𝐺 ) 𝐶 ) = ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) ( 𝐶 + 𝐵 ) ) )
33 21 30 28 31 32 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) 𝐵 ) ( -g ‘ 𝐺 ) 𝐶 ) = ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) ( 𝐶 + 𝐵 ) ) )
34 12 30 eqeltrrd ⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) ∈ ( Base ‘ 𝐺 ) )
35 22 1 13 grpsubsub4 ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝐶 + 𝐷 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝐶 ∈ ( Base ‘ 𝐺 ) ∧ 𝐵 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) = ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) ( 𝐵 + 𝐶 ) ) )
36 21 34 31 28 35 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) = ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) ( 𝐵 + 𝐶 ) ) )
37 19 33 36 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) 𝐵 ) ( -g ‘ 𝐺 ) 𝐶 ) = ( ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) )
38 22 1 13 grppncan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ ( Base ‘ 𝐺 ) ∧ 𝐵 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) 𝐵 ) = 𝐴 )
39 21 25 28 38 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) 𝐵 ) = 𝐴 )
40 39 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ( -g ‘ 𝐺 ) 𝐵 ) ( -g ‘ 𝐺 ) 𝐶 ) = ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) )
41 1 3 cntzi ⊢ ( ( 𝐶 ∈ ( 𝑍 ‘ 𝑈 ) ∧ 𝐷 ∈ 𝑈 ) → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) )
42 16 11 41 syl2anc ⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) )
43 42 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) 𝐶 ) = ( ( 𝐷 + 𝐶 ) ( -g ‘ 𝐺 ) 𝐶 ) )
44 27 11 sseldd ⊢ ( 𝜑 → 𝐷 ∈ ( Base ‘ 𝐺 ) )
45 22 1 13 grppncan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐷 ∈ ( Base ‘ 𝐺 ) ∧ 𝐶 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐷 + 𝐶 ) ( -g ‘ 𝐺 ) 𝐶 ) = 𝐷 )
46 21 44 31 45 syl3anc ⊢ ( 𝜑 → ( ( 𝐷 + 𝐶 ) ( -g ‘ 𝐺 ) 𝐶 ) = 𝐷 )
47 43 46 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) 𝐶 ) = 𝐷 )
48 47 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐶 + 𝐷 ) ( -g ‘ 𝐺 ) 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( -g ‘ 𝐺 ) 𝐵 ) )
49 37 40 48 3eqtr3d ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) = ( 𝐷 ( -g ‘ 𝐺 ) 𝐵 ) )
50 13 subgsubcl ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐷 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐷 ( -g ‘ 𝐺 ) 𝐵 ) ∈ 𝑈 )
51 5 11 10 50 syl3anc ⊢ ( 𝜑 → ( 𝐷 ( -g ‘ 𝐺 ) 𝐵 ) ∈ 𝑈 )
52 49 51 eqeltrd ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) ∈ 𝑈 )
53 15 52 elind ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) ∈ ( 𝑇 ∩ 𝑈 ) )
54 53 6 eleqtrd ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) ∈ { 0 } )
55 elsni ⊢ ( ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) ∈ { 0 } → ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) = 0 )
56 54 55 syl ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) = 0 )
57 22 2 13 grpsubeq0 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ ( Base ‘ 𝐺 ) ∧ 𝐶 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) = 0 ↔ 𝐴 = 𝐶 ) )
58 21 25 31 57 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 ( -g ‘ 𝐺 ) 𝐶 ) = 0 ↔ 𝐴 = 𝐶 ) )
59 56 58 mpbid ⊢ ( 𝜑 → 𝐴 = 𝐶 )