Detailed syntax breakdown of Definition df-obs
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cobs 21722 | . 2
class
OBasis | 
| 2 |  | vh | . . 3
setvar ℎ | 
| 3 |  | cphl 21642 | . . 3
class
PreHil | 
| 4 |  | vx | . . . . . . . . . 10
setvar 𝑥 | 
| 5 | 4 | cv 1539 | . . . . . . . . 9
class 𝑥 | 
| 6 |  | vy | . . . . . . . . . 10
setvar 𝑦 | 
| 7 | 6 | cv 1539 | . . . . . . . . 9
class 𝑦 | 
| 8 | 2 | cv 1539 | . . . . . . . . . 10
class ℎ | 
| 9 |  | cip 17302 | . . . . . . . . . 10
class
·𝑖 | 
| 10 | 8, 9 | cfv 6561 | . . . . . . . . 9
class
(·𝑖‘ℎ) | 
| 11 | 5, 7, 10 | co 7431 | . . . . . . . 8
class (𝑥(·𝑖‘ℎ)𝑦) | 
| 12 | 4, 6 | weq 1962 | . . . . . . . . 9
wff 𝑥 = 𝑦 | 
| 13 |  | csca 17300 | . . . . . . . . . . 11
class
Scalar | 
| 14 | 8, 13 | cfv 6561 | . . . . . . . . . 10
class
(Scalar‘ℎ) | 
| 15 |  | cur 20178 | . . . . . . . . . 10
class
1r | 
| 16 | 14, 15 | cfv 6561 | . . . . . . . . 9
class
(1r‘(Scalar‘ℎ)) | 
| 17 |  | c0g 17484 | . . . . . . . . . 10
class
0g | 
| 18 | 14, 17 | cfv 6561 | . . . . . . . . 9
class
(0g‘(Scalar‘ℎ)) | 
| 19 | 12, 16, 18 | cif 4525 | . . . . . . . 8
class if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) | 
| 20 | 11, 19 | wceq 1540 | . . . . . . 7
wff (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) | 
| 21 |  | vb | . . . . . . . 8
setvar 𝑏 | 
| 22 | 21 | cv 1539 | . . . . . . 7
class 𝑏 | 
| 23 | 20, 6, 22 | wral 3061 | . . . . . 6
wff
∀𝑦 ∈
𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) | 
| 24 | 23, 4, 22 | wral 3061 | . . . . 5
wff
∀𝑥 ∈
𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) | 
| 25 |  | cocv 21678 | . . . . . . . 8
class
ocv | 
| 26 | 8, 25 | cfv 6561 | . . . . . . 7
class
(ocv‘ℎ) | 
| 27 | 22, 26 | cfv 6561 | . . . . . 6
class
((ocv‘ℎ)‘𝑏) | 
| 28 | 8, 17 | cfv 6561 | . . . . . . 7
class
(0g‘ℎ) | 
| 29 | 28 | csn 4626 | . . . . . 6
class
{(0g‘ℎ)} | 
| 30 | 27, 29 | wceq 1540 | . . . . 5
wff
((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)} | 
| 31 | 24, 30 | wa 395 | . . . 4
wff
(∀𝑥 ∈
𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)}) | 
| 32 |  | cbs 17247 | . . . . . 6
class
Base | 
| 33 | 8, 32 | cfv 6561 | . . . . 5
class
(Base‘ℎ) | 
| 34 | 33 | cpw 4600 | . . . 4
class 𝒫
(Base‘ℎ) | 
| 35 | 31, 21, 34 | crab 3436 | . . 3
class {𝑏 ∈ 𝒫
(Base‘ℎ) ∣
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})} | 
| 36 | 2, 3, 35 | cmpt 5225 | . 2
class (ℎ ∈ PreHil ↦ {𝑏 ∈ 𝒫
(Base‘ℎ) ∣
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}) | 
| 37 | 1, 36 | wceq 1540 | 1
wff OBasis =
(ℎ ∈ PreHil ↦
{𝑏 ∈ 𝒫
(Base‘ℎ) ∣
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}) |