Theorem ocsh 5164

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		ssrab 1556	. . . . 5 |- {x e. H~ | A.y e. A (x .i y) = 0} (_ H~
2		ocvalt 5161	. . . . . 6 |- (A (_ H~ -> (_|_` A) = {x e. H~ | A.y e. A (x .i y) = 0})
3	2	sseq1d 1527	. . . . 5 |- (A (_ H~ -> ((_|_` A) (_ H~ <-> {x e. H~ | A.y e. A (x .i y) = 0} (_ H~))
4	1, 3	mpbiri 169	. . . 4 |- (A (_ H~ -> (_|_` A) (_ H~)
5		ssel 1502	. . . . . . . 8 |- (A (_ H~ -> (y e. A -> y e. H~))
6		hizer1t 5054	. . . . . . . 8 |- (y e. H~ -> (0v .i y) = 0)
7	5, 6	syl6 23	. . . . . . 7 |- (A (_ H~ -> (y e. A -> (0v .i y) = 0))
8	7	r19.21aiv 1259	. . . . . 6 |- (A (_ H~ -> A.y e. A (0v .i y) = 0)
9		ax-hvzercl 4987	. . . . . 6 |- 0v e. H~
10	8, 9	jctil 240	. . . . 5 |- (A (_ H~ -> (0v e. H~ /\ A.y e. A (0v .i y) = 0))
11		ocelt 5162	. . . . 5 |- (A (_ H~ -> (0v e. (_|_` A) <-> (0v e. H~ /\ A.y e. A (0v .i y) = 0)))
12	10, 11	mpbird 171	. . . 4 |- (A (_ H~ -> 0v e. (_|_` A))
13	4, 12	jca 236	. . 3 |- (A (_ H~ -> ((_|_` A) (_ H~ /\ 0v e. (_|_` A)))
14		ax-his2 5046	. . . . . . . . . . . . . . . . . 18 |- ((x e. H~ /\ y e. H~ /\ z e. H~) -> ((x +v y) .i z) = ((x .i z) + (y .i z)))
15	14	3expa 612	. . . . . . . . . . . . . . . . 17 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> ((x +v y) .i z) = ((x .i z) + (y .i z)))
16		opreq12 3008	. . . . . . . . . . . . . . . . . 18 |- (((x .i z) = 0 /\ (y .i z) = 0) -> ((x .i z) + (y .i z)) = (0 + 0))
17		0cn 4100	. . . . . . . . . . . . . . . . . . 19 |- 0 e. CC
18	17	addid1 4112	. . . . . . . . . . . . . . . . . 18 |- (0 + 0) = 0
19	16, 18	syl6eq 1140	. . . . . . . . . . . . . . . . 17 |- (((x .i z) = 0 /\ (y .i z) = 0) -> ((x .i z) + (y .i z)) = 0)
20	15, 19	sylan9eq 1144	. . . . . . . . . . . . . . . 16 |- ((((x e. H~ /\ y e. H~) /\ z e. H~) /\ ((x .i z) = 0 /\ (y .i z) = 0)) -> ((x +v y) .i z) = 0)
21	20	exp 291	. . . . . . . . . . . . . . 15 |- (((x e. H~ /\ y e. H~) /\ z e. H~) -> (((x .i z) = 0 /\ (y .i z) = 0) -> ((x +v y) .i z) = 0))
22	21	ancoms 334	. . . . . . . . . . . . . 14 |- ((z e. H~ /\ (x e. H~ /\ y e. H~)) -> (((x .i z) = 0 /\ (y .i z) = 0) -> ((x +v y) .i z) = 0))
23		ssel2 1503	. . . . . . . . . . . . . 14 |- ((A (_ H~ /\ z e. A) -> z e. H~)
24	22, 23	sylan 343	. . . . . . . . . . . . 13 |- (((A (_ H~ /\ z e. A) /\ (x e. H~ /\ y e. H~)) -> (((x .i z) = 0 /\ (y .i z) = 0) -> ((x +v y) .i z) = 0))
25	24	an1rs 373	. . . . . . . . . . . 12 |- (((A (_ H~ /\ (x e. H~ /\ y e. H~)) /\ z e. A) -> (((x .i z) = 0 /\ (y .i z) = 0) -> ((x +v y) .i z) = 0))
26	25	r19.20dva 1256	. . . . . . . . . . 11 |- ((A (_ H~ /\ (x e. H~ /\ y e. H~)) -> (A.z e. A ((x .i z) = 0 /\ (y .i z) = 0) -> A.z e. A ((x +v y) .i z) = 0))
27	26	exp 291	. . . . . . . . . 10 |- (A (_ H~ -> ((x e. H~ /\ y e. H~) -> (A.z e. A ((x .i z) = 0 /\ (y .i z) = 0) -> A.z e. A ((x +v y) .i z) = 0)))
28	27	imdistand 342	. . . . . . . . 9 |- (A (_ H~ -> (((x e. H~ /\ y e. H~) /\ A.z e. A ((x .i z) = 0 /\ (y .i z) = 0)) -> ((x e. H~ /\ y e. H~) /\ A.z e. A ((x +v y) .i z) = 0)))
29		ax-hvaddcl 4984	. . . . . . . . . 10 |- ((x e. H~ /\ y e. H~) -> (x +v y) e. H~)
30	29	anim1i 269	. . . . . . . . 9 |- (((x e. H~ /\ y e. H~) /\ A.z e. A ((x +v y) .i z) = 0) -> ((x +v y) e. H~ /\ A.z e. A ((x +v y) .i z) = 0))
31	28, 30	syl6 23	. . . . . . . 8 |- (A (_ H~ -> (((x e. H~ /\ y e. H~) /\ A.z e. A ((x .i z) = 0 /\ (y .i z) = 0)) -> ((x +v y) e. H~ /\ A.z e. A ((x +v y) .i z) = 0)))
32		ocelt 5162	. . . . . . . . . 10 |- (A (_ H~ -> (x e. (_|_` A) <-> (x e. H~ /\ A.z e. A (x .i z) = 0)))
33		ocelt 5162	. . . . . . . . . 10 |- (A (_ H~ -> (y e. (_|_` A) <-> (y e. H~ /\ A.z e. A (y .i z) = 0)))
34	32, 33	anbi12d 476	. . . . . . . . 9 |- (A (_ H~ -> ((x e. (_|_` A) /\ y e. (_|_` A)) <-> ((x e. H~ /\ A.z e. A (x .i z) = 0) /\ (y e. H~ /\ A.z e. A (y .i z) = 0))))
35		an4 388	. . . . . . . . . 10 |- (((x e. H~ /\ A.z e. A (x .i z) = 0) /\ (y e. H~ /\ A.z e. A (y .i z) = 0)) <-> ((x e. H~ /\ y e. H~) /\ (A.z e. A (x .i z) = 0 /\ A.z e. A (y .i z) = 0)))
36		r19.26 1289	. . . . . . . . . . 11 |- (A.z e. A ((x .i z) = 0 /\ (y .i z) = 0) <-> (A.z e. A (x .i z) = 0 /\ A.z e. A (y .i z) = 0))
37	36	anbi2i 367	. . . . . . . . . 10 |- (((x e. H~ /\ y e. H~) /\ A.z e. A ((x .i z) = 0 /\ (y .i z) = 0)) <-> ((x e. H~ /\ y e. H~) /\ (A.z e. A (x .i z) = 0 /\ A.z e. A (y .i z) = 0)))
38	35, 37	bitr4 154	. . . . . . . . 9 |- (((x e. H~ /\ A.z e. A (x .i z) = 0) /\ (y e. H~ /\ A.z e. A (y .i z) = 0)) <-> ((x e. H~ /\ y e. H~) /\ A.z e. A ((x .i z) = 0 /\ (y .i z) = 0)))
39	34, 38	syl6bb 414	. . . . . . . 8 |- (A (_ H~ -> ((x e. (_|_` A) /\ y e. (_|_` A)) <-> ((x e. H~ /\ y e. H~) /\ A.z e. A ((x .i z) = 0 /\ (y .i z) = 0))))
40		ocelt 5162	. . . . . . . 8 |- (A (_ H~ -> ((x +v y) e. (_|_` A) <-> ((x +v y) e. H~ /\ A.z e. A ((x +v y) .i z) = 0)))
41	31, 39, 40	3imtr4d 421	. . . . . . 7 |- (A (_ H~ -> ((x e. (_|_` A) /\ y e. (_|_` A)) -> (x +v y) e. (_|_` A)))
42	41	exp3a 292	. . . . . 6 |- (A (_ H~ -> (x e. (_|_` A) -> (y e. (_|_` A) -> (x +v y) e. (_|_` A))))
43	42	r19.21adv 1262	. . . . 5 |- (A (_ H~ -> (x e. (_|_` A) -> A.y e. (_|_` A)(x +v y) e. (_|_` A)))
44	43	r19.21aiv 1259	. . . 4 |- (A (_ H~ -> A.x e. (_|_` A)A.y e. (_|_` A)(x +v y) e. (_|_` A))
45		opreq2 3007	. . . . . . . . . . . . . . . . . . 19 |- ((y .i z) = 0 -> (x x. (y .i z)) = (x x. 0))
46	45	cleq1d 1109	. . . . . . . . . . . . . . . . . 18 |- ((y .i z) = 0 -> ((x x. (y .i z)) = 0 <-> (x x. 0) = 0))
47		mulzer1t 4188	. . . . . . . . . . . . . . . . . 18 |- (x e. CC -> (x x. 0) = 0)
48	46, 47	syl5bir 184	. . . . . . . . . . . . . . . . 17 |- ((y .i z) = 0 -> (x e. CC -> (x x. (y .i z)) = 0))
49	48	com12 13	. . . . . . . . . . . . . . . 16 |- (x e. CC -> ((y .i z) = 0 -> (x x. (y .i z)) = 0))
50	49	ad2antrl 322	. . . . . . . . . . . . . . 15 |- ((z e. H~ /\ (x e. CC /\ y e. H~)) -> ((y .i z) = 0 -> (x x. (y .i z)) = 0))
51		ax-his3 5047	. . . . . . . . . . . . . . . . . 18 |- ((x e. CC /\ y e. H~ /\ z e. H~) -> ((x .s y) .i z) = (x x. (y .i z)))
52	51	cleq1d 1109	. . . . . . . . . . . . . . . . 17 |- ((x e. CC /\ y e. H~ /\ z e. H~) -> (((x .s y) .i z) = 0 <-> (x x. (y .i z)) = 0))
53	52	3expa 612	. . . . . . . . . . . . . . . 16 |- (((x e. CC /\ y e. H~) /\ z e. H~) -> (((x .s y) .i z) = 0 <-> (x x. (y .i z)) = 0))
54	53	ancoms 334	. . . . . . . . . . . . . . 15 |- ((z e. H~ /\ (x e. CC /\ y e. H~)) -> (((x .s y) .i z) = 0 <-> (x x. (y .i z)) = 0))
55	50, 54	sylibrd 179	. . . . . . . . . . . . . 14 |- ((z e. H~ /\ (x e. CC /\ y e. H~)) -> ((y .i z) = 0 -> ((x .s y) .i z) = 0)