Metamath Proof Explorer

Definition df-dveca

Description: Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013)

Ref Expression
Assertion df-dveca ⊢ DVecA = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ Base ndx LTrn ⁡ k ⁡ w + ndx f ∈ LTrn ⁡ k ⁡ w , g ∈ LTrn ⁡ k ⁡ w ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ k ⁡ w ∪ ⋅ ndx s ∈ TEndo ⁡ k ⁡ w , f ∈ LTrn ⁡ k ⁡ w ⟼ s ⁡ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdveca class DVecA
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 cbs class Base
8 cnx class ndx
9 8 7 cfv class Base ndx
10 cltrn class LTrn
11 5 10 cfv class LTrn ⁡ k
12 3 cv setvar w
13 12 11 cfv class LTrn ⁡ k ⁡ w
14 9 13 cop class Base ndx LTrn ⁡ k ⁡ w
15 cplusg class + 𝑔
16 8 15 cfv class + ndx
17 vf setvar f
18 vg setvar g
19 17 cv setvar f
20 18 cv setvar g
21 19 20 ccom class f ∘ g
22 17 18 13 13 21 cmpo class f ∈ LTrn ⁡ k ⁡ w , g ∈ LTrn ⁡ k ⁡ w ⟼ f ∘ g
23 16 22 cop class + ndx f ∈ LTrn ⁡ k ⁡ w , g ∈ LTrn ⁡ k ⁡ w ⟼ f ∘ g
24 csca class Scalar
25 8 24 cfv class Scalar ⁡ ndx
26 cedring class EDRing
27 5 26 cfv class EDRing ⁡ k
28 12 27 cfv class EDRing ⁡ k ⁡ w
29 25 28 cop class Scalar ⁡ ndx EDRing ⁡ k ⁡ w
30 14 23 29 ctp class Base ndx LTrn ⁡ k ⁡ w + ndx f ∈ LTrn ⁡ k ⁡ w , g ∈ LTrn ⁡ k ⁡ w ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ k ⁡ w
31 cvsca class ⋅ 𝑠
32 8 31 cfv class ⋅ ndx
33 vs setvar s
34 ctendo class TEndo
35 5 34 cfv class TEndo ⁡ k
36 12 35 cfv class TEndo ⁡ k ⁡ w
37 33 cv setvar s
38 19 37 cfv class s ⁡ f
39 33 17 36 13 38 cmpo class s ∈ TEndo ⁡ k ⁡ w , f ∈ LTrn ⁡ k ⁡ w ⟼ s ⁡ f
40 32 39 cop class ⋅ ndx s ∈ TEndo ⁡ k ⁡ w , f ∈ LTrn ⁡ k ⁡ w ⟼ s ⁡ f
41 40 csn class ⋅ ndx s ∈ TEndo ⁡ k ⁡ w , f ∈ LTrn ⁡ k ⁡ w ⟼ s ⁡ f
42 30 41 cun class Base ndx LTrn ⁡ k ⁡ w + ndx f ∈ LTrn ⁡ k ⁡ w , g ∈ LTrn ⁡ k ⁡ w ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ k ⁡ w ∪ ⋅ ndx s ∈ TEndo ⁡ k ⁡ w , f ∈ LTrn ⁡ k ⁡ w ⟼ s ⁡ f
43 3 6 42 cmpt class w ∈ LHyp ⁡ k ⟼ Base ndx LTrn ⁡ k ⁡ w + ndx f ∈ LTrn ⁡ k ⁡ w , g ∈ LTrn ⁡ k ⁡ w ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ k ⁡ w ∪ ⋅ ndx s ∈ TEndo ⁡ k ⁡ w , f ∈ LTrn ⁡ k ⁡ w ⟼ s ⁡ f
44 1 2 43 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ Base ndx LTrn ⁡ k ⁡ w + ndx f ∈ LTrn ⁡ k ⁡ w , g ∈ LTrn ⁡ k ⁡ w ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ k ⁡ w ∪ ⋅ ndx s ∈ TEndo ⁡ k ⁡ w , f ∈ LTrn ⁡ k ⁡ w ⟼ s ⁡ f
45 0 44 wceq wff DVecA = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ Base ndx LTrn ⁡ k ⁡ w + ndx f ∈ LTrn ⁡ k ⁡ w , g ∈ LTrn ⁡ k ⁡ w ⟼ f ∘ g Scalar ⁡ ndx EDRing ⁡ k ⁡ w ∪ ⋅ ndx s ∈ TEndo ⁡ k ⁡ w , f ∈ LTrn ⁡ k ⁡ w ⟼ s ⁡ f