Theorem h1de2 5458

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector.

Hypotheses

Ref	Expression
h1de2.1	|- A e. H~
h1de2.2	|- B e. H~

Assertion

Ref	Expression
h1de2	|- (A e. (_|_` (_|_` {B})) -> ((B .i B) .s A) = ((A .i B) .s B))

Proof of Theorem h1de2

Step	Hyp	Ref	Expression
1		h1de2.2	. . . . . . . . . 10 |- B e. H~
2	1, 1	hicl 5044	. . . . . . . . 9 |- (B .i B) e. CC
3		h1de2.1	. . . . . . . . 9 |- A e. H~
4	2, 3	hvmulcl 4990	. . . . . . . 8 |- ((B .i B) .s A) e. H~
5	3, 1	hicl 5044	. . . . . . . . 9 |- (A .i B) e. CC
6	5, 1	hvmulcl 4990	. . . . . . . 8 |- ((A .i B) .s B) e. H~
7		his2subt 5052	. . . . . . . 8 |- ((((B .i B) .s A) e. H~ /\ ((A .i B) .s B) e. H~ /\ B e. H~) -> ((((B .i B) .s A) -v ((A .i B) .s B)) .i B) = ((((B .i B) .s A) .i B) - (((A .i B) .s B) .i B)))
8	4, 6, 1, 7	mp3an 642	. . . . . . 7 |- ((((B .i B) .s A) -v ((A .i B) .s B)) .i B) = ((((B .i B) .s A) .i B) - (((A .i B) .s B) .i B))
9	2, 5	mulcom 4107	. . . . . . . . 9 |- ((B .i B) x. (A .i B)) = ((A .i B) x. (B .i B))
10		ax-his3 5047	. . . . . . . . . 10 |- (((B .i B) e. CC /\ A e. H~ /\ B e. H~) -> (((B .i B) .s A) .i B) = ((B .i B) x. (A .i B)))
11	2, 3, 1, 10	mp3an 642	. . . . . . . . 9 |- (((B .i B) .s A) .i B) = ((B .i B) x. (A .i B))
12		ax-his3 5047	. . . . . . . . . 10 |- (((A .i B) e. CC /\ B e. H~ /\ B e. H~) -> (((A .i B) .s B) .i B) = ((A .i B) x. (B .i B)))
13	5, 1, 1, 12	mp3an 642	. . . . . . . . 9 |- (((A .i B) .s B) .i B) = ((A .i B) x. (B .i B))
14	9, 11, 13	3eqtr4 1126	. . . . . . . 8 |- (((B .i B) .s A) .i B) = (((A .i B) .s B) .i B)
15	4, 1	hicl 5044	. . . . . . . . 9 |- (((B .i B) .s A) .i B) e. CC
16	6, 1	hicl 5044	. . . . . . . . 9 |- (((A .i B) .s B) .i B) e. CC
17	15, 16	subeq0 4163	. . . . . . . 8 |- (((((B .i B) .s A) .i B) - (((A .i B) .s B) .i B)) = 0 <-> (((B .i B) .s A) .i B) = (((A .i B) .s B) .i B))
18	14, 17	mpbir 165	. . . . . . 7 |- ((((B .i B) .s A) .i B) - (((A .i B) .s B) .i B)) = 0
19	8, 18	eqtr 1119	. . . . . 6 |- ((((B .i B) .s A) -v ((A .i B) .s B)) .i B) = 0
20	1	h1det 5455	. . . . . . . . 9 |- (A e. (_|_` (_|_` {B})) <-> (A e. H~ /\ A.x e. H~ ((B .i x) = 0 -> (A .i x) = 0)))
21	20, 3	mpbiran 547	. . . . . . . 8 |- (A e. (_|_` (_|_` {B})) <-> A.x e. H~ ((B .i x) = 0 -> (A .i x) = 0))
22	4, 6	hvsubcl 5002	. . . . . . . . 9 |- (((B .i B) .s A) -v ((A .i B) .s B)) e. H~
23		opreq2 3007	. . . . . . . . . . . 12 |- (x = (((B .i B) .s A) -v ((A .i B) .s B)) -> (B .i x) = (B .i (((B .i B) .s A) -v ((A .i B) .s B))))
24	23	cleq1d 1109	. . . . . . . . . . 11 |- (x = (((B .i B) .s A) -v ((A .i B) .s B)) -> ((B .i x) = 0 <-> (B .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0))
25		opreq2 3007	. . . . . . . . . . . 12 |- (x = (((B .i B) .s A) -v ((A .i B) .s B)) -> (A .i x) = (A .i (((B .i B) .s A) -v ((A .i B) .s B))))
26	25	cleq1d 1109	. . . . . . . . . . 11 |- (x = (((B .i B) .s A) -v ((A .i B) .s B)) -> ((A .i x) = 0 <-> (A .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0))
27	24, 26	imbi12d 474	. . . . . . . . . 10 |- (x = (((B .i B) .s A) -v ((A .i B) .s B)) -> (((B .i x) = 0 -> (A .i x) = 0) <-> ((B .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0 -> (A .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0)))
28	27	rcla4v 1402	. . . . . . . . 9 |- (A.x e. H~ ((B .i x) = 0 -> (A .i x) = 0) -> ((((B .i B) .s A) -v ((A .i B) .s B)) e. H~ -> ((B .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0 -> (A .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0)))
29	22, 28	mpi 44	. . . . . . . 8 |- (A.x e. H~ ((B .i x) = 0 -> (A .i x) = 0) -> ((B .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0 -> (A .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0))
30	21, 29	sylbi 174	. . . . . . 7 |- (A e. (_|_` (_|_` {B})) -> ((B .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0 -> (A .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0))
31		orthcom 5061	. . . . . . . 8 |- (((((B .i B) .s A) -v ((A .i B) .s B)) e. H~ /\ B e. H~) -> (((((B .i B) .s A) -v ((A .i B) .s B)) .i B) = 0 <-> (B .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0))
32	22, 1, 31	mp2an 520	. . . . . . 7 |- (((((B .i B) .s A) -v ((A .i B) .s B)) .i B) = 0 <-> (B .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0)
33		orthcom 5061	. . . . . . . 8 |- (((((B .i B) .s A) -v ((A .i B) .s B)) e. H~ /\ A e. H~) -> (((((B .i B) .s A) -v ((A .i B) .s B)) .i A) = 0 <-> (A .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0))
34	22, 3, 33	mp2an 520	. . . . . . 7 |- (((((B .i B) .s A) -v ((A .i B) .s B)) .i A) = 0 <-> (A .i (((B .i B) .s A) -v ((A .i B) .s B))) = 0)
35	30, 32, 34	3imtr4g 426	. . . . . 6 |- (A e. (_|_` (_|_` {B})) -> (((((B .i B) .s A) -v ((A .i B) .s B)) .i B) = 0 -> ((((B .i B) .s A) -v ((A .i B) .s B)) .i A) = 0))
36	19, 35	mpi 44	. . . . 5 |- (A e. (_|_` (_|_` {B})) -> ((((B .i B) .s A) -v ((A .i B) .s B)) .i A) = 0)
37		his2subt 5052	. . . . . . 7 |- ((((B .i B) .s A) e. H~ /\ ((A .i B) .s B) e. H~ /\ A e. H~) -> ((((B .i B) .s A) -v ((A .i B) .s B)) .i A) = ((((B .i B) .s A) .i A) - (((A .i B) .s B) .i A)))
38	4, 6, 3, 37	mp3an 642	. . . . . 6 |- ((((B .i B) .s A) -v ((A .i B) .s B)) .i A) = ((((B .i B) .s A) .i A) - (((A .i B) .s B) .i A))
39		ax-his3 5047	. . . . . . . . 9 |- (((B .i B) e. CC /\ A e. H~ /\ A e. H~) -> (((B .i B) .s A) .i A) = ((B .i B) x. (A .i A)))
40	2, 3, 3, 39	mp3an 642	. . . . . . . 8 |- (((B .i B) .s A) .i A) = ((B .i B) x. (A .i A))
41	3, 3	hicl 5044	. . . . . . . . 9 |- (A .i A) e. CC
42	2, 41	mulcom 4107	. . . . . . . 8 |- ((B .i B) x. (A .i A)) = ((A .i A) x. (B .i B))
43	40, 42	eqtr 1119	. . . . . . 7 |- (((B .i B) .s A) .i A) = ((A .i A) x. (B .i B))
44		ax-his3 5047	. . . . . . . 8 |- (((A .i B) e. CC /\ B e. H~ /\ A e. H~) -> (((A .i B) .s B) .i A) = ((A .i B) x. (B .i A)))
45	5, 1, 3, 44	mp3an 642	. . . . . . 7 |- (((A .i B) .s B) .i A) = ((A .i B) x. (B .i A))
46	43, 45	opreq12i 3011	. . . . . 6 |- ((((B .i B) .s A) .i A) - (((A .i B) .s B) .i A)) = (((A .i A) x. (B .i B)) - (