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 |
|
incom |
⊢ ( 𝑇 ∩ 𝑈 ) = ( 𝑈 ∩ 𝑇 ) |
14 |
13 6
|
eqtr3id |
⊢ ( 𝜑 → ( 𝑈 ∩ 𝑇 ) = { 0 } ) |
15 |
3 4 5 7
|
cntzrecd |
⊢ ( 𝜑 → 𝑈 ⊆ ( 𝑍 ‘ 𝑇 ) ) |
16 |
7 8
|
sseldd |
⊢ ( 𝜑 → 𝐴 ∈ ( 𝑍 ‘ 𝑈 ) ) |
17 |
1 3
|
cntzi |
⊢ ( ( 𝐴 ∈ ( 𝑍 ‘ 𝑈 ) ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) |
18 |
16 10 17
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) ) |
19 |
7 9
|
sseldd |
⊢ ( 𝜑 → 𝐶 ∈ ( 𝑍 ‘ 𝑈 ) ) |
20 |
1 3
|
cntzi |
⊢ ( ( 𝐶 ∈ ( 𝑍 ‘ 𝑈 ) ∧ 𝐷 ∈ 𝑈 ) → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) ) |
21 |
19 11 20
|
syl2anc |
⊢ ( 𝜑 → ( 𝐶 + 𝐷 ) = ( 𝐷 + 𝐶 ) ) |
22 |
12 18 21
|
3eqtr3d |
⊢ ( 𝜑 → ( 𝐵 + 𝐴 ) = ( 𝐷 + 𝐶 ) ) |
23 |
1 2 3 5 4 14 15 10 11 8 9 22
|
subgdisj1 |
⊢ ( 𝜑 → 𝐵 = 𝐷 ) |