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