Step | Hyp | Ref
| Expression |
1 | | df-obs 19868 |
. . . . 5
⊢ OBasis =
(ℎ ∈ PreHil ↦
{𝑏 ∈ 𝒫
(Base‘ℎ) ∣
(∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})}) |
2 | 1 | dmmptss 5548 |
. . . 4
⊢ dom
OBasis ⊆ PreHil |
3 | | elfvdm 6130 |
. . . 4
⊢ (𝐵 ∈ (OBasis‘𝑊) → 𝑊 ∈ dom OBasis) |
4 | 2, 3 | sseldi 3566 |
. . 3
⊢ (𝐵 ∈ (OBasis‘𝑊) → 𝑊 ∈ PreHil) |
5 | | fveq2 6103 |
. . . . . . . . 9
⊢ (ℎ = 𝑊 → (Base‘ℎ) = (Base‘𝑊)) |
6 | | isobs.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . . . 8
⊢ (ℎ = 𝑊 → (Base‘ℎ) = 𝑉) |
8 | 7 | pweqd 4113 |
. . . . . . 7
⊢ (ℎ = 𝑊 → 𝒫 (Base‘ℎ) = 𝒫 𝑉) |
9 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑊 →
(·𝑖‘ℎ) =
(·𝑖‘𝑊)) |
10 | | isobs.h |
. . . . . . . . . . . 12
⊢ , =
(·𝑖‘𝑊) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑊 →
(·𝑖‘ℎ) = , ) |
12 | 11 | oveqd 6566 |
. . . . . . . . . 10
⊢ (ℎ = 𝑊 → (𝑥(·𝑖‘ℎ)𝑦) = (𝑥 , 𝑦)) |
13 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (ℎ = 𝑊 → (Scalar‘ℎ) = (Scalar‘𝑊)) |
14 | | isobs.f |
. . . . . . . . . . . . . 14
⊢ 𝐹 = (Scalar‘𝑊) |
15 | 13, 14 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑊 → (Scalar‘ℎ) = 𝐹) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑊 →
(1r‘(Scalar‘ℎ)) = (1r‘𝐹)) |
17 | | isobs.u |
. . . . . . . . . . . 12
⊢ 1 =
(1r‘𝐹) |
18 | 16, 17 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑊 →
(1r‘(Scalar‘ℎ)) = 1 ) |
19 | 15 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝑊 →
(0g‘(Scalar‘ℎ)) = (0g‘𝐹)) |
20 | | isobs.z |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝐹) |
21 | 19, 20 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑊 →
(0g‘(Scalar‘ℎ)) = 0 ) |
22 | 18, 21 | ifeq12d 4056 |
. . . . . . . . . 10
⊢ (ℎ = 𝑊 → if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) = if(𝑥 = 𝑦, 1 , 0 )) |
23 | 12, 22 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (ℎ = 𝑊 → ((𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ↔ (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ))) |
24 | 23 | 2ralbidv 2972 |
. . . . . . . 8
⊢ (ℎ = 𝑊 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ↔ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ))) |
25 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑊 → (ocv‘ℎ) = (ocv‘𝑊)) |
26 | | isobs.o |
. . . . . . . . . . 11
⊢ ⊥ =
(ocv‘𝑊) |
27 | 25, 26 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (ℎ = 𝑊 → (ocv‘ℎ) = ⊥ ) |
28 | 27 | fveq1d 6105 |
. . . . . . . . 9
⊢ (ℎ = 𝑊 → ((ocv‘ℎ)‘𝑏) = ( ⊥ ‘𝑏)) |
29 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (ℎ = 𝑊 → (0g‘ℎ) = (0g‘𝑊)) |
30 | | isobs.y |
. . . . . . . . . . 11
⊢ 𝑌 = (0g‘𝑊) |
31 | 29, 30 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (ℎ = 𝑊 → (0g‘ℎ) = 𝑌) |
32 | 31 | sneqd 4137 |
. . . . . . . . 9
⊢ (ℎ = 𝑊 → {(0g‘ℎ)} = {𝑌}) |
33 | 28, 32 | eqeq12d 2625 |
. . . . . . . 8
⊢ (ℎ = 𝑊 → (((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)} ↔ ( ⊥ ‘𝑏) = {𝑌})) |
34 | 24, 33 | anbi12d 743 |
. . . . . . 7
⊢ (ℎ = 𝑊 → ((∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)}) ↔ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥ ‘𝑏) = {𝑌}))) |
35 | 8, 34 | rabeqbidv 3168 |
. . . . . 6
⊢ (ℎ = 𝑊 → {𝑏 ∈ 𝒫 (Base‘ℎ) ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥(·𝑖‘ℎ)𝑦) = if(𝑥 = 𝑦, (1r‘(Scalar‘ℎ)),
(0g‘(Scalar‘ℎ))) ∧ ((ocv‘ℎ)‘𝑏) = {(0g‘ℎ)})} = {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥ ‘𝑏) = {𝑌})}) |
36 | | fvex 6113 |
. . . . . . . . 9
⊢
(Base‘𝑊)
∈ V |
37 | 6, 36 | eqeltri 2684 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
38 | 37 | pwex 4774 |
. . . . . . 7
⊢ 𝒫
𝑉 ∈ V |
39 | 38 | rabex 4740 |
. . . . . 6
⊢ {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝑏) = {𝑌})} ∈ V |
40 | 35, 1, 39 | fvmpt 6191 |
. . . . 5
⊢ (𝑊 ∈ PreHil →
(OBasis‘𝑊) = {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝑏) = {𝑌})}) |
41 | 40 | eleq2d 2673 |
. . . 4
⊢ (𝑊 ∈ PreHil → (𝐵 ∈ (OBasis‘𝑊) ↔ 𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝑏) = {𝑌})})) |
42 | | raleq 3115 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ↔ ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ))) |
43 | 42 | raleqbi1dv 3123 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ))) |
44 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → ( ⊥ ‘𝑏) = ( ⊥ ‘𝐵)) |
45 | 44 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (( ⊥ ‘𝑏) = {𝑌} ↔ ( ⊥ ‘𝐵) = {𝑌})) |
46 | 43, 45 | anbi12d 743 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝑏) = {𝑌}) ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌}))) |
47 | 46 | elrab 3331 |
. . . . 5
⊢ (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝑏) = {𝑌})} ↔ (𝐵 ∈ 𝒫 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌}))) |
48 | 37 | elpw2 4755 |
. . . . . 6
⊢ (𝐵 ∈ 𝒫 𝑉 ↔ 𝐵 ⊆ 𝑉) |
49 | 48 | anbi1i 727 |
. . . . 5
⊢ ((𝐵 ∈ 𝒫 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌})) ↔ (𝐵 ⊆ 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌}))) |
50 | 47, 49 | bitri 263 |
. . . 4
⊢ (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝑏) = {𝑌})} ↔ (𝐵 ⊆ 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌}))) |
51 | 41, 50 | syl6bb 275 |
. . 3
⊢ (𝑊 ∈ PreHil → (𝐵 ∈ (OBasis‘𝑊) ↔ (𝐵 ⊆ 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌})))) |
52 | 4, 51 | biadan2 672 |
. 2
⊢ (𝐵 ∈ (OBasis‘𝑊) ↔ (𝑊 ∈ PreHil ∧ (𝐵 ⊆ 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌})))) |
53 | | 3anass 1035 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝐵 ⊆ 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌})) ↔ (𝑊 ∈ PreHil ∧ (𝐵 ⊆ 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌})))) |
54 | 52, 53 | bitr4i 266 |
1
⊢ (𝐵 ∈ (OBasis‘𝑊) ↔ (𝑊 ∈ PreHil ∧ 𝐵 ⊆ 𝑉 ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 , 𝑦) = if(𝑥 = 𝑦, 1 , 0 ) ∧ ( ⊥
‘𝐵) = {𝑌}))) |