This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ocsh

Description: The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion ocsh ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )

Proof

Step Hyp Ref Expression
1 ocval ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
2 ssrab2 ⊢ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ ℋ
3 1 2 eqsstrdi ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
4 ssel ⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ ) )
5 hi01 ⊢ ( 𝑦 ∈ ℋ → ( 0ℎ ·ih 𝑦 ) = 0 )
6 4 5 syl6 ⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → ( 0ℎ ·ih 𝑦 ) = 0 ) )
7 6 ralrimiv ⊢ ( 𝐴 ⊆ ℋ → ∀ 𝑦 ∈ 𝐴 ( 0ℎ ·ih 𝑦 ) = 0 )
8 ax-hv0cl ⊢ 0ℎ ∈ ℋ
9 7 8 jctil ⊢ ( 𝐴 ⊆ ℋ → ( 0ℎ ∈ ℋ ∧ ∀ 𝑦 ∈ 𝐴 ( 0ℎ ·ih 𝑦 ) = 0 ) )
10 ocel ⊢ ( 𝐴 ⊆ ℋ → ( 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 0ℎ ∈ ℋ ∧ ∀ 𝑦 ∈ 𝐴 ( 0ℎ ·ih 𝑦 ) = 0 ) ) )
11 9 10 mpbird ⊢ ( 𝐴 ⊆ ℋ → 0ℎ ∈ ( ⊥ ‘ 𝐴 ) )
12 3 11 jca ⊢ ( 𝐴 ⊆ ℋ → ( ( ⊥ ‘ 𝐴 ) ⊆ ℋ ∧ 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ) )
13 ssel2 ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℋ )
14 ax-his2 ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = ( ( 𝑥 ·ih 𝑧 ) + ( 𝑦 ·ih 𝑧 ) ) )
15 14 3expa ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = ( ( 𝑥 ·ih 𝑧 ) + ( 𝑦 ·ih 𝑧 ) ) )
16 oveq12 ⊢ ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ·ih 𝑧 ) + ( 𝑦 ·ih 𝑧 ) ) = ( 0 + 0 ) )
17 00id ⊢ ( 0 + 0 ) = 0
18 16 17 eqtrdi ⊢ ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ·ih 𝑧 ) + ( 𝑦 ·ih 𝑧 ) ) = 0 )
19 15 18 sylan9eq ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 )
20 19 ex ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
21 20 ancoms ⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
22 13 21 sylan ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
23 22 an32s ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
24 23 ralimdva ⊢ ( ( 𝐴 ⊆ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
25 24 imdistanda ⊢ ( 𝐴 ⊆ ℋ → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
26 hvaddcl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ )
27 26 anim1i ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
28 25 27 syl6 ⊢ ( 𝐴 ⊆ ℋ → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) → ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
29 ocel ⊢ ( 𝐴 ⊆ ℋ → ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ) ) )
30 ocel ⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
31 29 30 anbi12d ⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ) ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) ) )
32 an4 ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ) ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
33 r19.26 ⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ↔ ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) )
34 33 anbi2i ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
35 32 34 bitr4i ⊢ ( ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ) ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
36 31 35 bitrdi ⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) ) )
37 ocel ⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
38 28 36 37 3imtr4d ⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ) )
39 38 ralrimivv ⊢ ( 𝐴 ⊆ ℋ → ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) )
40 mul01 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 0 ) = 0 )
41 oveq2 ⊢ ( ( 𝑦 ·ih 𝑧 ) = 0 → ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = ( 𝑥 · 0 ) )
42 41 eqeq1d ⊢ ( ( 𝑦 ·ih 𝑧 ) = 0 → ( ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ↔ ( 𝑥 · 0 ) = 0 ) )
43 40 42 syl5ibrcom ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
44 43 ad2antrl ⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
45 ax-his3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) )
46 45 eqeq1d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ↔ ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
47 46 3expa ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ↔ ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
48 47 ancoms ⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ↔ ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
49 44 48 sylibrd ⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
50 13 49 sylan ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
51 50 an32s ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
52 51 ralimdva ⊢ ( ( 𝐴 ⊆ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 → ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
53 52 imdistanda ⊢ ( 𝐴 ⊆ ℋ → ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
54 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
55 54 anim1i ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
56 53 55 syl6 ⊢ ( 𝐴 ⊆ ℋ → ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
57 30 anbi2d ⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) ) )
58 anass ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
59 57 58 bitr4di ⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
60 ocel ⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
61 56 59 60 3imtr4d ⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ) )
62 61 ralrimivv ⊢ ( 𝐴 ⊆ ℋ → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) )
63 39 62 jca ⊢ ( 𝐴 ⊆ ℋ → ( ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ) )
64 issh2 ⊢ ( ( ⊥ ‘ 𝐴 ) ∈ Sℋ ↔ ( ( ( ⊥ ‘ 𝐴 ) ⊆ ℋ ∧ 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ) ) )
65 12 63 64 sylanbrc ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )