| Step |
Hyp |
Ref |
Expression |
| 1 |
|
nghmplusg.p |
⊢ + = ( +g ‘ 𝑇 ) |
| 2 |
|
nghmrcl1 |
⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑆 ∈ NrmGrp ) |
| 3 |
2
|
3ad2ant2 |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑆 ∈ NrmGrp ) |
| 4 |
|
nghmrcl2 |
⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝑇 ∈ NrmGrp ) |
| 5 |
4
|
3ad2ant2 |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → 𝑇 ∈ NrmGrp ) |
| 6 |
|
id |
⊢ ( 𝑇 ∈ Abel → 𝑇 ∈ Abel ) |
| 7 |
|
nghmghm |
⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) |
| 8 |
|
nghmghm |
⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) |
| 9 |
1
|
ghmplusg |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 GrpHom 𝑇 ) ) |
| 10 |
6 7 8 9
|
syl3an |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 GrpHom 𝑇 ) ) |
| 11 |
|
eqid |
⊢ ( 𝑆 normOp 𝑇 ) = ( 𝑆 normOp 𝑇 ) |
| 12 |
11
|
nghmcl |
⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) ∈ ℝ ) |
| 13 |
12
|
3ad2ant2 |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) ∈ ℝ ) |
| 14 |
11
|
nghmcl |
⊢ ( 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ∈ ℝ ) |
| 15 |
14
|
3ad2ant3 |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ∈ ℝ ) |
| 16 |
13 15
|
readdcld |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ∈ ℝ ) |
| 17 |
11 1
|
nmotri |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( ( 𝑆 normOp 𝑇 ) ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ) |
| 18 |
11
|
bddnghm |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ∈ ℝ ∧ ( ( 𝑆 normOp 𝑇 ) ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ ( ( ( 𝑆 normOp 𝑇 ) ‘ 𝐹 ) + ( ( 𝑆 normOp 𝑇 ) ‘ 𝐺 ) ) ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 NGHom 𝑇 ) ) |
| 19 |
3 5 10 16 17 18
|
syl32anc |
⊢ ( ( 𝑇 ∈ Abel ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 NGHom 𝑇 ) ) → ( 𝐹 ∘f + 𝐺 ) ∈ ( 𝑆 NGHom 𝑇 ) ) |