Metamath Proof Explorer


Theorem ngppropd

Description: Property deduction for a normed group. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses ngppropd.1 φ B = Base K
ngppropd.2 φ B = Base L
ngppropd.3 φ x B y B x + K y = x + L y
ngppropd.4 φ dist K B × B = dist L B × B
ngppropd.5 φ TopOpen K = TopOpen L
Assertion ngppropd φ K NrmGrp L NrmGrp

Proof

Step Hyp Ref Expression
1 ngppropd.1 φ B = Base K
2 ngppropd.2 φ B = Base L
3 ngppropd.3 φ x B y B x + K y = x + L y
4 ngppropd.4 φ dist K B × B = dist L B × B
5 ngppropd.5 φ TopOpen K = TopOpen L
6 1 2 4 5 mspropd φ K MetSp L MetSp
7 6 adantr φ K Grp K MetSp L MetSp
8 1 adantr φ K Grp B = Base K
9 2 adantr φ K Grp B = Base L
10 simpr φ K Grp K Grp
11 3 adantlr φ K Grp x B y B x + K y = x + L y
12 4 adantr φ K Grp dist K B × B = dist L B × B
13 8 9 10 11 12 nmpropd2 φ K Grp norm K = norm L
14 8 9 10 11 grpsubpropd2 φ K Grp - K = - L
15 13 14 coeq12d φ K Grp norm K - K = norm L - L
16 1 sqxpeqd φ B × B = Base K × Base K
17 16 reseq2d φ dist K B × B = dist K Base K × Base K
18 2 sqxpeqd φ B × B = Base L × Base L
19 18 reseq2d φ dist L B × B = dist L Base L × Base L
20 4 17 19 3eqtr3d φ dist K Base K × Base K = dist L Base L × Base L
21 20 adantr φ K Grp dist K Base K × Base K = dist L Base L × Base L
22 15 21 eqeq12d φ K Grp norm K - K = dist K Base K × Base K norm L - L = dist L Base L × Base L
23 7 22 anbi12d φ K Grp K MetSp norm K - K = dist K Base K × Base K L MetSp norm L - L = dist L Base L × Base L
24 23 pm5.32da φ K Grp K MetSp norm K - K = dist K Base K × Base K K Grp L MetSp norm L - L = dist L Base L × Base L
25 1 2 3 grppropd φ K Grp L Grp
26 25 anbi1d φ K Grp L MetSp norm L - L = dist L Base L × Base L L Grp L MetSp norm L - L = dist L Base L × Base L
27 24 26 bitrd φ K Grp K MetSp norm K - K = dist K Base K × Base K L Grp L MetSp norm L - L = dist L Base L × Base L
28 3anass K Grp K MetSp norm K - K = dist K Base K × Base K K Grp K MetSp norm K - K = dist K Base K × Base K
29 3anass L Grp L MetSp norm L - L = dist L Base L × Base L L Grp L MetSp norm L - L = dist L Base L × Base L
30 27 28 29 3bitr4g φ K Grp K MetSp norm K - K = dist K Base K × Base K L Grp L MetSp norm L - L = dist L Base L × Base L
31 eqid norm K = norm K
32 eqid - K = - K
33 eqid dist K = dist K
34 eqid Base K = Base K
35 eqid dist K Base K × Base K = dist K Base K × Base K
36 31 32 33 34 35 isngp2 K NrmGrp K Grp K MetSp norm K - K = dist K Base K × Base K
37 eqid norm L = norm L
38 eqid - L = - L
39 eqid dist L = dist L
40 eqid Base L = Base L
41 eqid dist L Base L × Base L = dist L Base L × Base L
42 37 38 39 40 41 isngp2 L NrmGrp L Grp L MetSp norm L - L = dist L Base L × Base L
43 30 36 42 3bitr4g φ K NrmGrp L NrmGrp