Metamath Proof Explorer

Theorem dvhvaddcl

Description: Closure of the vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses dvhvaddcl.h ⊢H=LHyp⁡K
dvhvaddcl.t ⊢T=LTrn⁡K⁡W
dvhvaddcl.e ⊢E=TEndo⁡K⁡W
dvhvaddcl.u ⊢U=DVecH⁡K⁡W
dvhvaddcl.d ⊢D=Scalar⁡U
dvhvaddcl.p ⊢⨣˙=+D
dvhvaddcl.a ⊢+˙=+U
Assertion dvhvaddcl ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→F+˙G∈T×E

Proof

Step Hyp Ref Expression
1 dvhvaddcl.h ⊢H=LHyp⁡K
2 dvhvaddcl.t ⊢T=LTrn⁡K⁡W
3 dvhvaddcl.e ⊢E=TEndo⁡K⁡W
4 dvhvaddcl.u ⊢U=DVecH⁡K⁡W
5 dvhvaddcl.d ⊢D=Scalar⁡U
6 dvhvaddcl.p ⊢⨣˙=+D
7 dvhvaddcl.a ⊢+˙=+U
8 1 2 3 4 5 7 6 dvhvadd ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→F+˙G=1st⁡F∘1st⁡G2nd⁡F⨣˙2nd⁡G
9 simpl ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→K∈HL∧W∈H
10 xp1st ⊢F∈T×E→1st⁡F∈T
11 10 ad2antrl ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→1st⁡F∈T
12 xp1st ⊢G∈T×E→1st⁡G∈T
13 12 ad2antll ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→1st⁡G∈T
14 1 2 ltrnco ⊢K∈HL∧W∈H∧1st⁡F∈T∧1st⁡G∈T→1st⁡F∘1st⁡G∈T
15 9 11 13 14 syl3anc ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→1st⁡F∘1st⁡G∈T
16 eqid ⊢a∈E,b∈E⟼c∈T⟼a⁡c∘b⁡c=a∈E,b∈E⟼c∈T⟼a⁡c∘b⁡c
17 1 2 3 4 5 16 6 dvhfplusr ⊢K∈HL∧W∈H→⨣˙=a∈E,b∈E⟼c∈T⟼a⁡c∘b⁡c
18 17 adantr ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→⨣˙=a∈E,b∈E⟼c∈T⟼a⁡c∘b⁡c
19 18 oveqd ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→2nd⁡F⨣˙2nd⁡G=2nd⁡Fa∈E,b∈E⟼c∈T⟼a⁡c∘b⁡c2nd⁡G
20 xp2nd ⊢F∈T×E→2nd⁡F∈E
21 20 ad2antrl ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→2nd⁡F∈E
22 xp2nd ⊢G∈T×E→2nd⁡G∈E
23 22 ad2antll ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→2nd⁡G∈E
24 1 2 3 16 tendoplcl ⊢K∈HL∧W∈H∧2nd⁡F∈E∧2nd⁡G∈E→2nd⁡Fa∈E,b∈E⟼c∈T⟼a⁡c∘b⁡c2nd⁡G∈E
25 9 21 23 24 syl3anc ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→2nd⁡Fa∈E,b∈E⟼c∈T⟼a⁡c∘b⁡c2nd⁡G∈E
26 19 25 eqeltrd ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→2nd⁡F⨣˙2nd⁡G∈E
27 opelxpi ⊢1st⁡F∘1st⁡G∈T∧2nd⁡F⨣˙2nd⁡G∈E→1st⁡F∘1st⁡G2nd⁡F⨣˙2nd⁡G∈T×E
28 15 26 27 syl2anc ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→1st⁡F∘1st⁡G2nd⁡F⨣˙2nd⁡G∈T×E
29 8 28 eqeltrd ⊢K∈HL∧W∈H∧F∈T×E∧G∈T×E→F+˙G∈T×E