tngngp3

Description: Alternate definition of a normed group (i.e., a group equipped with a norm) without using the properties of a metric space. This corresponds to the definition in N. H. Bingham, A. J. Ostaszewski: "Normed versus topological groups: dichotomy and duality", 2010, Dissertationes Mathematicae 472, pp. 1-138 and E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006. (Contributed by AV, 16-Oct-2021)

	Ref	Expression
Hypotheses	tngngp3.t	$⊢ T = G toNrmGrp N$
	tngngp3.x	$⊢ X = {Base}_{G}$
	tngngp3.z	$⊢ \underset{˙}{0} = 0_{G}$
	tngngp3.p	$⊢ \underset{˙}{+} = +_{G}$
	tngngp3.i	$⊢ I = {inv}_{g} (G)$
Assertion	tngngp3	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))))$

Proof

Step	Hyp	Ref	Expression
1		tngngp3.t	$⊢ T = G toNrmGrp N$
2		tngngp3.x	$⊢ X = {Base}_{G}$
3		tngngp3.z	$⊢ \underset{˙}{0} = 0_{G}$
4		tngngp3.p	$⊢ \underset{˙}{+} = +_{G}$
5		tngngp3.i	$⊢ I = {inv}_{g} (G)$
6	2	fvexi	$⊢ X \in V$
7		fex	$⊢ (N : X ⟶ ℝ \land X \in V) \to N \in V$
8	6 7	mpan2	$⊢ N : X ⟶ ℝ \to N \in V$
9	1	tnggrpr	$⊢ (N \in V \land T \in NrmGrp) \to G \in Grp$
10		simp2	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to G \in Grp$
11		eqid	$⊢ {Base}_{T} = {Base}_{T}$
12		eqid	$⊢ norm (T) = norm (T)$
13		eqid	$⊢ 0_{T} = 0_{T}$
14	11 12 13	nmeq0	$⊢ (T \in NrmGrp \land x \in {Base}_{T}) \to (norm (T) (x) = 0 \leftrightarrow x = 0_{T})$
15		eqid	$⊢ {inv}_{g} (T) = {inv}_{g} (T)$
16	11 12 15	nminv	$⊢ (T \in NrmGrp \land x \in {Base}_{T}) \to norm (T) ({inv}_{g} (T) (x)) = norm (T) (x)$
17		eqid	$⊢ +_{T} = +_{T}$
18	11 12 17	nmtri	$⊢ (T \in NrmGrp \land x \in {Base}_{T} \land y \in {Base}_{T}) \to norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y)$
19	18	3expa	$⊢ ((T \in NrmGrp \land x \in {Base}_{T}) \land y \in {Base}_{T}) \to norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y)$
20	19	ralrimiva	$⊢ (T \in NrmGrp \land x \in {Base}_{T}) \to \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y)$
21	14 16 20	3jca	$⊢ (T \in NrmGrp \land x \in {Base}_{T}) \to ((norm (T) (x) = 0 \leftrightarrow x = 0_{T}) \land norm (T) ({inv}_{g} (T) (x)) = norm (T) (x) \land \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y))$
22	21	ralrimiva	$⊢ T \in NrmGrp \to \forall x \in {Base}_{T} ((norm (T) (x) = 0 \leftrightarrow x = 0_{T}) \land norm (T) ({inv}_{g} (T) (x)) = norm (T) (x) \land \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y))$
23	22	adantl	$⊢ (N \in V \land T \in NrmGrp) \to \forall x \in {Base}_{T} ((norm (T) (x) = 0 \leftrightarrow x = 0_{T}) \land norm (T) ({inv}_{g} (T) (x)) = norm (T) (x) \land \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y))$
24	23	3ad2ant1	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to \forall x \in {Base}_{T} ((norm (T) (x) = 0 \leftrightarrow x = 0_{T}) \land norm (T) ({inv}_{g} (T) (x)) = norm (T) (x) \land \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y))$
25	1 2	tngbas	$⊢ N \in V \to X = {Base}_{T}$
26	1 4	tngplusg	$⊢ N \in V \to \underset{˙}{+} = +_{T}$
27		eqidd	$⊢ N \in V \to {Base}_{G} = {Base}_{G}$
28		eqid	$⊢ {Base}_{G} = {Base}_{G}$
29	1 28	tngbas	$⊢ N \in V \to {Base}_{G} = {Base}_{T}$
30		eqid	$⊢ +_{G} = +_{G}$
31	1 30	tngplusg	$⊢ N \in V \to +_{G} = +_{T}$
32	31	oveqd	$⊢ N \in V \to x +_{G} y = x +_{T} y$
33	32	adantr	$⊢ (N \in V \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to x +_{G} y = x +_{T} y$
34	27 29 33	grpinvpropd	$⊢ N \in V \to {inv}_{g} (G) = {inv}_{g} (T)$
35	5 34	syl5eq	$⊢ N \in V \to I = {inv}_{g} (T)$
36	25 26 35	3jca	$⊢ N \in V \to (X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T))$
37	36	adantr	$⊢ (N \in V \land T \in NrmGrp) \to (X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T))$
38	37	3ad2ant1	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to (X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T))$
39		reex	$⊢ ℝ \in V$
40	1 2 39	tngnm	$⊢ (G \in Grp \land N : X ⟶ ℝ) \to N = norm (T)$
41	40	3adant1	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to N = norm (T)$
42	1 3	tng0	$⊢ N \in V \to \underset{˙}{0} = 0_{T}$
43	42	adantr	$⊢ (N \in V \land T \in NrmGrp) \to \underset{˙}{0} = 0_{T}$
44	43	3ad2ant1	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to \underset{˙}{0} = 0_{T}$
45	38 41 44	3jca	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T})$
46		simp1	$⊢ (X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \to X = {Base}_{T}$
47	46	3ad2ant1	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to X = {Base}_{T}$
48		simp2	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to N = norm (T)$
49	48	fveq1d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to N (x) = norm (T) (x)$
50	49	eqeq1d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to (N (x) = 0 \leftrightarrow norm (T) (x) = 0)$
51		simp3	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to \underset{˙}{0} = 0_{T}$
52	51	eqeq2d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to (x = \underset{˙}{0} \leftrightarrow x = 0_{T})$
53	50 52	bibi12d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \leftrightarrow (norm (T) (x) = 0 \leftrightarrow x = 0_{T}))$
54		simp3	$⊢ (X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \to I = {inv}_{g} (T)$
55	54	3ad2ant1	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to I = {inv}_{g} (T)$
56	55	fveq1d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to I (x) = {inv}_{g} (T) (x)$
57	48 56	fveq12d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to N (I (x)) = norm (T) ({inv}_{g} (T) (x))$
58	57 49	eqeq12d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to (N (I (x)) = N (x) \leftrightarrow norm (T) ({inv}_{g} (T) (x)) = norm (T) (x))$
59		simp2	$⊢ (X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \to \underset{˙}{+} = +_{T}$
60	59	3ad2ant1	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to \underset{˙}{+} = +_{T}$
61	60	oveqd	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to x \underset{˙}{+} y = x +_{T} y$
62	48 61	fveq12d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to N (x \underset{˙}{+} y) = norm (T) (x +_{T} y)$
63		fveq1	$⊢ N = norm (T) \to N (x) = norm (T) (x)$
64		fveq1	$⊢ N = norm (T) \to N (y) = norm (T) (y)$
65	63 64	oveq12d	$⊢ N = norm (T) \to N (x) + N (y) = norm (T) (x) + norm (T) (y)$
66	65	3ad2ant2	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to N (x) + N (y) = norm (T) (x) + norm (T) (y)$
67	62 66	breq12d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to (N (x \underset{˙}{+} y) \leq N (x) + N (y) \leftrightarrow norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y))$
68	47 67	raleqbidv	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to (\forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y) \leftrightarrow \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y))$
69	53 58 68	3anbi123d	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to (((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \leftrightarrow ((norm (T) (x) = 0 \leftrightarrow x = 0_{T}) \land norm (T) ({inv}_{g} (T) (x)) = norm (T) (x) \land \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y)))$
70	47 69	raleqbidv	$⊢ ((X = {Base}_{T} \land \underset{˙}{+} = +_{T} \land I = {inv}_{g} (T)) \land N = norm (T) \land \underset{˙}{0} = 0_{T}) \to (\forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \leftrightarrow \forall x \in {Base}_{T} ((norm (T) (x) = 0 \leftrightarrow x = 0_{T}) \land norm (T) ({inv}_{g} (T) (x)) = norm (T) (x) \land \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y)))$
71	45 70	syl	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to (\forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \leftrightarrow \forall x \in {Base}_{T} ((norm (T) (x) = 0 \leftrightarrow x = 0_{T}) \land norm (T) ({inv}_{g} (T) (x)) = norm (T) (x) \land \forall y \in {Base}_{T} norm (T) (x +_{T} y) \leq norm (T) (x) + norm (T) (y)))$
72	24 71	mpbird	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))$
73	10 72	jca	$⊢ ((N \in V \land T \in NrmGrp) \land G \in Grp \land N : X ⟶ ℝ) \to (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))$
74	73	3exp	$⊢ (N \in V \land T \in NrmGrp) \to (G \in Grp \to (N : X ⟶ ℝ \to (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))))$
75	9 74	mpd	$⊢ (N \in V \land T \in NrmGrp) \to (N : X ⟶ ℝ \to (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))))$
76	75	expcom	$⊢ T \in NrmGrp \to (N \in V \to (N : X ⟶ ℝ \to (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))))$
77	76	com13	$⊢ N : X ⟶ ℝ \to (N \in V \to (T \in NrmGrp \to (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))))$
78	8 77	mpd	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \to (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))))$
79		eqid	$⊢ -_{G} = -_{G}$
80		simpl	$⊢ (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))) \to G \in Grp$
81	80	adantl	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \to G \in Grp$
82		simpl	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \to N : X ⟶ ℝ$
83		fveq2	$⊢ x = a \to N (x) = N (a)$
84	83	eqeq1d	$⊢ x = a \to (N (x) = 0 \leftrightarrow N (a) = 0)$
85		eqeq1	$⊢ x = a \to (x = \underset{˙}{0} \leftrightarrow a = \underset{˙}{0})$
86	84 85	bibi12d	$⊢ x = a \to ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \leftrightarrow (N (a) = 0 \leftrightarrow a = \underset{˙}{0}))$
87		fveq2	$⊢ x = a \to I (x) = I (a)$
88	87	fveq2d	$⊢ x = a \to N (I (x)) = N (I (a))$
89	88 83	eqeq12d	$⊢ x = a \to (N (I (x)) = N (x) \leftrightarrow N (I (a)) = N (a))$
90		fvoveq1	$⊢ x = a \to N (x \underset{˙}{+} y) = N (a \underset{˙}{+} y)$
91	83	oveq1d	$⊢ x = a \to N (x) + N (y) = N (a) + N (y)$
92	90 91	breq12d	$⊢ x = a \to (N (x \underset{˙}{+} y) \leq N (x) + N (y) \leftrightarrow N (a \underset{˙}{+} y) \leq N (a) + N (y))$
93	92	ralbidv	$⊢ x = a \to (\forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y) \leftrightarrow \forall y \in X N (a \underset{˙}{+} y) \leq N (a) + N (y))$
94	86 89 93	3anbi123d	$⊢ x = a \to (((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \leftrightarrow ((N (a) = 0 \leftrightarrow a = \underset{˙}{0}) \land N (I (a)) = N (a) \land \forall y \in X N (a \underset{˙}{+} y) \leq N (a) + N (y)))$
95	94	rspccva	$⊢ (\forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land a \in X) \to ((N (a) = 0 \leftrightarrow a = \underset{˙}{0}) \land N (I (a)) = N (a) \land \forall y \in X N (a \underset{˙}{+} y) \leq N (a) + N (y))$
96		simp1	$⊢ ((N (a) = 0 \leftrightarrow a = \underset{˙}{0}) \land N (I (a)) = N (a) \land \forall y \in X N (a \underset{˙}{+} y) \leq N (a) + N (y)) \to (N (a) = 0 \leftrightarrow a = \underset{˙}{0})$
97	95 96	syl	$⊢ (\forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land a \in X) \to (N (a) = 0 \leftrightarrow a = \underset{˙}{0})$
98	97	ex	$⊢ \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to (a \in X \to (N (a) = 0 \leftrightarrow a = \underset{˙}{0}))$
99	98	adantl	$⊢ (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))) \to (a \in X \to (N (a) = 0 \leftrightarrow a = \underset{˙}{0}))$
100	99	adantl	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \to (a \in X \to (N (a) = 0 \leftrightarrow a = \underset{˙}{0}))$
101	100	imp	$⊢ ((N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \land a \in X) \to (N (a) = 0 \leftrightarrow a = \underset{˙}{0})$
102	2 4 5 79	grpsubval	$⊢ (a \in X \land b \in X) \to a -_{G} b = a \underset{˙}{+} I (b)$
103	102	adantl	$⊢ ((N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \land (a \in X \land b \in X)) \to a -_{G} b = a \underset{˙}{+} I (b)$
104	103	fveq2d	$⊢ ((N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \land (a \in X \land b \in X)) \to N (a -_{G} b) = N (a \underset{˙}{+} I (b))$
105		3simpc	$⊢ ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))$
106	105	ralimi	$⊢ \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to \forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))$
107		simpr	$⊢ (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)$
108	107	ralimi	$⊢ \forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to \forall x \in X \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)$
109		oveq2	$⊢ y = I (b) \to a \underset{˙}{+} y = a \underset{˙}{+} I (b)$
110	109	fveq2d	$⊢ y = I (b) \to N (a \underset{˙}{+} y) = N (a \underset{˙}{+} I (b))$
111		fveq2	$⊢ y = I (b) \to N (y) = N (I (b))$
112	111	oveq2d	$⊢ y = I (b) \to N (a) + N (y) = N (a) + N (I (b))$
113	110 112	breq12d	$⊢ y = I (b) \to (N (a \underset{˙}{+} y) \leq N (a) + N (y) \leftrightarrow N (a \underset{˙}{+} I (b)) \leq N (a) + N (I (b)))$
114	92 113	rspc2v	$⊢ (a \in X \land I (b) \in X) \to (\forall x \in X \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (I (b)))$
115	2 5	grpinvcl	$⊢ (G \in Grp \land b \in X) \to I (b) \in X$
116	115	ex	$⊢ G \in Grp \to (b \in X \to I (b) \in X)$
117	116	anim2d	$⊢ G \in Grp \to ((a \in X \land b \in X) \to (a \in X \land I (b) \in X))$
118	117	imp	$⊢ (G \in Grp \land (a \in X \land b \in X)) \to (a \in X \land I (b) \in X)$
119	114 118	syl11	$⊢ \forall x \in X \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y) \to ((G \in Grp \land (a \in X \land b \in X)) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (I (b)))$
120	119	expd	$⊢ \forall x \in X \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y) \to (G \in Grp \to ((a \in X \land b \in X) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (I (b))))$
121	108 120	syl	$⊢ \forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to (G \in Grp \to ((a \in X \land b \in X) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (I (b))))$
122	121	imp	$⊢ (\forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land G \in Grp) \to ((a \in X \land b \in X) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (I (b)))$
123	122	imp	$⊢ ((\forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land G \in Grp) \land (a \in X \land b \in X)) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (I (b))$
124		simpl	$⊢ (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to N (I (x)) = N (x)$
125	124	ralimi	$⊢ \forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to \forall x \in X N (I (x)) = N (x)$
126		fveq2	$⊢ x = b \to I (x) = I (b)$
127	126	fveq2d	$⊢ x = b \to N (I (x)) = N (I (b))$
128		fveq2	$⊢ x = b \to N (x) = N (b)$
129	127 128	eqeq12d	$⊢ x = b \to (N (I (x)) = N (x) \leftrightarrow N (I (b)) = N (b))$
130	129	rspccva	$⊢ (\forall x \in X N (I (x)) = N (x) \land b \in X) \to N (I (b)) = N (b)$
131	130	eqcomd	$⊢ (\forall x \in X N (I (x)) = N (x) \land b \in X) \to N (b) = N (I (b))$
132	131	ex	$⊢ \forall x \in X N (I (x)) = N (x) \to (b \in X \to N (b) = N (I (b)))$
133	125 132	syl	$⊢ \forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to (b \in X \to N (b) = N (I (b)))$
134	133	adantr	$⊢ (\forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land G \in Grp) \to (b \in X \to N (b) = N (I (b)))$
135	134	adantld	$⊢ (\forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land G \in Grp) \to ((a \in X \land b \in X) \to N (b) = N (I (b)))$
136	135	imp	$⊢ ((\forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land G \in Grp) \land (a \in X \land b \in X)) \to N (b) = N (I (b))$
137	136	oveq2d	$⊢ ((\forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land G \in Grp) \land (a \in X \land b \in X)) \to N (a) + N (b) = N (a) + N (I (b))$
138	123 137	breqtrrd	$⊢ ((\forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land G \in Grp) \land (a \in X \land b \in X)) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (b)$
139	138	ex	$⊢ (\forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \land G \in Grp) \to ((a \in X \land b \in X) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (b))$
140	139	ex	$⊢ \forall x \in X (N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to (G \in Grp \to ((a \in X \land b \in X) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (b)))$
141	106 140	syl	$⊢ \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)) \to (G \in Grp \to ((a \in X \land b \in X) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (b)))$
142	141	impcom	$⊢ (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))) \to ((a \in X \land b \in X) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (b))$
143	142	adantl	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \to ((a \in X \land b \in X) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (b))$
144	143	imp	$⊢ ((N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \land (a \in X \land b \in X)) \to N (a \underset{˙}{+} I (b)) \leq N (a) + N (b)$
145	104 144	eqbrtrd	$⊢ ((N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \land (a \in X \land b \in X)) \to N (a -_{G} b) \leq N (a) + N (b)$
146	1 2 79 3 81 82 101 145	tngngpd	$⊢ (N : X ⟶ ℝ \land (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y)))) \to T \in NrmGrp$
147	146	ex	$⊢ N : X ⟶ ℝ \to ((G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))) \to T \in NrmGrp)$
148	78 147	impbid	$⊢ N : X ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land \forall x \in X ((N (x) = 0 \leftrightarrow x = \underset{˙}{0}) \land N (I (x)) = N (x) \land \forall y \in X N (x \underset{˙}{+} y) \leq N (x) + N (y))))$

Metamath Proof Explorer

Theorem tngngp3

Proof