[STATEMENT]
lemma inj1_linear:
  fixes K V1 V2
  assumes h1: "vectorspace K V1" and h2: "vectorspace K V2"
  shows "linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
from h1 h2
[PROOF STATE]
proof (chain)
picking this:
vectorspace K V1
vectorspace K V2
[PROOF STEP]
have mod: "mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)"
[PROOF STATE]
proof (prove)
using this:
vectorspace K V1
vectorspace K V2

goal (1 subgoal):
 1. mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
by (unfold vectorspace_def, intro inj1_hom, auto)
[PROOF STATE]
proof (state)
this:
mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)

goal (1 subgoal):
 1. linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
from mod h1 h2
[PROOF STATE]
proof (chain)
picking this:
mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)
vectorspace K V1
vectorspace K V2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)
vectorspace K V1
vectorspace K V2

goal (1 subgoal):
 1. linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
by (unfold linear_map_def vectorspace_def , auto, intro direct_sum_is_module, auto)
[PROOF STATE]
proof (state)
this:
linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)

goal:
No subgoals!
[PROOF STEP]
qed