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	ralrimivw	⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∈ ℋ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 ) )
3		ss2rab	⊢ ( { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } ↔ ∀ 𝑥 ∈ ℋ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 ) )
4	2 3	sylibr	⊢ ( 𝐴 ⊆ 𝐵 → { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
5	4	adantl	⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
6		ocval	⊢ ( 𝐵 ⊆ ℋ → ( ⊥ ‘ 𝐵 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } )
7	6	ad2antlr	⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐵 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ·ih 𝑦 ) = 0 } )
8		ocval	⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
9	8	ad2antrr	⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐴 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
10	5 7 9	3sstr4d	⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) ∧ 𝐴 ⊆ 𝐵 ) → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) )
11	10	ex	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ⊆ 𝐵 → ( ⊥ ‘ 𝐵 ) ⊆ ( ⊥ ‘ 𝐴 ) ) )