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

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 ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ssralv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 ) )
2 1 adantr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 ) )
3 2 ss2rabdv ⊢ ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
4 3 adantl ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
5 ocval ⊢ ( 𝐵 ⊆ ℋ → ( ⊥ ‘ 𝐵 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } )
6 5 ad2antlr ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐵 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } )
7 ocval ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
8 7 ad2antrr ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐴 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
9 4 6 8 3sstr4d ⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) )
10 9 ex ⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) )