Metamath Proof Explorer

Theorem occon

Description: Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion occon ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ B → ⊥ ⁡ B ⊆ ⊥ ⁡ A

Proof

Step Hyp Ref Expression
1 ssralv ⊢ A ⊆ B → ∀ y ∈ B x ⋅ ih y = 0 → ∀ y ∈ A x ⋅ ih y = 0
2 1 adantr ⊢ A ⊆ B ∧ x ∈ ℋ → ∀ y ∈ B x ⋅ ih y = 0 → ∀ y ∈ A x ⋅ ih y = 0
3 2 ss2rabdv ⊢ A ⊆ B → x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0 ⊆ x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0
4 3 adantl ⊢ A ⊆ ℋ ∧ B ⊆ ℋ ∧ A ⊆ B → x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0 ⊆ x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0
5 ocval ⊢ B ⊆ ℋ → ⊥ ⁡ B = x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0
6 5 ad2antlr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ ∧ A ⊆ B → ⊥ ⁡ B = x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0
7 ocval ⊢ A ⊆ ℋ → ⊥ ⁡ A = x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0
8 7 ad2antrr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ ∧ A ⊆ B → ⊥ ⁡ A = x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0
9 4 6 8 3sstr4d ⊢ A ⊆ ℋ ∧ B ⊆ ℋ ∧ A ⊆ B → ⊥ ⁡ B ⊆ ⊥ ⁡ A
10 9 ex ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ B → ⊥ ⁡ B ⊆ ⊥ ⁡ A