Metamath Proof Explorer


Theorem nm2dif

Description: Inequality for the difference of norms. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses nmf.x X = Base G
nmf.n N = norm G
nmmtri.m - ˙ = - G
Assertion nm2dif G NrmGrp A X B X N A N B N A - ˙ B

Proof

Step Hyp Ref Expression
1 nmf.x X = Base G
2 nmf.n N = norm G
3 nmmtri.m - ˙ = - G
4 1 2 nmcl G NrmGrp A X N A
5 4 3adant3 G NrmGrp A X B X N A
6 1 2 nmcl G NrmGrp B X N B
7 6 3adant2 G NrmGrp A X B X N B
8 5 7 resubcld G NrmGrp A X B X N A N B
9 8 recnd G NrmGrp A X B X N A N B
10 9 abscld G NrmGrp A X B X N A N B
11 simp1 G NrmGrp A X B X G NrmGrp
12 ngpgrp G NrmGrp G Grp
13 1 3 grpsubcl G Grp A X B X A - ˙ B X
14 12 13 syl3an1 G NrmGrp A X B X A - ˙ B X
15 1 2 nmcl G NrmGrp A - ˙ B X N A - ˙ B
16 11 14 15 syl2anc G NrmGrp A X B X N A - ˙ B
17 8 leabsd G NrmGrp A X B X N A N B N A N B
18 1 2 3 nmrtri G NrmGrp A X B X N A N B N A - ˙ B
19 8 10 16 17 18 letrd G NrmGrp A X B X N A N B N A - ˙ B