Metamath Proof Explorer

Definition df-djh

Description: Define (closed) subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014)

Ref Expression
Assertion df-djh ⊢ joinH = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w , y ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ x ∩ ocH ⁡ k ⁡ w ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdjh class joinH
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 cbs class Base
9 cdvh class DVecH
10 5 9 cfv class DVecH ⁡ k
11 3 cv setvar w
12 11 10 cfv class DVecH ⁡ k ⁡ w
13 12 8 cfv class Base DVecH ⁡ k ⁡ w
14 13 cpw class 𝒫 Base DVecH ⁡ k ⁡ w
15 vy setvar y
16 coch class ocH
17 5 16 cfv class ocH ⁡ k
18 11 17 cfv class ocH ⁡ k ⁡ w
19 7 cv setvar x
20 19 18 cfv class ocH ⁡ k ⁡ w ⁡ x
21 15 cv setvar y
22 21 18 cfv class ocH ⁡ k ⁡ w ⁡ y
23 20 22 cin class ocH ⁡ k ⁡ w ⁡ x ∩ ocH ⁡ k ⁡ w ⁡ y
24 23 18 cfv class ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ x ∩ ocH ⁡ k ⁡ w ⁡ y
25 7 15 14 14 24 cmpo class x ∈ 𝒫 Base DVecH ⁡ k ⁡ w , y ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ x ∩ ocH ⁡ k ⁡ w ⁡ y
26 3 6 25 cmpt class w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w , y ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ x ∩ ocH ⁡ k ⁡ w ⁡ y
27 1 2 26 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w , y ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ x ∩ ocH ⁡ k ⁡ w ⁡ y
28 0 27 wceq wff joinH = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ 𝒫 Base DVecH ⁡ k ⁡ w , y ∈ 𝒫 Base DVecH ⁡ k ⁡ w ⟼ ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ x ∩ ocH ⁡ k ⁡ w ⁡ y