[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ Subtype.val ⁻¹' ↑S₁ = range ↑(inclusion h)
[PROOFSTEP]
convert (Set.range_subtype_map id _).symm
[GOAL]
case h.e'_2.h.e'_4
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ↑S₁ = id '' {x | x ∈ S₁}
[PROOFSTEP]
rw [Set.image_id]
[GOAL]
case h.e'_2.h.e'_4
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ↑S₁ = {x | x ∈ S₁}
[PROOFSTEP]
rfl
[GOAL]
case convert_4
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ∀ (x : A), x ∈ S₁ → id x ∈ S₂
[PROOFSTEP]
intro _ h'
[GOAL]
case convert_4
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
x✝ : A
h' : x✝ ∈ S₁
⊢ id x✝ ∈ S₂
[PROOFSTEP]
apply h h'
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : StarRing A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSemiring A
inst✝⁴ : ContinuousStar A
inst✝³ : TopologicalSpace B
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : StarRing B
s : Subalgebra R A
⊢ Subalgebra.topologicalClosure (star s) = star (Subalgebra.topologicalClosure s)
[PROOFSTEP]
suffices ∀ t : Subalgebra R A, (star t).topologicalClosure ≤ star t.topologicalClosure from
  le_antisymm (this s) (by simpa only [star_star] using Subalgebra.star_mono (this (star s)))
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : StarRing A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSemiring A
inst✝⁴ : ContinuousStar A
inst✝³ : TopologicalSpace B
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : StarRing B
s : Subalgebra R A
this : ∀ (t : Subalgebra R A), Subalgebra.topologicalClosure (star t) ≤ star (Subalgebra.topologicalClosure t)
⊢ star (Subalgebra.topologicalClosure s) ≤ Subalgebra.topologicalClosure (star s)
[PROOFSTEP]
simpa only [star_star] using Subalgebra.star_mono (this (star s))
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : StarRing A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSemiring A
inst✝⁴ : ContinuousStar A
inst✝³ : TopologicalSpace B
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : StarRing B
s : Subalgebra R A
⊢ ∀ (t : Subalgebra R A), Subalgebra.topologicalClosure (star t) ≤ star (Subalgebra.topologicalClosure t)
[PROOFSTEP]
exact fun t =>
  (star t).topologicalClosure_minimal (Subalgebra.star_mono subset_closure) (isClosed_closure.preimage continuous_star)
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
⊢ φ = ψ
[PROOFSTEP]
rw [FunLike.ext'_iff]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
⊢ ↑φ = ↑ψ
[PROOFSTEP]
have : Dense (Set.range <| inclusion (le_topologicalClosure S)) :=
  by
  refine' embedding_subtype_val.toInducing.dense_iff.2 fun x => _
  convert show ↑x ∈ closure (S : Set A) from x.prop
  rw [← Set.range_comp]
  exact
    Set.ext fun y =>
      ⟨by
        rintro ⟨y, rfl⟩
        exact y.prop, fun hy => ⟨⟨y, hy⟩, rfl⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
⊢ Dense (range ↑(inclusion (_ : S ≤ topologicalClosure S)))
[PROOFSTEP]
refine' embedding_subtype_val.toInducing.dense_iff.2 fun x => _
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
x : { x // x ∈ topologicalClosure S }
⊢ ↑x ∈ closure (Subtype.val '' range ↑(inclusion (_ : S ≤ topologicalClosure S)))
[PROOFSTEP]
convert show ↑x ∈ closure (S : Set A) from x.prop
[GOAL]
case h.e'_5.h.e'_3
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
x : { x // x ∈ topologicalClosure S }
⊢ Subtype.val '' range ↑(inclusion (_ : S ≤ topologicalClosure S)) = ↑S
[PROOFSTEP]
rw [← Set.range_comp]
[GOAL]
case h.e'_5.h.e'_3
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
x : { x // x ∈ topologicalClosure S }
⊢ range (Subtype.val ∘ ↑(inclusion (_ : S ≤ topologicalClosure S))) = ↑S
[PROOFSTEP]
exact
  Set.ext fun y =>
    ⟨by
      rintro ⟨y, rfl⟩
      exact y.prop, fun hy => ⟨⟨y, hy⟩, rfl⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
x : { x // x ∈ topologicalClosure S }
y : A
⊢ y ∈ range (Subtype.val ∘ ↑(inclusion (_ : S ≤ topologicalClosure S))) → y ∈ ↑S
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
x : { x // x ∈ topologicalClosure S }
y : { x // x ∈ S }
⊢ (Subtype.val ∘ ↑(inclusion (_ : S ≤ topologicalClosure S))) y ∈ ↑S
[PROOFSTEP]
exact y.prop
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
this : Dense (range ↑(inclusion (_ : S ≤ topologicalClosure S)))
⊢ ↑φ = ↑ψ
[PROOFSTEP]
refine' Continuous.ext_on this hφ hψ _
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
this : Dense (range ↑(inclusion (_ : S ≤ topologicalClosure S)))
⊢ EqOn (↑φ) (↑ψ) (range ↑(inclusion (_ : S ≤ topologicalClosure S)))
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹³ : CommSemiring R
inst✝¹² : StarRing R
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : Algebra R A
inst✝⁸ : StarRing A
inst✝⁷ : StarModule R A
inst✝⁶ : TopologicalSemiring A
inst✝⁵ : ContinuousStar A
inst✝⁴ : TopologicalSpace B
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : T2Space B
S : StarSubalgebra R A
φ ψ : { x // x ∈ topologicalClosure S } →⋆ₐ[R] B
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  StarAlgHom.comp φ (inclusion (_ : S ≤ topologicalClosure S)) =
    StarAlgHom.comp ψ (inclusion (_ : S ≤ topologicalClosure S))
this : Dense (range ↑(inclusion (_ : S ≤ topologicalClosure S)))
x : { x // x ∈ S }
⊢ ↑φ (↑(inclusion (_ : S ≤ topologicalClosure S)) x) = ↑ψ (↑(inclusion (_ : S ≤ topologicalClosure S)) x)
[PROOFSTEP]
simpa only using FunLike.congr_fun h x
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : StarRing A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst✝ : StarAlgHomClass F R { x // x ∈ topologicalClosure S } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ∀ (x : { x // x ∈ S }),
    ↑φ (↑(inclusion (_ : S ≤ topologicalClosure S)) x) = ↑ψ (↑(inclusion (_ : S ≤ topologicalClosure S)) x)
⊢ φ = ψ
[PROOFSTEP]
have : (φ : S.topologicalClosure →⋆ₐ[R] B) = (ψ : S.topologicalClosure →⋆ₐ[R] B) :=
  by
  refine StarAlgHom.ext_topologicalClosure (R := R) (A := A) (B := B) hφ hψ (StarAlgHom.ext ?_)
  simpa only [StarAlgHom.coe_comp, StarAlgHom.coe_coe] using h
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : StarRing A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst✝ : StarAlgHomClass F R { x // x ∈ topologicalClosure S } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ∀ (x : { x // x ∈ S }),
    ↑φ (↑(inclusion (_ : S ≤ topologicalClosure S)) x) = ↑ψ (↑(inclusion (_ : S ≤ topologicalClosure S)) x)
⊢ ↑φ = ↑ψ
[PROOFSTEP]
refine StarAlgHom.ext_topologicalClosure (R := R) (A := A) (B := B) hφ hψ (StarAlgHom.ext ?_)
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : StarRing A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst✝ : StarAlgHomClass F R { x // x ∈ topologicalClosure S } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ∀ (x : { x // x ∈ S }),
    ↑φ (↑(inclusion (_ : S ≤ topologicalClosure S)) x) = ↑ψ (↑(inclusion (_ : S ≤ topologicalClosure S)) x)
⊢ ∀ (x : { x // x ∈ S }),
    ↑(StarAlgHom.comp (↑φ) (inclusion (_ : S ≤ topologicalClosure S))) x =
      ↑(StarAlgHom.comp (↑ψ) (inclusion (_ : S ≤ topologicalClosure S))) x
[PROOFSTEP]
simpa only [StarAlgHom.coe_comp, StarAlgHom.coe_coe] using h
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : StarRing A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst✝ : StarAlgHomClass F R { x // x ∈ topologicalClosure S } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ∀ (x : { x // x ∈ S }),
    ↑φ (↑(inclusion (_ : S ≤ topologicalClosure S)) x) = ↑ψ (↑(inclusion (_ : S ≤ topologicalClosure S)) x)
this : ↑φ = ↑ψ
⊢ φ = ψ
[PROOFSTEP]
rw [FunLike.ext'_iff, ← StarAlgHom.coe_coe]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : StarRing A
inst✝⁸ : StarModule R A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : T2Space B
F : Type u_4
S : StarSubalgebra R A
inst✝ : StarAlgHomClass F R { x // x ∈ topologicalClosure S } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ∀ (x : { x // x ∈ S }),
    ↑φ (↑(inclusion (_ : S ≤ topologicalClosure S)) x) = ↑ψ (↑(inclusion (_ : S ≤ topologicalClosure S)) x)
this : ↑φ = ↑ψ
⊢ ↑↑φ = ↑ψ
[PROOFSTEP]
apply congrArg _ this
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra R A
inst✝⁴ : StarModule R A
inst✝³ : TopologicalSpace B
inst✝² : Semiring B
inst✝¹ : StarRing B
inst✝ : Algebra R B
x : A
⊢ IsClosed (range Subtype.val)
[PROOFSTEP]
convert elementalStarAlgebra.isClosed R x
[GOAL]
case h.e'_3
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra R A
inst✝⁴ : StarModule R A
inst✝³ : TopologicalSpace B
inst✝² : Semiring B
inst✝¹ : StarRing B
inst✝ : Algebra R B
x : A
⊢ range Subtype.val = ↑(elementalStarAlgebra R x)
[PROOFSTEP]
exact
  Set.ext fun y =>
    ⟨by
      rintro ⟨y, rfl⟩
      exact y.prop, fun hy => ⟨⟨y, hy⟩, rfl⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra R A
inst✝⁴ : StarModule R A
inst✝³ : TopologicalSpace B
inst✝² : Semiring B
inst✝¹ : StarRing B
inst✝ : Algebra R B
x y : A
⊢ y ∈ range Subtype.val → y ∈ ↑(elementalStarAlgebra R x)
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : Semiring A
inst✝⁸ : StarRing A
inst✝⁷ : TopologicalSemiring A
inst✝⁶ : ContinuousStar A
inst✝⁵ : Algebra R A
inst✝⁴ : StarModule R A
inst✝³ : TopologicalSpace B
inst✝² : Semiring B
inst✝¹ : StarRing B
inst✝ : Algebra R B
x : A
y : { x_1 // x_1 ∈ ↑(elementalStarAlgebra R x) }
⊢ ↑y ∈ ↑(elementalStarAlgebra R x)
[PROOFSTEP]
exact y.prop
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
⊢ φ = ψ
[PROOFSTEP]
refine StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x : { x // x ∈ adjoin R {a} }
⊢ ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x)
[PROOFSTEP]
apply adjoin_induction' x ?_ ?_ ?_ ?_ ?_
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x : { x // x ∈ adjoin R {a} }
⊢ ∀ (x : A) (h : x ∈ {a}),
    ↑φ
        (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a})))
          { val := x, property := (_ : x ∈ ↑(adjoin R {a})) }) =
      ↑ψ
        (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a})))
          { val := x, property := (_ : x ∈ ↑(adjoin R {a})) })
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x : { x // x ∈ adjoin R {a} }
⊢ ∀ (r : R),
    ↑φ
        (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a})))
          (↑(algebraMap R { x // x ∈ adjoin R {a} }) r)) =
      ↑ψ
        (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a})))
          (↑(algebraMap R { x // x ∈ adjoin R {a} }) r))
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x : { x // x ∈ adjoin R {a} }
⊢ ∀ (x y : { x // x ∈ adjoin R {a} }),
    ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) =
        ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) →
      ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) y) =
          ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) y) →
        ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (x + y)) =
          ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (x + y))
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x : { x // x ∈ adjoin R {a} }
⊢ ∀ (x y : { x // x ∈ adjoin R {a} }),
    ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) =
        ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) →
      ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) y) =
          ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) y) →
        ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (x * y)) =
          ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (x * y))
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x : { x // x ∈ adjoin R {a} }
⊢ ∀ (x : { x // x ∈ adjoin R {a} }),
    ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) =
        ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) →
      ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (star x)) =
        ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (star x))
[PROOFSTEP]
exacts [fun y hy => by simpa only [Set.mem_singleton_iff.mp hy] using h, fun r => by simp only [AlgHomClass.commutes],
  fun x y hx hy => by simp only [map_add, hx, hy], fun x y hx hy => by simp only [map_mul, hx, hy], fun x hx => by
  simp only [map_star, hx]]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x : { x // x ∈ adjoin R {a} }
y : A
hy : y ∈ {a}
⊢ ↑φ
      (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a})))
        { val := y, property := (_ : y ∈ ↑(adjoin R {a})) }) =
    ↑ψ
      (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a})))
        { val := y, property := (_ : y ∈ ↑(adjoin R {a})) })
[PROOFSTEP]
simpa only [Set.mem_singleton_iff.mp hy] using h
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x : { x // x ∈ adjoin R {a} }
r : R
⊢ ↑φ
      (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a})))
        (↑(algebraMap R { x // x ∈ adjoin R {a} }) r)) =
    ↑ψ
      (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a})))
        (↑(algebraMap R { x // x ∈ adjoin R {a} }) r))
[PROOFSTEP]
simp only [AlgHomClass.commutes]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x✝ x y : { x // x ∈ adjoin R {a} }
hx :
  ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x)
hy :
  ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) y) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) y)
⊢ ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (x + y)) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (x + y))
[PROOFSTEP]
simp only [map_add, hx, hy]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x✝ x y : { x // x ∈ adjoin R {a} }
hx :
  ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x)
hy :
  ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) y) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) y)
⊢ ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (x * y)) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (x * y))
[PROOFSTEP]
simp only [map_mul, hx, hy]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : StarRing R
inst✝¹² : TopologicalSpace A
inst✝¹¹ : Semiring A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : ContinuousStar A
inst✝⁷ : Algebra R A
inst✝⁶ : StarModule R A
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring B
inst✝³ : StarRing B
inst✝² : Algebra R B
inst✝¹ : T2Space B
F : Type u_4
a : A
inst✝ : StarAlgHomClass F R { x // x ∈ elementalStarAlgebra R a } B
φ ψ : F
hφ : Continuous ↑φ
hψ : Continuous ↑ψ
h :
  ↑φ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) } =
    ↑ψ { val := a, property := (_ : a ∈ elementalStarAlgebra R a) }
x✝ x : { x // x ∈ adjoin R {a} }
hx :
  ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) x)
⊢ ↑φ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (star x)) =
    ↑ψ (↑(StarSubalgebra.inclusion (_ : adjoin R {a} ≤ topologicalClosure (adjoin R {a}))) (star x))
[PROOFSTEP]
simp only [map_star, hx]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace γ
a b c : α
h : a ≤ b
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
s : Set ↑(Icc a b)
hs : IsOpen (projIcc a b h ⁻¹' s)
⊢ Subtype.val ⁻¹' (projIcc a b h ⁻¹' s) = s
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace γ
a b c : α
h : a ≤ b
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
s : Set ↑(Icc a b)
hs : IsOpen (projIcc a b h ⁻¹' s)
x✝ : { x // x ∈ Icc a b }
⊢ x✝ ∈ Subtype.val ⁻¹' (projIcc a b h ⁻¹' s) ↔ x✝ ∈ s
[PROOFSTEP]
simp