Theorem h1dei

Description: Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypothesis	h1deot.1	⊢ 𝐵 ∈ ℋ
Assertion	h1dei	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐴 ·ih 𝑥 ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		h1deot.1	⊢ 𝐵 ∈ ℋ
2		snssi	⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
3		occl	⊢ ( { 𝐵 } ⊆ ℋ → ( ⊥ ‘ { 𝐵 } ) ∈ Cℋ )
4	1 2 3	mp2b	⊢ ( ⊥ ‘ { 𝐵 } ) ∈ Cℋ
5	4	chssii	⊢ ( ⊥ ‘ { 𝐵 } ) ⊆ ℋ
6		ocel	⊢ ( ( ⊥ ‘ { 𝐵 } ) ⊆ ℋ → ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ ( ⊥ ‘ { 𝐵 } ) ( 𝐴 ·ih 𝑥 ) = 0 ) ) )
7	5 6	ax-mp	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ ( ⊥ ‘ { 𝐵 } ) ( 𝐴 ·ih 𝑥 ) = 0 ) )
8	1	h1deoi	⊢ ( 𝑥 ∈ ( ⊥ ‘ { 𝐵 } ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝑥 ·ih 𝐵 ) = 0 ) )
9		orthcom	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝑥 ·ih 𝐵 ) = 0 ↔ ( 𝐵 ·ih 𝑥 ) = 0 ) )
10	1 9	mpan2	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑥 ·ih 𝐵 ) = 0 ↔ ( 𝐵 ·ih 𝑥 ) = 0 ) )
11	10	pm5.32i	⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑥 ·ih 𝐵 ) = 0 ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝐵 ·ih 𝑥 ) = 0 ) )
12	8 11	bitri	⊢ ( 𝑥 ∈ ( ⊥ ‘ { 𝐵 } ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝐵 ·ih 𝑥 ) = 0 ) )
13	12	imbi1i	⊢ ( ( 𝑥 ∈ ( ⊥ ‘ { 𝐵 } ) → ( 𝐴 ·ih 𝑥 ) = 0 ) ↔ ( ( 𝑥 ∈ ℋ ∧ ( 𝐵 ·ih 𝑥 ) = 0 ) → ( 𝐴 ·ih 𝑥 ) = 0 ) )
14		impexp	⊢ ( ( ( 𝑥 ∈ ℋ ∧ ( 𝐵 ·ih 𝑥 ) = 0 ) → ( 𝐴 ·ih 𝑥 ) = 0 ) ↔ ( 𝑥 ∈ ℋ → ( ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐴 ·ih 𝑥 ) = 0 ) ) )
15	13 14	bitri	⊢ ( ( 𝑥 ∈ ( ⊥ ‘ { 𝐵 } ) → ( 𝐴 ·ih 𝑥 ) = 0 ) ↔ ( 𝑥 ∈ ℋ → ( ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐴 ·ih 𝑥 ) = 0 ) ) )
16	15	ralbii2	⊢ ( ∀ 𝑥 ∈ ( ⊥ ‘ { 𝐵 } ) ( 𝐴 ·ih 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐴 ·ih 𝑥 ) = 0 ) )
17	16	anbi2i	⊢ ( ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ ( ⊥ ‘ { 𝐵 } ) ( 𝐴 ·ih 𝑥 ) = 0 ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐴 ·ih 𝑥 ) = 0 ) ) )
18	7 17	bitri	⊢ ( 𝐴 ∈ ( ⊥ ‘ ( ⊥ ‘ { 𝐵 } ) ) ↔ ( 𝐴 ∈ ℋ ∧ ∀ 𝑥 ∈ ℋ ( ( 𝐵 ·ih 𝑥 ) = 0 → ( 𝐴 ·ih 𝑥 ) = 0 ) ) )