Definition df-dveca

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

	Ref	Expression
Assertion	df-dveca	⊢ DVecA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( { ⟨ ( Base ‘ ndx ) , ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) , 𝑔 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑓 ∘ 𝑔 ) ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑠 ∈ ( ( TEndo ‘ 𝑘 ) ‘ 𝑤 ) , 𝑓 ∈ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( 𝑠 ‘ 𝑓 ) ) ⟩ } ) ) )

Detailed syntax breakdown

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