Theorem ocsh 9072

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 2121	. . . . 5 |- {x e. H~ | A.y e. A (x .ih y) = 0} (_ H~
2		ocvalt 9069	. . . . . 6 |- (A (_ H~ -> (_|_` A) = {x e. H~ | A.y e. A (x .ih y) = 0})
3	2	sseq1d 2078	. . . . 5 |- (A (_ H~ -> ((_|_` A) (_ H~ <-> {x e. H~ | A.y e. A (x .ih y) = 0} (_ H~))
4	1, 3	mpbiri 194	. . . 4 |- (A (_ H~ -> (_|_` A) (_ H~)
5		ssel 2053	. . . . . . . 8 |- (A (_ H~ -> (y e. A -> y e. H~))
6		hi01t 8883	. . . . . . . 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 1705	. . . . . 6 |- (A (_ H~ -> A.y e. A (0h .ih y) = 0)
9		ax-hv0cl 8794	. . . . . 6 |- 0h e. H~
10	8, 9	jctil 292	. . . . 5 |- (A (_ H~ -> (0h e. H~ /\ A.y e. A (0h .ih y) = 0))
11		ocelt 9070	. . . . 5 |- (A (_ H~ -> (0h e. (_|_` A) <-> (0h e. H~ /\ A.y e. A (0h .ih y) = 0)))
12	10, 11	mpbird 196	. . . 4 |- (A (_ H~ -> 0h e. (_|_` A))
13	4, 12	jca 288	. . 3 |- (A (_ H~ -> ((_|_` A) (_ H~ /\ 0h e. (_|_` A)))
14		ax-his2 8871	. . . . . . . . . . . . . . . . . 18 |- ((x e. H~ /\ y e. H~ /\ z e. H~) -> ((x +h y) .ih z) = ((x .ih z) + (y .ih z)))
15	14	3expa 831	. . . . . . . . . . . . . . . . 17 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x +h y) .ih z) = ((x .ih z) + (y .ih z)))
16		opreq12 3955	. . . . . . . . . . . . . . . . . 18 |- (((x .ih z) = 0 /\ (y .ih z) = 0) -> ((x .ih z) + (y .ih z)) = (0 + 0))
17		0cn 5300	. . . . . . . . . . . . . . . . . . 19 |- 0 e. CC
18	17	addid1 5302	. . . . . . . . . . . . . . . . . 18 |- (0 + 0) = 0
19	16, 18	syl6eq 1515	. . . . . . . . . . . . . . . . 17 |- (((x .ih z) = 0 /\ (y .ih z) = 0) -> ((x .ih z) + (y .ih z)) = 0)
20	15, 19	sylan9eq 1519	. . . . . . . . . . . . . . . 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 373	. . . . . . . . . . . . . . 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 436	. . . . . . . . . . . . . 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 2054	. . . . . . . . . . . . . 14 |- ((A (_ H~ /\ z e. A) -> z e. H~)
24	22, 23	sylan 448	. . . . . . . . . . . . 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 488	. . . . . . . . . . . 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 1701	. . . . . . . . . . 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 373	. . . . . . . . . 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 445	. . . . . . . . 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		hvaddclt 8803	. . . . . . . . . 10 |- ((x e. H~ /\ y e. H~) -> (x +h y) e. H~)
30	29	anim1i 334	. . . . . . . . 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		ocelt 9070	. . . . . . . . . 10 |- (A (_ H~ -> (x e. (_|_` A) <-> (x e. H~ /\ A.z e. A (x .ih z) = 0)))
33		ocelt 9070	. . . . . . . . . 10 |- (A (_ H~ -> (y e. (_|_` A) <-> (y e. H~ /\ A.z e. A (y .ih z) = 0)))
34	32, 33	anbi12d 626	. . . . . . . . 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 505	. . . . . . . . . 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 1742	. . . . . . . . . . 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 479	. . . . . . . . . 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	bitr4 176	. . . . . . . . 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 534	. . . . . . . 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		ocelt 9070	. . . . . . . 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 541	. . . . . . 7 |- (A (_ H~ -> ((x e. (_|_` A) /\ y e. (_|_` A)) -> (x +h y) e. (_|_` A)))
42	41	exp3a 375	. . . . . 6 |- (A (_ H~ -> (x e. (_|_` A) -> (y e. (_|_` A) -> (x +h y) e. (_|_` A))))
43	42	r19.21adv 1710	. . . . 5 |- (A (_ H~ -> (x e. (_|_` A) -> A.y e. (_|_` A)(x +h y) e. (_|_` A)))
44	43	r19.21aiv 1705	. . . 4 |- (A (_ H~ -> A.x e. (_|_` A)A.y e. (_|_` A)(x +h y) e. (_|_` A))
45		opreq2 3954	. . . . . . . . . . . . . . . . . 18 |- ((y .ih z) = 0 -> (x x. (y .ih z)) = (x x. 0))
46	45	eqeq1d 1475	. . . . . . . . . . . . . . . . 17 |- ((y .ih z) = 0 -> ((x x. (y .ih z)) = 0 <-> (x x. 0) = 0))
47		mul01t 5415	. . . . . . . . . . . . . . . . 17 |- (x e. CC -> (x x. 0) = 0)
48	46, 47	syl5cbir 211	. . . . . . . . . . . . . . . 16 |- (x e. CC -> ((y .ih z) = 0 -> (x x. (y .ih z)) = 0))
49	48	ad2antrl 406	. . . . . . . . . . . . . . 15 |- ((z e. H~ /\ (x e. CC /\ y e. H~)) -> ((y .ih z) = 0 -> (x x. (y .ih z)) = 0))
50		ax-his3 8872	. . . . . . . . . . . . . . . . . 18 |- ((x e. CC /\ y e. H~ /\ z e. H~) -> ((x .h y) .ih z) = (x x. (y .ih z)))
51	50	eqeq1d 1475	. . . . . . . . . . . . . . . . 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 831	. . . . . . . . . . . . . . . 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 436	. . . . . . . . . . . . . . 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 204	. . . . . . . . . . . . . 14 |- ((z