[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule T ≤ ↑toSubmodule (S ⊔ T)
[PROOFSTEP]
rw [Submodule.mul_le]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ∀ (m : A), m ∈ ↑toSubmodule S → ∀ (n : A), n ∈ ↑toSubmodule T → m * n ∈ ↑toSubmodule (S ⊔ T)
[PROOFSTEP]
intro y hy z hz
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ ↑toSubmodule S
z : A
hz : z ∈ ↑toSubmodule T
⊢ y * z ∈ ↑toSubmodule (S ⊔ T)
[PROOFSTEP]
show y * z ∈ S ⊔ T
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ ↑toSubmodule S
z : A
hz : z ∈ ↑toSubmodule T
⊢ y * z ∈ S ⊔ T
[PROOFSTEP]
exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule S = ↑toSubmodule S
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule S ≤ ↑toSubmodule S
[PROOFSTEP]
refine' (mul_toSubmodule_le _ _).trans_eq _
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule (S ⊔ S) = ↑toSubmodule S
[PROOFSTEP]
rw [sup_idem]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S ≤ ↑toSubmodule S * ↑toSubmodule S
[PROOFSTEP]
intro x hx1
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ ↑toSubmodule S
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule S
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ ↑toSubmodule S
⊢ x * 1 ∈ ↑toSubmodule S * ↑toSubmodule S
[PROOFSTEP]
exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)
[GOAL]
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule T = ↑toSubmodule (S ⊔ T)
[PROOFSTEP]
refine' le_antisymm (mul_toSubmodule_le _ _) _
[GOAL]
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule (S ⊔ T) ≤ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rintro x (hx : x ∈ Algebra.adjoin R (S ∪ T : Set A))
[GOAL]
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
refine' Algebra.adjoin_induction hx (fun x hx => _) (fun r => _) (fun _ _ => Submodule.add_mem _) fun x y hx hy => _
[GOAL]
case refine'_1
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hx : x ∈ ↑S ∪ ↑T
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
cases' hx with hxS hxT
[GOAL]
case refine'_1.inl
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
case refine'_1.inl
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x * 1 ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
exact Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)
[GOAL]
case refine'_1.inr
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rw [← one_mul x]
[GOAL]
case refine'_1.inr
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ 1 * x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) hxT
[GOAL]
case refine'_2
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ ↑(algebraMap R A) r ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rw [← one_mul (algebraMap _ _ _)]
[GOAL]
case refine'_2
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ 1 * ↑(algebraMap R A) r ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem T _)
[GOAL]
case refine'_3
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
hx : x ∈ ↑toSubmodule S * ↑toSubmodule T
hy : y ∈ ↑toSubmodule S * ↑toSubmodule T
⊢ x * y ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
have := Submodule.mul_mem_mul hx hy
[GOAL]
case refine'_3
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
hx : x ∈ ↑toSubmodule S * ↑toSubmodule T
hy : y ∈ ↑toSubmodule S * ↑toSubmodule T
this : x * y ∈ ↑toSubmodule S * ↑toSubmodule T * (↑toSubmodule S * ↑toSubmodule T)
⊢ x * y ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rwa [mul_assoc, mul_comm _ (Subalgebra.toSubmodule T), ← mul_assoc _ _ (Subalgebra.toSubmodule S), mul_self,
  mul_comm (Subalgebra.toSubmodule T), ← mul_assoc, mul_self] at this 
