Metamath Proof Explorer

Theorem isngp4

Description: Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015)

Ref Expression
Hypotheses ngprcan.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
ngprcan.p ⊢ + = ( +g ‘ 𝐺 )
ngprcan.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
Assertion isngp4 ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 ngprcan.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 ngprcan.p ⊢ + = ( +g ‘ 𝐺 )
3 ngprcan.d ⊢ 𝐷 = ( dist ‘ 𝐺 )
4 ngpgrp ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
5 ngpms ⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp )
6 1 2 3 ngprcan ⊢ ( ( 𝐺 ∈ NrmGrp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) )
7 6 ralrimivvva ⊢ ( 𝐺 ∈ NrmGrp → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) )
8 4 5 7 3jca ⊢ ( 𝐺 ∈ NrmGrp → ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ) )
9 simp1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ) → 𝐺 ∈ Grp )
10 simp2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ) → 𝐺 ∈ MetSp )
11 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
12 1 11 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 )
13 12 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 )
14 eqcom ⊢ ( ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ↔ ( 𝑥 𝐷 𝑦 ) = ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) )
15 oveq2 ⊢ ( 𝑧 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( 𝑥 + 𝑧 ) = ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
16 oveq2 ⊢ ( 𝑧 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( 𝑦 + 𝑧 ) = ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
17 15 16 oveq12d ⊢ ( 𝑧 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) 𝐷 ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
18 17 eqeq2d ⊢ ( 𝑧 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( ( 𝑥 𝐷 𝑦 ) = ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) ↔ ( 𝑥 𝐷 𝑦 ) = ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) 𝐷 ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) ) )
19 14 18 bitrid ⊢ ( 𝑧 = ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) → ( ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ↔ ( 𝑥 𝐷 𝑦 ) = ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) 𝐷 ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) ) )
20 19 rspcv ⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) 𝐷 ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) ) )
21 13 20 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) 𝐷 ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) ) )
22 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
23 1 2 11 22 grpsubval ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
24 23 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
25 24 eqcomd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) )
26 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
27 1 2 26 11 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 0g ‘ 𝐺 ) )
28 27 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) = ( 0g ‘ 𝐺 ) )
29 25 28 oveq12d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) 𝐷 ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) 𝐷 ( 0g ‘ 𝐺 ) ) )
30 1 22 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
31 30 3expb ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
32 31 adantlr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
33 eqid ⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
34 33 1 26 3 nmval ⊢ ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 → ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) 𝐷 ( 0g ‘ 𝐺 ) ) )
35 32 34 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) 𝐷 ( 0g ‘ 𝐺 ) ) )
36 29 35 eqtr4d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) 𝐷 ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) )
37 36 eqeq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = ( ( 𝑥 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) 𝐷 ( 𝑦 + ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ) ↔ ( 𝑥 𝐷 𝑦 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) ) )
38 21 37 sylibd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) ) )
39 38 ralimdvva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) ) )
40 39 3impia ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) )
41 33 22 3 1 isngp3 ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐷 𝑦 ) = ( ( norm ‘ 𝐺 ) ‘ ( 𝑥 ( -g ‘ 𝐺 ) 𝑦 ) ) ) )
42 9 10 40 41 syl3anbrc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ) → 𝐺 ∈ NrmGrp )
43 8 42 impbii ⊢ ( 𝐺 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 + 𝑧 ) 𝐷 ( 𝑦 + 𝑧 ) ) = ( 𝑥 𝐷 𝑦 ) ) )