M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
⊢ ‖normedMk S‖ = 0
refine' le_antisymm (opNorm_le_bound _ le_rfl fun x => _) (norm_nonneg _)
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
hker : x ∈ topologicalClosure (ker (normedMk S))
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
have hker : x ∈ S.normedMk.ker.topologicalClosure := by
  rw [S.ker_normedMk, ← SetLike.mem_coe, h]
  trivial
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
hker : x ∈ topologicalClosure S
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
hker : x ∈ topologicalClosure (ker (normedMk S))
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
rw [ker_normedMk] at hker
no goals
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
hker : x ∈ topologicalClosure S
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
simp only [(quotient_norm_eq_zero_iff S x).mpr hker, normedMk.apply, zero_mul, le_rfl]
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ x ∈ univ
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ x ∈ topologicalClosure (ker (normedMk S))
rw [S.ker_normedMk, ← SetLike.mem_coe, h]
no goals
M : Type u_1
N : Type ?u.456398
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ x ∈ univ
trivial