R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.90184
M₆ : Type ?u.90187
S✝ : Type ?u.90190
inst✝¹³ : Semiring R
inst✝¹² : Semiring S✝
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid M₅
inst✝⁶ : AddCommMonoid M₆
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R M₅
inst✝ : Module R M₆
f✝ : M →ₗ[R] M₂
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun a => ↑f a.fst + ↑g a.snd) '' ↑(Submodule.prod S S') = (fun a => ↑f a) '' ↑S + (fun a => ↑g a) '' ↑S'
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.90184
M₆ : Type ?u.90187
S✝ : Type ?u.90190
inst✝¹³ : Semiring R
inst✝¹² : Semiring S✝
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid M₅
inst✝⁶ : AddCommMonoid M₆
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R M₅
inst✝ : Module R M₆
f✝ : M →ₗ[R] M₂
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ ↑(Submodule.map (coprod f g) (Submodule.prod S S')) = ↑(Submodule.map f S ⊔ Submodule.map g S')
simp only [LinearMap.coprod_apply, Submodule.coe_sup, Submodule.map_coe]
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.90184
M₆ : Type ?u.90187
S✝ : Type ?u.90190
inst✝¹³ : Semiring R
inst✝¹² : Semiring S✝
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid M₅
inst✝⁶ : AddCommMonoid M₆
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R M₅
inst✝ : Module R M₆
f✝ : M →ₗ[R] M₂
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun a => ↑f a.fst + ↑g a.snd) '' ↑(Submodule.prod S S') = Set.image2 (fun a b => ↑f a + ↑g b) ↑S ↑S'
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.90184
M₆ : Type ?u.90187
S✝ : Type ?u.90190
inst✝¹³ : Semiring R
inst✝¹² : Semiring S✝
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid M₅
inst✝⁶ : AddCommMonoid M₆
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R M₅
inst✝ : Module R M₆
f✝ : M →ₗ[R] M₂
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun a => ↑f a.fst + ↑g a.snd) '' ↑(Submodule.prod S S') = (fun a => ↑f a) '' ↑S + (fun a => ↑g a) '' ↑S'
rw [← Set.image2_add, Set.image2_image_left, Set.image2_image_right]
no goals
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type ?u.90184
M₆ : Type ?u.90187
S✝ : Type ?u.90190
inst✝¹³ : Semiring R
inst✝¹² : Semiring S✝
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid M₅
inst✝⁶ : AddCommMonoid M₆
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R M₅
inst✝ : Module R M₆
f✝ : M →ₗ[R] M₂
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
S : Submodule R M
S' : Submodule R M₂
⊢ (fun a => ↑f a.fst + ↑g a.snd) '' ↑(Submodule.prod S S') = Set.image2 (fun a b => ↑f a + ↑g b) ↑S ↑S'
exact Set.image_prod fun m m₂ => f m + g m₂