case disjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ Disjoint p (ker f)

case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ Codisjoint p (ker f)
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ IsCompl p (ker f)
constructor
case disjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ p ⊓ ker f ≤ ⊥
case disjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ Disjoint p (ker f)
rw [disjoint_iff_inf_le]
case disjoint.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
hpx : x ∈ ↑p
hfx : x ∈ ↑(ker f)
⊢ x ∈ ⊥
case disjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ p ⊓ ker f ≤ ⊥
rintro x ⟨hpx, hfx⟩
case disjoint.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
hpx : x ∈ ↑p
hfx : x = 0
⊢ x ∈ ⊥
case disjoint.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
hpx : x ∈ ↑p
hfx : x ∈ ↑(ker f)
⊢ x ∈ ⊥
erw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx
no goals
case disjoint.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
hpx : x ∈ ↑p
hfx : x = 0
⊢ x ∈ ⊥
simp only [hfx, SetLike.mem_coe, zero_mem]
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ ⊤ ≤ p ⊔ ker f
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ Codisjoint p (ker f)
rw [codisjoint_iff_le_sup]
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
a✝ : x ∈ ⊤
⊢ x ∈ p ⊔ ker f
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ ⊤ ≤ p ⊔ ker f
intro x _
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
a✝ : x ∈ ⊤
⊢ ∃ y z, ↑y + ↑z = x
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
a✝ : x ∈ ⊤
⊢ x ∈ p ⊔ ker f
rw [mem_sup']
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
a✝ : x ∈ ⊤
⊢ x - ↑(↑f x) ∈ ker f
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
a✝ : x ∈ ⊤
⊢ ∃ y z, ↑y + ↑z = x
refine' ⟨f x, ⟨x - f x, _⟩, add_sub_cancel'_right _ _⟩
no goals
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.23402
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.23918
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.24881
inst✝² : Semiring S
M : Type ?u.24887
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
a✝ : x ∈ ⊤
⊢ x - ↑(↑f x) ∈ ker f
rw [mem_ker, LinearMap.map_sub, hf, sub_self]