Theorem ocsh 9239

Description: The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of [Beran] p. 107.

Assertion

Ref	Expression
ocsh	|- (A (_ H~ -> (_|_` A) e. SH)

Proof of Theorem ocsh

Step	Hyp	Ref	Expression
1		ssrab2 2182	. . . . 5 |- {x e. H~ | A.y e. A (x .ih y) = 0} (_ H~
2		ocval 9236	. . . . . 6 |- (A (_ H~ -> (_|_` A) = {x e. H~ | A.y e. A (x .ih y) = 0})
3	2	sseq1d 2139	. . . . 5 |- (A (_ H~ -> ((_|_` A) (_ H~ <-> {x e. H~ | A.y e. A (x .ih y) = 0} (_ H~))
4	1, 3	mpbiri 201	. . . 4 |- (A (_ H~ -> (_|_` A) (_ H~)
5		ssel 2114	. . . . . . . 8 |- (A (_ H~ -> (y e. A -> y e. H~))
6		hi01 9045	. . . . . . . 8 |- (y e. H~ -> (0h .ih y) = 0)
7	5, 6	syl6 22	. . . . . . 7 |- (A (_ H~ -> (y e. A -> (0h .ih y) = 0))
8	7	r19.21aiv 1760	. . . . . 6 |- (A (_ H~ -> A.y e. A (0h .ih y) = 0)
9		ax-hv0cl 8956	. . . . . 6 |- 0h e. H~
10	8, 9	jctil 299	. . . . 5 |- (A (_ H~ -> (0h e. H~ /\ A.y e. A (0h .ih y) = 0))
11		ocel 9237	. . . . 5 |- (A (_ H~ -> (0h e. (_|_` A) <-> (0h e. H~ /\ A.y e. A (0h .ih y) = 0)))
12	10, 11	mpbird 203	. . . 4 |- (A (_ H~ -> 0h e. (_|_` A))
13	4, 12	jca 295	. . 3 |- (A (_ H~ -> ((_|_` A) (_ H~ /\ 0h e. (_|_` A)))
14		ax-his2 9033	. . . . . . . . . . . . . . . . . 18 |- ((x e. H~ /\ y e. H~ /\ z e. H~) -> ((x +h y) .ih z) = ((x .ih z) + (y .ih z)))
15	14	3expa 845	. . . . . . . . . . . . . . . . 17 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x +h y) .ih z) = ((x .ih z) + (y .ih z)))
16		opreq12 4028	. . . . . . . . . . . . . . . . . 18 |- (((x .ih z) = 0 /\ (y .ih z) = 0) -> ((x .ih z) + (y .ih z)) = (0 + 0))
17		0cn 5393	. . . . . . . . . . . . . . . . . . 19 |- 0 e. CC
18	17	addid1i 5395	. . . . . . . . . . . . . . . . . 18 |- (0 + 0) = 0
19	16, 18	syl6eq 1570	. . . . . . . . . . . . . . . . 17 |- (((x .ih z) = 0 /\ (y .ih z) = 0) -> ((x .ih z) + (y .ih z)) = 0)
20	15, 19	sylan9eq 1574	. . . . . . . . . . . . . . . 16 |- ((((x e. H~ /\ y e. H~) /\ z e. H~) /\ ((x .ih z) = 0 /\ (y .ih z) = 0)) -> ((x +h y) .ih z) = 0)
21	20	ex 380	. . . . . . . . . . . . . . 15 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> (((x .ih z) = 0 /\ (y .ih z) = 0) -> ((x +h y) .ih z) = 0))
22	21	ancoms 447	. . . . . . . . . . . . . 14 |- ((z e. H~ /\ (x e. H~ /\ y e. H~)) -> (((x .ih z) = 0 /\ (y .ih z) = 0) -> ((x +h y) .ih z) = 0))
23		ssel2 2115	. . . . . . . . . . . . . 14 |- ((A (_ H~ /\ z e. A) -> z e. H~)
24	22, 23	sylan 459	. . . . . . . . . . . . 13 |- (((A (_ H~ /\ z e. A) /\ (x e. H~ /\ y e. H~)) -> (((x .ih z) = 0 /\ (y .ih z) = 0) -> ((x +h y) .ih z) = 0))
25	24	an1rs 500	. . . . . . . . . . . 12 |- (((A (_ H~ /\ (x e. H~ /\ y e. H~)) /\ z e. A) -> (((x .ih z) = 0 /\ (y .ih z) = 0) -> ((x +h y) .ih z) = 0))
26	25	r19.20dva 1756	. . . . . . . . . . 11 |- ((A (_ H~ /\ (x e. H~ /\ y e. H~)) -> (A.z e. A ((x .ih z) = 0 /\ (y .ih z) = 0) -> A.z e. A ((x +h y) .ih z) = 0))
27	26	ex 380	. . . . . . . . . 10 |- (A (_ H~ -> ((x e. H~ /\ y e. H~) -> (A.z e. A ((x .ih z) = 0 /\ (y .ih z) = 0) -> A.z e. A ((x +h y) .ih z) = 0)))
28	27	imdistand 456	. . . . . . . . 9 |- (A (_ H~ -> (((x e. H~ /\ y e. H~) /\ A.z e. A ((x .ih z) = 0 /\ (y .ih z) = 0)) -> ((x e. H~ /\ y e. H~) /\ A.z e. A ((x +h y) .ih z) = 0)))
29		hvaddcl 8965	. . . . . . . . . 10 |- ((x e. H~ /\ y e. H~) -> (x +h y) e. H~)
30	29	anim1i 341	. . . . . . . . 9 |- (((x e. H~ /\ y e. H~) /\ A.z e. A ((x +h y) .ih z) = 0) -> ((x +h y) e. H~ /\ A.z e. A ((x +h y) .ih z) = 0))
31	28, 30	syl6 22	. . . . . . . 8 |- (A (_ H~ -> (((x e. H~ /\ y e. H~) /\ A.z e. A ((x .ih z) = 0 /\ (y .ih z) = 0)) -> ((x +h y) e. H~ /\ A.z e. A ((x +h y) .ih z) = 0)))
32		ocel 9237	. . . . . . . . . 10 |- (A (_ H~ -> (x e. (_|_` A) <-> (x e. H~ /\ A.z e. A (x .ih z) = 0)))
33		ocel 9237	. . . . . . . . . 10 |- (A (_ H~ -> (y e. (_|_` A) <-> (y e. H~ /\ A.z e. A (y .ih z) = 0)))
34	32, 33	anbi12d 639	. . . . . . . . 9 |- (A (_ H~ -> ((x e. (_|_` A) /\ y e. (_|_` A)) <-> ((x e. H~ /\ A.z e. A (x .ih z) = 0) /\ (y e. H~ /\ A.z e. A (y .ih z) = 0))))
35		an4 517	. . . . . . . . . 10 |- (((x e. H~ /\ A.z e. A (x .ih z) = 0) /\ (y e. H~ /\ A.z e. A (y .ih z) = 0)) <-> ((x e. H~ /\ y e. H~) /\ (A.z e. A (x .ih z) = 0 /\ A.z e. A (y .ih z) = 0)))
36		r19.26 1797	. . . . . . . . . . 11 |- (A.z e. A ((x .ih z) = 0 /\ (y .ih z) = 0) <-> (A.z e. A (x .ih z) = 0 /\ A.z e. A (y .ih z) = 0))
37	36	anbi2i 491	. . . . . . . . . 10 |- (((x e. H~ /\ y e. H~) /\ A.z e. A ((x .ih z) = 0 /\ (y .ih z) = 0)) <-> ((x e. H~ /\ y e. H~) /\ (A.z e. A (x .ih z) = 0 /\ A.z e. A (y .ih z) = 0)))
38	35, 37	bitr4i 183	. . . . . . . . 9 |- (((x e. H~ /\ A.z e. A (x .ih z) = 0) /\ (y e. H~ /\ A.z e. A (y .ih z) = 0)) <-> ((x e. H~ /\ y e. H~) /\ A.z e. A ((x .ih z) = 0 /\ (y .ih z) = 0)))
39	34, 38	syl6bb 547	. . . . . . . 8 |- (A (_ H~ -> ((x e. (_|_` A) /\ y e. (_|_` A)) <-> ((x e. H~ /\ y e. H~) /\ A.z e. A ((x .ih z) = 0 /\ (y .ih z) = 0))))
40		ocel 9237	. . . . . . . 8 |- (A (_ H~ -> ((x +h y) e. (_|_` A) <-> ((x +h y) e. H~ /\ A.z e. A ((x +h y) .ih z) = 0)))
41	31, 39, 40	3imtr4d 554	. . . . . . 7 |- (A (_ H~ -> ((x e. (_|_` A) /\ y e. (_|_` A)) -> (x +h y) e. (_|_` A)))
42	41	exp3a 383	. . . . . 6 |- (A (_ H~ -> (x e. (_|_` A) -> (y e. (_|_` A) -> (x +h y) e. (_|_` A))))
43	42	r19.21adv 1765	. . . . 5 |- (A (_ H~ -> (x e. (_|_` A) -> A.y e. (_|_` A)(x +h y) e. (_|_` A)))
44	43	r19.21aiv 1760	. . . 4 |- (A (_ H~ -> A.x e. (_|_` A)A.y e. (_|_` A)(x +h y) e. (_|_` A))
45		opreq2 4027	. . . . . . . . . . . . . . . . . 18 |- ((y .ih z) = 0 -> (x x. (y .ih z)) = (x x. 0))
46	45	eqeq1d 1530	. . . . . . . . . . . . . . . . 17 |- ((y .ih z) = 0 -> ((x x. (y .ih z)) = 0 <-> (x x. 0) = 0))
47		mul01 5508	. . . . . . . . . . . . . . . . 17 |- (x e. CC -> (x x. 0) = 0)
48	46, 47	syl5cbir 218	. . . . . . . . . . . . . . . 16 |- (x e. CC -> ((y .ih z) = 0 -> (x x. (y .ih z)) = 0))
49	48	ad2antrl 415	. . . . . . . . . . . . . . 15 |- ((z e. H~ /\ (x e. CC /\ y e. H~)) -> ((y .ih z) = 0 -> (x x. (y .ih z)) = 0))
50		ax-his3 9034	. . . . . . . . . . . . . . . . . 18 |- ((x e. CC /\ y e. H~ /\ z e. H~) -> ((x .h y) .ih z) = (x x. (y .ih z)))
51	50	eqeq1d 1530	. . . . . . . . . . . . . . . . 17 |- ((x e. CC /\ y e. H~ /\ z e. H~) -> (((x .h y) .ih z) = 0 <-> (x x. (y .ih z)) = 0))
52	51	3expa 845	. . . . . . . . . . . . . . . 16 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> (((x .h y) .ih z) = 0 <-> (x x. (y .ih z)) = 0))
53	52	ancoms 447	. . . . . . . . . . . . . . 15 |- ((z e. H~ /\ (x e. CC /\ y e. H~)) -> (((x .h y) .ih z) = 0 <-> (x x. (y .ih z)) = 0))
54	49, 53	sylibrd 211	. . . . . . . . . . . . . 14 |- ((