Step |
Hyp |
Ref |
Expression |
1 |
|
ocvss.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
ocvss.o |
⊢ ⊥ = ( ocv ‘ 𝑊 ) |
3 |
1 2
|
ocvss |
⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 |
4 |
3
|
a1i |
⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ) |
5 |
|
simpr |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 ) |
6 |
5
|
sselda |
⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑉 ) |
7 |
|
eqid |
⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 ) |
8 |
|
eqid |
⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) |
9 |
|
eqid |
⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) |
10 |
1 7 8 9 2
|
ocvi |
⊢ ( ( 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) |
11 |
10
|
ancoms |
⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) |
12 |
11
|
adantll |
⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) |
13 |
|
simplll |
⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → 𝑊 ∈ PreHil ) |
14 |
4
|
sselda |
⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → 𝑦 ∈ 𝑉 ) |
15 |
6
|
adantr |
⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → 𝑥 ∈ 𝑉 ) |
16 |
8 7 1 9
|
iporthcom |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
17 |
13 14 15 16
|
syl3anc |
⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → ( ( 𝑦 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
18 |
12 17
|
mpbid |
⊢ ( ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ) → ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) |
19 |
18
|
ralrimiva |
⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) |
20 |
1 7 8 9 2
|
elocv |
⊢ ( 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ↔ ( ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ ∀ 𝑦 ∈ ( ⊥ ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
21 |
4 6 19 20
|
syl3anbrc |
⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) |
22 |
21
|
ex |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) ) |
23 |
22
|
ssrdv |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) |