Step |
Hyp |
Ref |
Expression |
1 |
|
nmtri2.x |
|- X = ( Base ` G ) |
2 |
|
nmtri2.n |
|- N = ( norm ` G ) |
3 |
|
nmtri2.m |
|- .- = ( -g ` G ) |
4 |
|
ngpgrp |
|- ( G e. NrmGrp -> G e. Grp ) |
5 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
6 |
1 5 3
|
grpnpncan |
|- ( ( G e. Grp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A .- B ) ( +g ` G ) ( B .- C ) ) = ( A .- C ) ) |
7 |
6
|
eqcomd |
|- ( ( G e. Grp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .- C ) = ( ( A .- B ) ( +g ` G ) ( B .- C ) ) ) |
8 |
4 7
|
sylan |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .- C ) = ( ( A .- B ) ( +g ` G ) ( B .- C ) ) ) |
9 |
8
|
fveq2d |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( A .- C ) ) = ( N ` ( ( A .- B ) ( +g ` G ) ( B .- C ) ) ) ) |
10 |
|
simpl |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. NrmGrp ) |
11 |
4
|
adantr |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. Grp ) |
12 |
|
simpr1 |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A e. X ) |
13 |
|
simpr2 |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> B e. X ) |
14 |
1 3
|
grpsubcl |
|- ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( A .- B ) e. X ) |
15 |
11 12 13 14
|
syl3anc |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A .- B ) e. X ) |
16 |
|
simpr3 |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> C e. X ) |
17 |
1 3
|
grpsubcl |
|- ( ( G e. Grp /\ B e. X /\ C e. X ) -> ( B .- C ) e. X ) |
18 |
11 13 16 17
|
syl3anc |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B .- C ) e. X ) |
19 |
1 2 5
|
nmtri |
|- ( ( G e. NrmGrp /\ ( A .- B ) e. X /\ ( B .- C ) e. X ) -> ( N ` ( ( A .- B ) ( +g ` G ) ( B .- C ) ) ) <_ ( ( N ` ( A .- B ) ) + ( N ` ( B .- C ) ) ) ) |
20 |
10 15 18 19
|
syl3anc |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( ( A .- B ) ( +g ` G ) ( B .- C ) ) ) <_ ( ( N ` ( A .- B ) ) + ( N ` ( B .- C ) ) ) ) |
21 |
9 20
|
eqbrtrd |
|- ( ( G e. NrmGrp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( N ` ( A .- C ) ) <_ ( ( N ` ( A .- B ) ) + ( N ` ( B .- C ) ) ) ) |