[GOAL]
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
n : ℕ
N : Fin n → Type u_5
inst✝³ : (i : Fin n) → AddCommGroup (N i)
inst✝² : (i : Fin n) → Module R (N i)
inst✝¹ : ∀ (i : Fin n), Module.Finite R (N i)
inst✝ : ∀ (i : Fin n), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n : ℕ
N✝ : Fin n → Type u_5
inst✝⁷ : (i : Fin n) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n), Module.Free R (N✝ i)
N : Fin Nat.zero → Type u_5
inst✝³ : (i : Fin Nat.zero) → AddCommGroup (N i)
inst✝² : (i : Fin Nat.zero) → Module R (N i)
inst✝¹ : ∀ (i : Fin Nat.zero), Module.Finite R (N i)
inst✝ : ∀ (i : Fin Nat.zero), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
haveI : IsEmpty (Fin Nat.zero) := inferInstanceAs (IsEmpty (Fin 0))
[GOAL]
case zero
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n : ℕ
N✝ : Fin n → Type u_5
inst✝⁷ : (i : Fin n) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n), Module.Free R (N✝ i)
N : Fin Nat.zero → Type u_5
inst✝³ : (i : Fin Nat.zero) → AddCommGroup (N i)
inst✝² : (i : Fin Nat.zero) → Module R (N i)
inst✝¹ : ∀ (i : Fin Nat.zero), Module.Finite R (N i)
inst✝ : ∀ (i : Fin Nat.zero), Module.Free R (N i)
this : IsEmpty (Fin Nat.zero)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
exact ⟨Module.Free.of_equiv (constLinearEquivOfIsEmpty R N M₂), Module.Finite.equiv (constLinearEquivOfIsEmpty R N M₂)⟩
[GOAL]
case succ
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
suffices
  Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i : Fin n => N i.succ) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i : Fin n => N i.succ) M₂)
  by
  cases this
  exact
    ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂), Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂)⟩
[GOAL]
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
this :
  Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
cases this
[GOAL]
case intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
left✝ : Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
right✝ : Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
[PROOFSTEP]
exact ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂), Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂)⟩
[GOAL]
case succ
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
⊢ Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
[PROOFSTEP]
cases ih fun i => N i.succ
[GOAL]
case succ.intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝¹³ : Finite ι
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module.Finite R M₂
inst✝⁸ : Module.Free R M₂
n✝ : ℕ
N✝ : Fin n✝ → Type u_5
inst✝⁷ : (i : Fin n✝) → AddCommGroup (N✝ i)
inst✝⁶ : (i : Fin n✝) → Module R (N✝ i)
inst✝⁵ : ∀ (i : Fin n✝), Module.Finite R (N✝ i)
inst✝⁴ : ∀ (i : Fin n✝), Module.Free R (N✝ i)
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [inst_2 : ∀ (i : Fin n), Module.Finite R (N i)] [inst_3 : ∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (Nat.succ n) → Type u_5
inst✝³ : (i : Fin (Nat.succ n)) → AddCommGroup (N i)
inst✝² : (i : Fin (Nat.succ n)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (Nat.succ n)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (Nat.succ n)), Module.Free R (N i)
left✝ : Module.Free R (MultilinearMap R (fun i => N (Fin.succ i)) M₂)
right✝ : Module.Finite R (MultilinearMap R (fun i => N (Fin.succ i)) M₂)
⊢ Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i => N (Fin.succ i)) M₂)
[PROOFSTEP]
exact ⟨Module.Free.linearMap _ _ _, Module.Finite.linearMap _ _⟩
[GOAL]
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
have := @free_and_finite_fin R M₂ _ _ _ _ _ (Fintype.card ι) (fun x => M₁ ((Fintype.equivFin ι).symm x))
[GOAL]
case intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
this :
  ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_2 : ∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_3 : ∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ (↑(Fintype.equivFin ι).symm i))],
    Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂) ∧
      Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
cases' this with l r
[GOAL]
case intro.intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
this :
  ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_2 : ∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_3 : ∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ (↑(Fintype.equivFin ι).symm i))],
    Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂) ∧
      Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
l : Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
r : Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
have e := domDomCongrLinearEquiv' R M₁ M₂ (Fintype.equivFin ι)
[GOAL]
case intro.intro
ι : Type u_1
R : Type u_2
M₂ : Type u_3
M₁ : ι → Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
inst✝³ : (i : ι) → AddCommGroup (M₁ i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : ∀ (i : ι), Module.Finite R (M₁ i)
inst✝ : ∀ (i : ι), Module.Free R (M₁ i)
val✝ : Fintype ι
this :
  ∀ [inst : (i : Fin (Fintype.card ι)) → AddCommGroup (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_1 : (i : Fin (Fintype.card ι)) → Module R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_2 : ∀ (i : Fin (Fintype.card ι)), Module.Finite R (M₁ (↑(Fintype.equivFin ι).symm i))]
    [inst_3 : ∀ (i : Fin (Fintype.card ι)), Module.Free R (M₁ (↑(Fintype.equivFin ι).symm i))],
    Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂) ∧
      Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
l : Module.Free R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
r : Module.Finite R (MultilinearMap R (fun x => M₁ (↑(Fintype.equivFin ι).symm x)) M₂)
e : MultilinearMap R M₁ M₂ ≃ₗ[R] MultilinearMap R (fun i => M₁ (↑(Fintype.equivFin ι).symm i)) M₂
⊢ Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
[PROOFSTEP]
exact ⟨Module.Free.of_equiv e.symm, Module.Finite.equiv e.symm⟩


[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
⊢ ker (id - comp (Submodule.subtype p) f) = p
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
⊢ x ∈ ker (id - comp (Submodule.subtype p) f) ↔ x ∈ p
[PROOFSTEP]
simp only [comp_apply, mem_ker, subtype_apply, sub_apply, id_apply, sub_eq_zero]
[GOAL]
case h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
⊢ x = ↑(↑f x) ↔ x ∈ p
[PROOFSTEP]
exact ⟨fun h => h.symm ▸ Submodule.coe_mem _, fun hx => by erw [hf ⟨x, hx⟩, Subtype.coe_mk]⟩
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
hx : x ∈ p
⊢ x = ↑(↑f x)
[PROOFSTEP]
erw [hf ⟨x, hx⟩, Subtype.coe_mk]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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)
[PROOFSTEP]
constructor
[GOAL]
case disjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case disjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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 ≤ ⊥
[PROOFSTEP]
rintro x ⟨hpx, hfx⟩
[GOAL]
case disjoint.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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 ∈ ⊥
[PROOFSTEP]
erw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx
[GOAL]
case disjoint.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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 ∈ ⊥
[PROOFSTEP]
simp only [hfx, SetLike.mem_coe, zero_mem]
[GOAL]
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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)
[PROOFSTEP]
rw [codisjoint_iff_le_sup]
[GOAL]
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
[PROOFSTEP]
intro x _
[GOAL]
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
[PROOFSTEP]
rw [mem_sup']
[GOAL]
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
[PROOFSTEP]
refine' ⟨f x, ⟨x - f x, _⟩, add_sub_cancel'_right _ _⟩
[GOAL]
case codisjoint
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
[PROOFSTEP]
rw [mem_ker, LinearMap.map_sub, hf, sub_self]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Injective ↑(comp (mkQ p) (Submodule.subtype q))
[PROOFSTEP]
rw [← ker_eq_bot, ker_comp, ker_mkQ, disjoint_iff_comap_eq_bot.1 h.symm.disjoint]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Surjective ↑(comp (mkQ p) (Submodule.subtype q))
[PROOFSTEP]
rw [← range_eq_top, range_comp, range_subtype, map_mkQ_eq_top, h.sup_eq_top]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ ({ x // x ∈ p } × { x // x ∈ q }) ≃ₗ[R] E
[PROOFSTEP]
apply LinearEquiv.ofBijective (p.subtype.coprod q.subtype)
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Bijective ↑(coprod (Submodule.subtype p) (Submodule.subtype q))
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Injective ↑(coprod (Submodule.subtype p) (Submodule.subtype q))
[PROOFSTEP]
rw [← ker_eq_bot, ker_coprod_of_disjoint_range, ker_subtype, ker_subtype, prod_bot]
[GOAL]
case left.hd
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Disjoint (range (Submodule.subtype p)) (range (Submodule.subtype q))
[PROOFSTEP]
rw [range_subtype, range_subtype]
[GOAL]
case left.hd
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Disjoint p q
[PROOFSTEP]
exact h.1
[GOAL]
case right
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Surjective ↑(coprod (Submodule.subtype p) (Submodule.subtype q))
[PROOFSTEP]
rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : { x // x ∈ p }
⊢ ↑x = ↑(prodEquivOfIsCompl p q h) (x, 0)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : { x // x ∈ q }
⊢ ↑x = ↑(prodEquivOfIsCompl p q h) (0, x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x).fst = 0 ↔ x ∈ q
[PROOFSTEP]
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
| x ∈ q
[PROOFSTEP]
rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
| x ∈ q
[PROOFSTEP]
rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
| x ∈ q
[PROOFSTEP]
rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x).fst = 0 ↔
    ↑(prodEquivOfIsCompl p q h) (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x) ∈ q
[PROOFSTEP]
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
  mem_right_iff_eq_zero_of_disjoint h.disjoint]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x).snd = 0 ↔ x ∈ p
[PROOFSTEP]
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
| x ∈ p
[PROOFSTEP]
rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
| x ∈ p
[PROOFSTEP]
rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
| x ∈ p
[PROOFSTEP]
rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x).snd = 0 ↔
    ↑(prodEquivOfIsCompl p q h) (↑(LinearEquiv.symm (prodEquivOfIsCompl p q h)) x) ∈ p
[PROOFSTEP]
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
  mem_left_iff_eq_zero_of_disjoint h.disjoint]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : { x // x ∈ p }
⊢ ↑(linearProjOfIsCompl p q h) ↑x = x
[PROOFSTEP]
simp [linearProjOfIsCompl]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x : E
⊢ ↑(linearProjOfIsCompl p q h) x = 0 ↔ x ∈ q
[PROOFSTEP]
simp [linearProjOfIsCompl]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hpq : IsCompl p q
x : E
⊢ ↑(↑(linearProjOfIsCompl p q hpq) x) + ↑(↑(linearProjOfIsCompl q p (_ : IsCompl q p)) x) = x
[PROOFSTEP]
dsimp only [linearProjOfIsCompl]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hpq : IsCompl p q
x : E
⊢ ↑(↑(comp (LinearMap.fst R { x // x ∈ p } { x // x ∈ q }) ↑(LinearEquiv.symm (prodEquivOfIsCompl p q hpq))) x) +
      ↑(↑(comp (LinearMap.fst R { x // x ∈ q } { x // x ∈ p })
              ↑(LinearEquiv.symm (prodEquivOfIsCompl q p (_ : IsCompl q p))))
          x) =
    x
[PROOFSTEP]
rw [← prodComm_trans_prodEquivOfIsCompl _ _ hpq]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hpq : IsCompl p q
x : E
⊢ ↑(↑(comp (LinearMap.fst R { x // x ∈ p } { x // x ∈ q }) ↑(LinearEquiv.symm (prodEquivOfIsCompl p q hpq))) x) +
      ↑(↑(comp (LinearMap.fst R { x // x ∈ q } { x // x ∈ p })
              ↑(LinearEquiv.symm
                  (LinearEquiv.trans (LinearEquiv.prodComm R { x // x ∈ q } { x // x ∈ p })
                    (prodEquivOfIsCompl p q hpq))))
          x) =
    x
[PROOFSTEP]
exact (prodEquivOfIsCompl _ _ hpq).apply_symm_apply x
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
u : { x // x ∈ p }
⊢ ↑(ofIsCompl h φ ψ) ↑u = ↑φ u
[PROOFSTEP]
simp [ofIsCompl]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
v : { x // x ∈ q }
⊢ ↑(ofIsCompl h φ ψ) ↑v = ↑ψ v
[PROOFSTEP]
simp [ofIsCompl]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u
hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u
⊢ ofIsCompl h φ ψ = χ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u
hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u
x : E
⊢ ↑(ofIsCompl h φ ψ) x = ↑χ x
[PROOFSTEP]
obtain ⟨_, _, rfl, _⟩ := existsUnique_add_of_isCompl h x
[GOAL]
case h.intro.intro.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
χ : E →ₗ[R] F
hφ : ∀ (u : { x // x ∈ p }), ↑φ u = ↑χ ↑u
hψ : ∀ (u : { x // x ∈ q }), ↑ψ u = ↑χ ↑u
w✝¹ : { x // x ∈ p }
w✝ : { x // x ∈ q }
right✝ : ∀ (r : { x // x ∈ p }) (s : { x // x ∈ q }), ↑r + ↑s = ↑w✝¹ + ↑w✝ → r = w✝¹ ∧ s = w✝
⊢ ↑(ofIsCompl h φ ψ) (↑w✝¹ + ↑w✝) = ↑χ (↑w✝¹ + ↑w✝)
[PROOFSTEP]
simp [ofIsCompl, hφ, hψ]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ₁ φ₂ : { x // x ∈ p } →ₗ[R] F
ψ₁ ψ₂ : { x // x ∈ q } →ₗ[R] F
⊢ ∀ (u : { x // x ∈ p }), ↑(φ₁ + φ₂) u = ↑(ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
φ₁ φ₂ : { x // x ∈ p } →ₗ[R] F
ψ₁ ψ₂ : { x // x ∈ q } →ₗ[R] F
⊢ ∀ (u : { x // x ∈ q }), ↑(ψ₁ + ψ₂) u = ↑(ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
inst✝¹⁴ : Ring R✝
E✝ : Type u_2
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module R✝ E✝
F✝ : Type u_3
inst✝¹¹ : AddCommGroup F✝
inst✝¹⁰ : Module R✝ F✝
G : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module R✝ G
p✝ q✝ : Submodule R✝ E✝
S : Type u_5
inst✝⁷ : Semiring S
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module S M
m : Submodule S M
R : Type u_7
inst✝⁴ : CommRing R
E : Type u_8
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_9
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
c : R
⊢ ∀ (u : { x // x ∈ p }), ↑(c • φ) u = ↑(c • ofIsCompl h φ ψ) ↑u
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u_1
inst✝¹⁴ : Ring R✝
E✝ : Type u_2
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module R✝ E✝
F✝ : Type u_3
inst✝¹¹ : AddCommGroup F✝
inst✝¹⁰ : Module R✝ F✝
G : Type u_4
inst✝⁹ : AddCommGroup G
inst✝⁸ : Module R✝ G
p✝ q✝ : Submodule R✝ E✝
S : Type u_5
inst✝⁷ : Semiring S
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module S M
m : Submodule S M
R : Type u_7
inst✝⁴ : CommRing R
E : Type u_8
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_9
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : { x // x ∈ p } →ₗ[R] F
ψ : { x // x ∈ q } →ₗ[R] F
c : R
⊢ ∀ (u : { x // x ∈ q }), ↑(c • ψ) u = ↑(c • ofIsCompl h φ ψ) ↑u
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
⊢ ∀ (x y : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
    (fun φ => ofIsCompl h φ.fst φ.snd) (x + y) =
      (fun φ => ofIsCompl h φ.fst φ.snd) x + (fun φ => ofIsCompl h φ.fst φ.snd) y
[PROOFSTEP]
intro φ ψ
[GOAL]
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ ψ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)
⊢ (fun φ => ofIsCompl h φ.fst φ.snd) (φ + ψ) =
    (fun φ => ofIsCompl h φ.fst φ.snd) φ + (fun φ => ofIsCompl h φ.fst φ.snd) ψ
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ ψ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)
⊢ ofIsCompl h (φ + ψ).fst (φ + ψ).snd = ofIsCompl h φ.fst φ.snd + ofIsCompl h ψ.fst ψ.snd
[PROOFSTEP]
rw [Prod.snd_add, Prod.fst_add, ofIsCompl_add]
[GOAL]
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
⊢ ∀ (r : R₁) (x : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
    AddHom.toFun
        { toFun := fun φ => ofIsCompl h φ.fst φ.snd,
          map_add' :=
            (_ :
              ∀ (φ ψ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                (fun φ => ofIsCompl h φ.fst φ.snd) (φ + ψ) =
                  (fun φ => ofIsCompl h φ.fst φ.snd) φ + (fun φ => ofIsCompl h φ.fst φ.snd) ψ) }
        (r • x) =
      ↑(RingHom.id R₁) r •
        AddHom.toFun
          { toFun := fun φ => ofIsCompl h φ.fst φ.snd,
            map_add' :=
              (_ :
                ∀ (φ ψ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                  (fun φ => ofIsCompl h φ.fst φ.snd) (φ + ψ) =
                    (fun φ => ofIsCompl h φ.fst φ.snd) φ + (fun φ => ofIsCompl h φ.fst φ.snd) ψ) }
          x
[PROOFSTEP]
intro c φ
[GOAL]
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
c : R₁
φ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)
⊢ AddHom.toFun
      { toFun := fun φ => ofIsCompl h φ.fst φ.snd,
        map_add' :=
          (_ :
            ∀ (φ ψ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
              (fun φ => ofIsCompl h φ.fst φ.snd) (φ + ψ) =
                (fun φ => ofIsCompl h φ.fst φ.snd) φ + (fun φ => ofIsCompl h φ.fst φ.snd) ψ) }
      (c • φ) =
    ↑(RingHom.id R₁) c •
      AddHom.toFun
        { toFun := fun φ => ofIsCompl h φ.fst φ.snd,
          map_add' :=
            (_ :
              ∀ (φ ψ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                (fun φ => ofIsCompl h φ.fst φ.snd) (φ + ψ) =
                  (fun φ => ofIsCompl h φ.fst φ.snd) φ + (fun φ => ofIsCompl h φ.fst φ.snd) ψ) }
        φ
[PROOFSTEP]
simp [Prod.smul_snd, Prod.smul_fst, ofIsCompl_smul]
[GOAL]
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
src✝ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F := ofIsComplProd h
φ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)
⊢ (fun φ => (domRestrict φ p, domRestrict φ q))
      (AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R₁) (x : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R₁) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        φ) =
    φ
[PROOFSTEP]
ext x
[GOAL]
case h₁.h
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
src✝ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F := ofIsComplProd h
φ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)
x : { x // x ∈ p }
⊢ ↑((fun φ => (domRestrict φ p, domRestrict φ q))
            (AddHom.toFun
              { toAddHom := src✝.toAddHom,
                  map_smul' :=
                    (_ :
                      ∀ (r : R₁) (x : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                        AddHom.toFun src✝.toAddHom (r • x) =
                          ↑(RingHom.id R₁) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
              φ)).fst
      x =
    ↑φ.fst x
[PROOFSTEP]
exact ofIsCompl_left_apply h x
[GOAL]
case h₂.h
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
src✝ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F := ofIsComplProd h
φ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)
x : { x // x ∈ q }
⊢ ↑((fun φ => (domRestrict φ p, domRestrict φ q))
            (AddHom.toFun
              { toAddHom := src✝.toAddHom,
                  map_smul' :=
                    (_ :
                      ∀ (r : R₁) (x : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                        AddHom.toFun src✝.toAddHom (r • x) =
                          ↑(RingHom.id R₁) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
              φ)).snd
      x =
    ↑φ.snd x
[PROOFSTEP]
exact ofIsCompl_right_apply h x
[GOAL]
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
src✝ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F := ofIsComplProd h
φ : E →ₗ[R₁] F
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R₁) (x : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R₁) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      ((fun φ => (domRestrict φ p, domRestrict φ q)) φ) =
    φ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
src✝ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F := ofIsComplProd h
φ : E →ₗ[R₁] F
x : E
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R₁) (x : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R₁) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ((fun φ => (domRestrict φ p, domRestrict φ q)) φ))
      x =
    ↑φ x
[PROOFSTEP]
obtain ⟨a, b, hab, _⟩ := existsUnique_add_of_isCompl h x
[GOAL]
case h.intro.intro.intro
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
src✝ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F := ofIsComplProd h
φ : E →ₗ[R₁] F
x : E
a : { x // x ∈ p }
b : { x // x ∈ q }
hab : ↑a + ↑b = x
right✝ : ∀ (r : { x // x ∈ p }) (s : { x // x ∈ q }), ↑r + ↑s = x → r = a ∧ s = b
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R₁) (x : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R₁) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ((fun φ => (domRestrict φ p, domRestrict φ q)) φ))
      x =
    ↑φ x
[PROOFSTEP]
rw [← hab]
[GOAL]
case h.intro.intro.intro
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
src✝ : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F) →ₗ[R₁] E →ₗ[R₁] F := ofIsComplProd h
φ : E →ₗ[R₁] F
x : E
a : { x // x ∈ p }
b : { x // x ∈ q }
hab : ↑a + ↑b = x
right✝ : ∀ (r : { x // x ∈ p }) (s : { x // x ∈ q }), ↑r + ↑s = x → r = a ∧ s = b
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R₁) (x : ({ x // x ∈ p } →ₗ[R₁] F) × ({ x // x ∈ q } →ₗ[R₁] F)),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R₁) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          ((fun φ => (domRestrict φ p, domRestrict φ q)) φ))
      (↑a + ↑b) =
    ↑φ (↑a + ↑b)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
⊢ linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f)) = f
[PROOFSTEP]
ext x
[GOAL]
case h.a
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) x) = ↑(↑f x)
[PROOFSTEP]
have : x ∈ p ⊔ (ker f) := by simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
⊢ x ∈ p ⊔ ker f
[PROOFSTEP]
simp only [(isCompl_of_proj hf).sup_eq_top, mem_top]
[GOAL]
case h.a
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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
this : x ∈ p ⊔ ker f
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) x) = ↑(↑f x)
[PROOFSTEP]
rcases mem_sup'.1 this with ⟨x, y, rfl⟩
[GOAL]
case h.a.intro.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
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 : { x // x ∈ p }
y : { x // x ∈ ker f }
this : ↑x + ↑y ∈ p ⊔ ker f
⊢ ↑(↑(linearProjOfIsCompl p (ker f) (_ : IsCompl p (ker f))) (↑x + ↑y)) = ↑(↑f (↑x + ↑y))
[PROOFSTEP]
simp [hf]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : range f = ⊤
hg : range g = ⊤
hfg : IsCompl (ker f) (ker g)
⊢ Function.Injective ↑(prod f g)
[PROOFSTEP]
simp [← ker_eq_bot, hfg.inf_eq_bot]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : range f = ⊤
hg : range g = ⊤
hfg : IsCompl (ker f) (ker g)
⊢ Function.Surjective ↑(prod f g)
[PROOFSTEP]
rw [← range_eq_top]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : range f = ⊤
hg : range g = ⊤
hfg : IsCompl (ker f) (ker g)
⊢ range (prod f g) = ⊤
[PROOFSTEP]
simp [range_prod_eq hfg.sup_eq_top, *]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q✝ : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
x✝ : { q // IsCompl p q }
q : Submodule R E
hq : IsCompl p q
⊢ (fun f => { val := ker ↑f, property := (_ : IsCompl p (ker ↑f)) })
      ((fun q =>
          { val := linearProjOfIsCompl p ↑q (_ : IsCompl p ↑q),
            property := (_ : ∀ (x : { x // x ∈ p }), ↑(linearProjOfIsCompl p ↑q (_ : IsCompl p ↑q)) ↑x = x) })
        { val := q, property := hq }) =
    { val := q, property := hq }
[PROOFSTEP]
simp only [linearProjOfIsCompl_ker, Subtype.coe_mk]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) ↔ comp f f = f
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) → comp f f = f
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : ∃ p, IsProj p f
⊢ comp f f = f
[PROOFSTEP]
obtain ⟨p, hp⟩ := h
[GOAL]
case mp.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
⊢ comp f f = f
[PROOFSTEP]
ext x
[GOAL]
case mp.intro.h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
x : M
⊢ ↑(comp f f) x = ↑f x
[PROOFSTEP]
rw [comp_apply]
[GOAL]
case mp.intro.h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
x : M
⊢ ↑f (↑f x) = ↑f x
[PROOFSTEP]
exact hp.map_id (f x) (hp.map_mem x)
[GOAL]
case mpr
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
⊢ comp f f = f → ∃ p, IsProj p f
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∃ p, IsProj p f
[PROOFSTEP]
use range f
[GOAL]
case h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ IsProj (range f) f
[PROOFSTEP]
constructor
[GOAL]
case h.map_mem
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∀ (x : M), ↑f x ∈ range f
[PROOFSTEP]
intro x
[GOAL]
case h.map_mem
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
⊢ ↑f x ∈ range f
[PROOFSTEP]
exact mem_range_self f x
[GOAL]
case h.map_id
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∀ (x : M), x ∈ range f → ↑f x = x
[PROOFSTEP]
intro x hx
[GOAL]
case h.map_id
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
hx : x ∈ range f
⊢ ↑f x = x
[PROOFSTEP]
obtain ⟨y, hy⟩ := mem_range.1 hx
[GOAL]
case h.map_id.intro
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
hx : x ∈ range f
y : M
hy : ↑f y = x
⊢ ↑f x = x
[PROOFSTEP]
rw [← hy, ← comp_apply, h]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : { x // x ∈ m }
⊢ ↑(codRestrict h) ↑x = x
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : { x // x ∈ m }
⊢ ↑(↑(codRestrict h) ↑x) = ↑x
[PROOFSTEP]
rw [codRestrict_apply]
[GOAL]
case a
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : IsProj m f
x : { x // x ∈ m }
⊢ ↑f ↑x = ↑x
[PROOFSTEP]
exact h.map_id x x.2
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p (ker f)
[PROOFSTEP]
rw [← codRestrict_ker]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p (ker (codRestrict ?m.444391))
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ IsProj ?m.444132 f
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ Submodule R E
[PROOFSTEP]
exact isCompl_of_proj h.codRestrict_apply_cod
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f))))
      (comp (prodMap id 0) ↑(LinearEquiv.symm (prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))))
[PROOFSTEP]
rw [← LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]
[GOAL]
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
⊢ comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f))) =
    comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0)
[PROOFSTEP]
ext x
[GOAL]
case hl.h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
x : { x // x ∈ p }
⊢ ↑(comp (comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (inl R { x // x ∈ p } { x // x ∈ ker f })) x =
    ↑(comp (comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
          (inl R { x // x ∈ p } { x // x ∈ ker f }))
      x
[PROOFSTEP]
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inl, coprod_apply, coeSubtype, _root_.map_zero, add_zero,
  h.map_id x x.2, prodMap_apply, id_apply]
[GOAL]
case hr.h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] E
h : IsProj p f
x : { x // x ∈ ker f }
⊢ ↑(comp (comp f ↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (inr R { x // x ∈ p } { x // x ∈ ker f })) x =
    ↑(comp (comp (↑(prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
          (inr R { x // x ∈ p } { x // x ∈ ker f }))
      x
[PROOFSTEP]
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, _root_.map_zero, coeSubtype, zero_add,
  map_coe_ker, prodMap_apply, zero_apply, add_zero]
[GOAL]
R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = ↑(LinearEquiv.conj (Submodule.prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0)
[PROOFSTEP]
rw [LinearEquiv.conj_apply]
[GOAL]
R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    comp (comp (↑(Submodule.prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f)))) (prodMap id 0))
      ↑(LinearEquiv.symm (Submodule.prodEquivOfIsCompl p (ker f) (_ : IsCompl p (ker f))))
[PROOFSTEP]
exact h.eq_conj_prod_map'