Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict

Goal state before:
pp: case hom_continuous
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ Continuous[_, inst✝³] ⇑(nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯)

pp: case hom_injective
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ Function.Injective ⇑(nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯)

pp: case hom_id
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ (nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯)
      { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    a

pp: case hom_map_spectrum
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∀ (f_1 : C(↑(σₙ R a), R)₀), σₙ R ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) f_1) = range ⇑f_1

pp: case predicate_hom
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∀ (f_1 : C(↑(σₙ R a), R)₀), p ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) f_1)

Tactic:
case hom_continuous => exact continuous_nonUnitalStarAlgHom (cfcₙHom_continuous _) _

Goal state after:
case hom_injective
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ Function.Injective ⇑(nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯)

case hom_id
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ (nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯)
      { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    a

case hom_map_spectrum
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∀ (f_1 : C(↑(σₙ R a), R)₀), σₙ R ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) f_1) = range ⇑f_1

case predicate_hom
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²³ : Semifield R
inst✝²² : StarRing R
inst✝²¹ : MetricSpace R
inst✝²⁰ : IsTopologicalSemiring R
inst✝¹⁹ : ContinuousStar R
inst✝¹⁸ : Field S
inst✝¹⁷ : StarRing S
inst✝¹⁶ : MetricSpace S
inst✝¹⁵ : IsTopologicalRing S
inst✝¹⁴ : ContinuousStar S
inst✝¹³ : NonUnitalRing A
inst✝¹² : StarRing A
inst✝¹¹ : Module S A
inst✝¹⁰ : IsScalarTower S A A
inst✝⁹ : SMulCommClass S A A
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus S A q
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsClosedEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∀ (f_1 : C(↑(σₙ R a), R)₀), p ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) f_1)