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 ⁡ 1 st ⁡ F R ∘ 2 nd ⁡ 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 → 1 st ⁡ F ∈ T
10 9 ad2antll ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ E ∧ F ∈ T × E → 1 st ⁡ F ∈ T
11 1 2 3 tendocl ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ E ∧ 1 st ⁡ F ∈ T → R ⁡ 1 st ⁡ F ∈ T
12 7 8 10 11 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ E ∧ F ∈ T × E → R ⁡ 1 st ⁡ F ∈ T
13 xp2nd ⊢ F ∈ T × E → 2 nd ⁡ F ∈ E
14 13 ad2antll ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ E ∧ F ∈ T × E → 2 nd ⁡ F ∈ E
15 1 3 tendococl ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ E ∧ 2 nd ⁡ F ∈ E → R ∘ 2 nd ⁡ F ∈ E
16 7 8 14 15 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ E ∧ F ∈ T × E → R ∘ 2 nd ⁡ F ∈ E
17 opelxpi ⊢ R ⁡ 1 st ⁡ F ∈ T ∧ R ∘ 2 nd ⁡ F ∈ E → R ⁡ 1 st ⁡ F R ∘ 2 nd ⁡ F ∈ T × E
18 12 16 17 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ E ∧ F ∈ T × E → R ⁡ 1 st ⁡ F R ∘ 2 nd ⁡ F ∈ T × E
19 6 18 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ R ∈ E ∧ F ∈ T × E → R · ˙ F ∈ T × E