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