Definition df-docaN

Description: Define subspace orthocomplement for DVecA partial vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 6-Dec-2013)

	Ref	Expression
Assertion	df-docaN	⊢ ocA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cocaN	⊢ ocA
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		vx	⊢ 𝑥
8		cltrn	⊢ LTrn
9	5 8	cfv	⊢ ( LTrn ‘ 𝑘 )
10	3	cv	⊢ 𝑤
11	10 9	cfv	⊢ ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
12	11	cpw	⊢ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 )
13		cdia	⊢ DIsoA
14	5 13	cfv	⊢ ( DIsoA ‘ 𝑘 )
15	10 14	cfv	⊢ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 )
16		coc	⊢ oc
17	5 16	cfv	⊢ ( oc ‘ 𝑘 )
18	15	ccnv	⊢ ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 )
19		vz	⊢ 𝑧
20	15	crn	⊢ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 )
21	7	cv	⊢ 𝑥
22	19	cv	⊢ 𝑧
23	21 22	wss	⊢ 𝑥 ⊆ 𝑧
24	23 19 20	crab	⊢ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 }
25	24	cint	⊢ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 }
26	25 18	cfv	⊢ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } )
27	26 17	cfv	⊢ ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) )
28		cjn	⊢ join
29	5 28	cfv	⊢ ( join ‘ 𝑘 )
30	10 17	cfv	⊢ ( ( oc ‘ 𝑘 ) ‘ 𝑤 )
31	27 30 29	co	⊢ ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) )
32		cmee	⊢ meet
33	5 32	cfv	⊢ ( meet ‘ 𝑘 )
34	31 10 33	co	⊢ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 )
35	34 15	cfv	⊢ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) )
36	7 12 35	cmpt	⊢ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) )
37	3 6 36	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) )
38	1 2 37	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )
39	0 38	wceq	⊢ ocA = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ 𝒫 ( ( LTrn ‘ 𝑘 ) ‘ 𝑤 ) ↦ ( ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ( oc ‘ 𝑘 ) ‘ ( ◡ ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ‘ ∩ { 𝑧 ∈ ran ( ( DIsoA ‘ 𝑘 ) ‘ 𝑤 ) ∣ 𝑥 ⊆ 𝑧 } ) ) ( join ‘ 𝑘 ) ( ( oc ‘ 𝑘 ) ‘ 𝑤 ) ) ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )