Metamath Proof Explorer

Theorem dvhvscacl

Description: Closure of the scalar product operation for the constructed full vector space H. (Contributed by NM, 12-Feb-2014)

Ref Expression
Hypotheses dvhfvsca.h ⊢H=LHyp⁡K
dvhfvsca.t ⊢T=LTrn⁡K⁡W
dvhfvsca.e ⊢E=TEndo⁡K⁡W
dvhfvsca.u ⊢U=DVecH⁡K⁡W
dvhfvsca.s ⊢·˙=⋅U
Assertion dvhvscacl ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→R·˙F∈T×E

Proof

Step Hyp Ref Expression
1 dvhfvsca.h ⊢H=LHyp⁡K
2 dvhfvsca.t ⊢T=LTrn⁡K⁡W
3 dvhfvsca.e ⊢E=TEndo⁡K⁡W
4 dvhfvsca.u ⊢U=DVecH⁡K⁡W
5 dvhfvsca.s ⊢·˙=⋅U
6 1 2 3 4 5 dvhvsca ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→R·˙F=R⁡1st⁡FR∘2nd⁡F
7 simpl ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→K∈HL∧W∈H
8 simprl ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→R∈E
9 xp1st ⊢F∈T×E→1st⁡F∈T
10 9 ad2antll ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→1st⁡F∈T
11 1 2 3 tendocl ⊢K∈HL∧W∈H∧R∈E∧1st⁡F∈T→R⁡1st⁡F∈T
12 7 8 10 11 syl3anc ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→R⁡1st⁡F∈T
13 xp2nd ⊢F∈T×E→2nd⁡F∈E
14 13 ad2antll ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→2nd⁡F∈E
15 1 3 tendococl ⊢K∈HL∧W∈H∧R∈E∧2nd⁡F∈E→R∘2nd⁡F∈E
16 7 8 14 15 syl3anc ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→R∘2nd⁡F∈E
17 opelxpi ⊢R⁡1st⁡F∈T∧R∘2nd⁡F∈E→R⁡1st⁡FR∘2nd⁡F∈T×E
18 12 16 17 syl2anc ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→R⁡1st⁡FR∘2nd⁡F∈T×E
19 6 18 eqeltrd ⊢K∈HL∧W∈H∧R∈E∧F∈T×E→R·˙F∈T×E