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 ) )