[GOAL]
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
⊢ Continuous ↑(algebraMap R A) ↔ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous ↑(algebraMap R A)
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
simp only [Algebra.smul_def]
[GOAL]
case refine'_1
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous ↑(algebraMap R A)
⊢ Continuous fun p => ↑(algebraMap R A) p.fst * p.snd
[PROOFSTEP]
exact (h.comp continuous_fst).mul continuous_snd
[GOAL]
case refine'_2
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous fun p => p.fst • p.snd
⊢ Continuous ↑(algebraMap R A)
[PROOFSTEP]
rw [algebraMap_eq_smul_one']
[GOAL]
case refine'_2
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous fun p => p.fst • p.snd
⊢ Continuous fun r => r • 1
[PROOFSTEP]
exact h.comp (continuous_id.prod_mk continuous_const)
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : TopologicalSemiring A
s : Subalgebra R A
⊢ IsClosed ↑(topologicalClosure s)
[PROOFSTEP]
convert @isClosed_closure A _ s
[GOAL]
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : TopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ↑f = ↑f'
⊢ comap f (topologicalClosure s) = topologicalClosure (comap f s)
[PROOFSTEP]
apply SetLike.ext'
[GOAL]
case h
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : TopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ↑f = ↑f'
⊢ ↑(comap f (topologicalClosure s)) = ↑(topologicalClosure (comap f s))
[PROOFSTEP]
simp only [Subalgebra.topologicalClosure_coe]
[GOAL]
case h
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : TopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ↑f = ↑f'
⊢ ↑(comap f (topologicalClosure s)) = closure ↑(comap f s)
[PROOFSTEP]
simp only [Subalgebra.coe_comap, Subsemiring.coe_comap, AlgHom.coe_toRingHom]
[GOAL]
case h
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : TopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ↑f = ↑f'
⊢ ↑f ⁻¹' ↑(topologicalClosure s) = closure (↑f ⁻¹' ↑s)
[PROOFSTEP]
rw [w]
[GOAL]
case h
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : TopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst✝³ : TopologicalSpace B
inst✝² : Ring B
inst✝¹ : TopologicalRing B
inst✝ : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : ↑f = ↑f'
⊢ ↑f' ⁻¹' ↑(topologicalClosure s) = closure (↑f' ⁻¹' ↑s)
[PROOFSTEP]
exact f'.preimage_closure _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : TopologicalRing A
inst✝ : T2Space A
x y : A
hy : y ∈ {x}
z : A
hz : z ∈ {x}
⊢ y * z = z * y
[PROOFSTEP]
rw [mem_singleton_iff] at hy hz
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : TopologicalRing A
inst✝ : T2Space A
x y : A
hy : y = x
z : A
hz : z = x
⊢ y * z = z * y
[PROOFSTEP]
rw [hy, hz]
[GOAL]
A : Type ?u.199010
inst✝³ : DivisionRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousMul A
inst✝ : CharZero A
r : ℚ
⊢ Continuous fun x => r • x
[PROOFSTEP]
simpa only [Algebra.smul_def] using continuous_const.mul continuous_id