Metamath Proof Explorer

Definition df-djaN

Description: Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013)

Ref Expression
Assertion df-djaN ⊢ vA = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w , y ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdjaN class vA
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 vx setvar x
8 cltrn class LTrn
9 5 8 cfv class LTrn ⁡ k
10 3 cv setvar w
11 10 9 cfv class LTrn ⁡ k ⁡ w
12 11 cpw class 𝒫 LTrn ⁡ k ⁡ w
13 vy setvar y
14 cocaN class ocA
15 5 14 cfv class ocA ⁡ k
16 10 15 cfv class ocA ⁡ k ⁡ w
17 7 cv setvar x
18 17 16 cfv class ocA ⁡ k ⁡ w ⁡ x
19 13 cv setvar y
20 19 16 cfv class ocA ⁡ k ⁡ w ⁡ y
21 18 20 cin class ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y
22 21 16 cfv class ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y
23 7 13 12 12 22 cmpo class x ∈ 𝒫 LTrn ⁡ k ⁡ w , y ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y
24 3 6 23 cmpt class w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w , y ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y
25 1 2 24 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w , y ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y
26 0 25 wceq wff vA = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 LTrn ⁡ k ⁡ w , y ∈ 𝒫 LTrn ⁡ k ⁡ w ⟼ ocA ⁡ k ⁡ w ⁡ ocA ⁡ k ⁡ w ⁡ x ∩ ocA ⁡ k ⁡ w ⁡ y