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