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 ralrimivw ⊢ A ⊆ B → ∀ x ∈ ℋ ∀ y ∈ B x ⋅ ih y = 0 → ∀ y ∈ A x ⋅ ih y = 0
3 ss2rab ⊢ x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0 ⊆ x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0 ↔ ∀ x ∈ ℋ ∀ y ∈ B x ⋅ ih y = 0 → ∀ y ∈ A x ⋅ ih y = 0
4 2 3 sylibr ⊢ A ⊆ B → x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0 ⊆ x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0
5 4 adantl ⊢ A ⊆ ℋ ∧ B ⊆ ℋ ∧ A ⊆ B → x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0 ⊆ x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0
6 ocval ⊢ B ⊆ ℋ → ⊥ ⁡ B = x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0
7 6 ad2antlr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ ∧ A ⊆ B → ⊥ ⁡ B = x ∈ ℋ | ∀ y ∈ B x ⋅ ih y = 0
8 ocval ⊢ A ⊆ ℋ → ⊥ ⁡ A = x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0
9 8 ad2antrr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ ∧ A ⊆ B → ⊥ ⁡ A = x ∈ ℋ | ∀ y ∈ A x ⋅ ih y = 0
10 5 7 9 3sstr4d ⊢ A ⊆ ℋ ∧ B ⊆ ℋ ∧ A ⊆ B → ⊥ ⁡ B ⊆ ⊥ ⁡ A
11 10 ex ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ B → ⊥ ⁡ B ⊆ ⊥ ⁡ A