Theorem ocsh

Description: The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	ocsh	⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )

Proof

Step	Hyp	Ref	Expression
1		ocval	⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) = { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } )
2		ssrab2	⊢ { 𝑥 ∈ ℋ ∣ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ·ih 𝑦 ) = 0 } ⊆ ℋ
3	1 2	eqsstrdi	⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ⊆ ℋ )
4		ssel	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ ) )
5		hi01	⊢ ( 𝑦 ∈ ℋ → ( 0ℎ ·ih 𝑦 ) = 0 )
6	4 5	syl6	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ 𝐴 → ( 0ℎ ·ih 𝑦 ) = 0 ) )
7	6	ralrimiv	⊢ ( 𝐴 ⊆ ℋ → ∀ 𝑦 ∈ 𝐴 ( 0ℎ ·ih 𝑦 ) = 0 )
8		ax-hv0cl	⊢ 0ℎ ∈ ℋ
9	7 8	jctil	⊢ ( 𝐴 ⊆ ℋ → ( 0ℎ ∈ ℋ ∧ ∀ 𝑦 ∈ 𝐴 ( 0ℎ ·ih 𝑦 ) = 0 ) )
10		ocel	⊢ ( 𝐴 ⊆ ℋ → ( 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 0ℎ ∈ ℋ ∧ ∀ 𝑦 ∈ 𝐴 ( 0ℎ ·ih 𝑦 ) = 0 ) ) )
11	9 10	mpbird	⊢ ( 𝐴 ⊆ ℋ → 0ℎ ∈ ( ⊥ ‘ 𝐴 ) )
12	3 11	jca	⊢ ( 𝐴 ⊆ ℋ → ( ( ⊥ ‘ 𝐴 ) ⊆ ℋ ∧ 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ) )
13		ssel2	⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℋ )
14		ax-his2	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = ( ( 𝑥 ·ih 𝑧 ) + ( 𝑦 ·ih 𝑧 ) ) )
15	14	3expa	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = ( ( 𝑥 ·ih 𝑧 ) + ( 𝑦 ·ih 𝑧 ) ) )
16		oveq12	⊢ ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ·ih 𝑧 ) + ( 𝑦 ·ih 𝑧 ) ) = ( 0 + 0 ) )
17		00id	⊢ ( 0 + 0 ) = 0
18	16 17	eqtrdi	⊢ ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ·ih 𝑧 ) + ( 𝑦 ·ih 𝑧 ) ) = 0 )
19	15 18	sylan9eq	⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) ∧ ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 )
20	19	ex	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
21	20	ancoms	⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
22	13 21	sylan	⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
23	22	an32s	⊢ ( ( ( 𝐴 ⊆ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
24	23	ralimdva	⊢ ( ( 𝐴 ⊆ ℋ ∧ ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) → ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
25	24	imdistanda	⊢ ( 𝐴 ⊆ ℋ → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) → ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
26		hvaddcl	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ )
27	26	anim1i	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) → ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
28	25 27	syl6	⊢ ( 𝐴 ⊆ ℋ → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) → ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
29		ocel	⊢ ( 𝐴 ⊆ ℋ → ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 𝑥 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ) ) )
30		ocel	⊢ ( 𝐴 ⊆ ℋ → ( 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ↔ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
31	29 30	anbi12d	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ) ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) ) )
32		an4	⊢ ( ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ) ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
33		r19.26	⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ↔ ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) )
34	33	anbi2i	⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
35	32 34	bitr4i	⊢ ( ( ( 𝑥 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑥 ·ih 𝑧 ) = 0 ) ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
36	31 35	bitrdi	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ih 𝑧 ) = 0 ∧ ( 𝑦 ·ih 𝑧 ) = 0 ) ) ) )
37		ocel	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 +ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
38	28 36 37	3imtr4d	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ) )
39	38	ralrimivv	⊢ ( 𝐴 ⊆ ℋ → ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) )
40		mul01	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 0 ) = 0 )
41		oveq2	⊢ ( ( 𝑦 ·ih 𝑧 ) = 0 → ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = ( 𝑥 · 0 ) )
42	41	eqeq1d	⊢ ( ( 𝑦 ·ih 𝑧 ) = 0 → ( ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ↔ ( 𝑥 · 0 ) = 0 ) )
43	40 42	syl5ibrcom	⊢ ( 𝑥 ∈ ℂ → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
44	43	ad2antrl	⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
45		ax-his3	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) )
46	45	eqeq1d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ↔ ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
47	46	3expa	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ 𝑧 ∈ ℋ ) → ( ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ↔ ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
48	47	ancoms	⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ↔ ( 𝑥 · ( 𝑦 ·ih 𝑧 ) ) = 0 ) )
49	44 48	sylibrd	⊢ ( ( 𝑧 ∈ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
50	13 49	sylan	⊢ ( ( ( 𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
51	50	an32s	⊢ ( ( ( 𝐴 ⊆ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 ·ih 𝑧 ) = 0 → ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
52	51	ralimdva	⊢ ( ( 𝐴 ⊆ ℋ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 → ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
53	52	imdistanda	⊢ ( 𝐴 ⊆ ℋ → ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
54		hvmulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
55	54	anim1i	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) )
56	53 55	syl6	⊢ ( 𝐴 ⊆ ℋ → ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) → ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
57	30	anbi2d	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) ) )
58		anass	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑦 ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
59	57 58	bitr4di	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) ↔ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ·ih 𝑧 ) = 0 ) ) )
60		ocel	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ↔ ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 ·ℎ 𝑦 ) ·ih 𝑧 ) = 0 ) ) )
61	56 59 60	3imtr4d	⊢ ( 𝐴 ⊆ ℋ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ) )
62	61	ralrimivv	⊢ ( 𝐴 ⊆ ℋ → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) )
63	39 62	jca	⊢ ( 𝐴 ⊆ ℋ → ( ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ) )
64		issh2	⊢ ( ( ⊥ ‘ 𝐴 ) ∈ Sℋ ↔ ( ( ( ⊥ ‘ 𝐴 ) ⊆ ℋ ∧ 0ℎ ∈ ( ⊥ ‘ 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ ( ⊥ ‘ 𝐴 ) ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( ⊥ ‘ 𝐴 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( ⊥ ‘ 𝐴 ) ) ) )
65	12 63 64	sylanbrc	⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Sℋ )