This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ngppropd

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

Ref Expression
Hypotheses ngppropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
ngppropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
ngppropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
ngppropd.4 ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) )
ngppropd.5 ⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐿 ) )
Assertion ngppropd ( 𝜑 → ( 𝐾 ∈ NrmGrp ↔ 𝐿 ∈ NrmGrp ) )

Proof

Step Hyp Ref Expression
1 ngppropd.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 ngppropd.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3 ngppropd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4 ngppropd.4 ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) )
5 ngppropd.5 ⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐿 ) )
6 1 2 4 5 mspropd ⊢ ( 𝜑 → ( 𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp ) )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → ( 𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp ) )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → 𝐵 = ( Base ‘ 𝐾 ) )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → 𝐵 = ( Base ‘ 𝐿 ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → 𝐾 ∈ Grp )
11 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ Grp ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
12 4 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) )
13 8 9 10 11 12 nmpropd2 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → ( norm ‘ 𝐾 ) = ( norm ‘ 𝐿 ) )
14 8 9 10 11 grpsubpropd2 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → ( -g ‘ 𝐾 ) = ( -g ‘ 𝐿 ) )
15 13 14 coeq12d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) )
16 1 sqxpeqd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
17 16 reseq2d ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
18 2 sqxpeqd ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) )
19 18 reseq2d ⊢ ( 𝜑 → ( ( dist ‘ 𝐿 ) ↾ ( 𝐵 × 𝐵 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
20 4 17 19 3eqtr3d ⊢ ( 𝜑 → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) )
22 15 21 eqeq12d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → ( ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ↔ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) )
23 7 22 anbi12d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ Grp ) → ( ( 𝐾 ∈ MetSp ∧ ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ↔ ( 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) )
24 23 pm5.32da ⊢ ( 𝜑 → ( ( 𝐾 ∈ Grp ∧ ( 𝐾 ∈ MetSp ∧ ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ) ↔ ( 𝐾 ∈ Grp ∧ ( 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) ) )
25 1 2 3 grppropd ⊢ ( 𝜑 → ( 𝐾 ∈ Grp ↔ 𝐿 ∈ Grp ) )
26 25 anbi1d ⊢ ( 𝜑 → ( ( 𝐾 ∈ Grp ∧ ( 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) ↔ ( 𝐿 ∈ Grp ∧ ( 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) ) )
27 24 26 bitrd ⊢ ( 𝜑 → ( ( 𝐾 ∈ Grp ∧ ( 𝐾 ∈ MetSp ∧ ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ) ↔ ( 𝐿 ∈ Grp ∧ ( 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) ) )
28 3anass ⊢ ( ( 𝐾 ∈ Grp ∧ 𝐾 ∈ MetSp ∧ ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ↔ ( 𝐾 ∈ Grp ∧ ( 𝐾 ∈ MetSp ∧ ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ) )
29 3anass ⊢ ( ( 𝐿 ∈ Grp ∧ 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ↔ ( 𝐿 ∈ Grp ∧ ( 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) )
30 27 28 29 3bitr4g ⊢ ( 𝜑 → ( ( 𝐾 ∈ Grp ∧ 𝐾 ∈ MetSp ∧ ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ↔ ( 𝐿 ∈ Grp ∧ 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) ) )
31 eqid ⊢ ( norm ‘ 𝐾 ) = ( norm ‘ 𝐾 )
32 eqid ⊢ ( -g ‘ 𝐾 ) = ( -g ‘ 𝐾 )
33 eqid ⊢ ( dist ‘ 𝐾 ) = ( dist ‘ 𝐾 )
34 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
35 eqid ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
36 31 32 33 34 35 isngp2 ⊢ ( 𝐾 ∈ NrmGrp ↔ ( 𝐾 ∈ Grp ∧ 𝐾 ∈ MetSp ∧ ( ( norm ‘ 𝐾 ) ∘ ( -g ‘ 𝐾 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
37 eqid ⊢ ( norm ‘ 𝐿 ) = ( norm ‘ 𝐿 )
38 eqid ⊢ ( -g ‘ 𝐿 ) = ( -g ‘ 𝐿 )
39 eqid ⊢ ( dist ‘ 𝐿 ) = ( dist ‘ 𝐿 )
40 eqid ⊢ ( Base ‘ 𝐿 ) = ( Base ‘ 𝐿 )
41 eqid ⊢ ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) )
42 37 38 39 40 41 isngp2 ⊢ ( 𝐿 ∈ NrmGrp ↔ ( 𝐿 ∈ Grp ∧ 𝐿 ∈ MetSp ∧ ( ( norm ‘ 𝐿 ) ∘ ( -g ‘ 𝐿 ) ) = ( ( dist ‘ 𝐿 ) ↾ ( ( Base ‘ 𝐿 ) × ( Base ‘ 𝐿 ) ) ) ) )
43 30 36 42 3bitr4g ⊢ ( 𝜑 → ( 𝐾 ∈ NrmGrp ↔ 𝐿 ∈ NrmGrp ) )