Theorem h1de2 9391

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 .ih B) .h A) = ((A .ih B) .h B))

Proof of Theorem h1de2

Step	Hyp	Ref	Expression
1		h1de2.2	. . . . . . . . . 10 |- B e. H~
2	1, 1	hicl 8869	. . . . . . . . 9 |- (B .ih B) e. CC
3		h1de2.1	. . . . . . . . 9 |- A e. H~
4	2, 3	hvmulcl 8805	. . . . . . . 8 |- ((B .ih B) .h A) e. H~
5	3, 1	hicl 8869	. . . . . . . . 9 |- (A .ih B) e. CC
6	5, 1	hvmulcl 8805	. . . . . . . 8 |- ((A .ih B) .h B) e. H~
7		his2subt 8879	. . . . . . . 8 |- ((((B .ih B) .h A) e. H~ /\ ((A .ih B) .h B) e. H~ /\ B e. H~) -> ((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih B) = ((((B .ih B) .h A) .ih B) - (((A .ih B) .h B) .ih B)))
8	4, 6, 1, 7	mp3an 913	. . . . . . 7 |- ((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih B) = ((((B .ih B) .h A) .ih B) - (((A .ih B) .h B) .ih B))
9	2, 5	mulcom 5295	. . . . . . . . 9 |- ((B .ih B) x. (A .ih B)) = ((A .ih B) x. (B .ih B))
10		ax-his3 8872	. . . . . . . . . 10 |- (((B .ih B) e. CC /\ A e. H~ /\ B e. H~) -> (((B .ih B) .h A) .ih B) = ((B .ih B) x. (A .ih B)))
11	2, 3, 1, 10	mp3an 913	. . . . . . . . 9 |- (((B .ih B) .h A) .ih B) = ((B .ih B) x. (A .ih B))
12		ax-his3 8872	. . . . . . . . . 10 |- (((A .ih B) e. CC /\ B e. H~ /\ B e. H~) -> (((A .ih B) .h B) .ih B) = ((A .ih B) x. (B .ih B)))
13	5, 1, 1, 12	mp3an 913	. . . . . . . . 9 |- (((A .ih B) .h B) .ih B) = ((A .ih B) x. (B .ih B))
14	9, 11, 13	3eqtr4 1497	. . . . . . . 8 |- (((B .ih B) .h A) .ih B) = (((A .ih B) .h B) .ih B)
15	4, 1	hicl 8869	. . . . . . . . 9 |- (((B .ih B) .h A) .ih B) e. CC
16	6, 1	hicl 8869	. . . . . . . . 9 |- (((A .ih B) .h B) .ih B) e. CC
17	15, 16	subeq0 5377	. . . . . . . 8 |- (((((B .ih B) .h A) .ih B) - (((A .ih B) .h B) .ih B)) = 0 <-> (((B .ih B) .h A) .ih B) = (((A .ih B) .h B) .ih B))
18	14, 17	mpbir 190	. . . . . . 7 |- ((((B .ih B) .h A) .ih B) - (((A .ih B) .h B) .ih B)) = 0
19	8, 18	eqtr 1487	. . . . . 6 |- ((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih B) = 0
20	1	h1det 9388	. . . . . . . . 9 |- (A e. (_|_` (_|_` {B})) <-> (A e. H~ /\ A.x e. H~ ((B .ih x) = 0 -> (A .ih x) = 0)))
21	20, 3	mpbiran 726	. . . . . . . 8 |- (A e. (_|_` (_|_` {B})) <-> A.x e. H~ ((B .ih x) = 0 -> (A .ih x) = 0))
22	4, 6	hvsubcl 8812	. . . . . . . . 9 |- (((B .ih B) .h A) -h ((A .ih B) .h B)) e. H~
23		opreq2 3954	. . . . . . . . . . . 12 |- (x = (((B .ih B) .h A) -h ((A .ih B) .h B)) -> (B .ih x) = (B .ih (((B .ih B) .h A) -h ((A .ih B) .h B))))
24	23	eqeq1d 1475	. . . . . . . . . . 11 |- (x = (((B .ih B) .h A) -h ((A .ih B) .h B)) -> ((B .ih x) = 0 <-> (B .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0))
25		opreq2 3954	. . . . . . . . . . . 12 |- (x = (((B .ih B) .h A) -h ((A .ih B) .h B)) -> (A .ih x) = (A .ih (((B .ih B) .h A) -h ((A .ih B) .h B))))
26	25	eqeq1d 1475	. . . . . . . . . . 11 |- (x = (((B .ih B) .h A) -h ((A .ih B) .h B)) -> ((A .ih x) = 0 <-> (A .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0))
27	24, 26	imbi12d 624	. . . . . . . . . 10 |- (x = (((B .ih B) .h A) -h ((A .ih B) .h B)) -> (((B .ih x) = 0 -> (A .ih x) = 0) <-> ((B .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0 -> (A .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0)))
28	27	rcla4v 1864	. . . . . . . . 9 |- ((((B .ih B) .h A) -h ((A .ih B) .h B)) e. H~ -> (A.x e. H~ ((B .ih x) = 0 -> (A .ih x) = 0) -> ((B .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0 -> (A .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0)))
29	22, 28	ax-mp 7	. . . . . . . 8 |- (A.x e. H~ ((B .ih x) = 0 -> (A .ih x) = 0) -> ((B .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0 -> (A .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0))
30	21, 29	sylbi 199	. . . . . . 7 |- (A e. (_|_` (_|_` {B})) -> ((B .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0 -> (A .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0))
31		orthcom 8895	. . . . . . . 8 |- (((((B .ih B) .h A) -h ((A .ih B) .h B)) e. H~ /\ B e. H~) -> (((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih B) = 0 <-> (B .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0))
32	22, 1, 31	mp2an 695	. . . . . . 7 |- (((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih B) = 0 <-> (B .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0)
33		orthcom 8895	. . . . . . . 8 |- (((((B .ih B) .h A) -h ((A .ih B) .h B)) e. H~ /\ A e. H~) -> (((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih A) = 0 <-> (A .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0))
34	22, 3, 33	mp2an 695	. . . . . . 7 |- (((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih A) = 0 <-> (A .ih (((B .ih B) .h A) -h ((A .ih B) .h B))) = 0)
35	30, 32, 34	3imtr4g 551	. . . . . 6 |- (A e. (_|_` (_|_` {B})) -> (((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih B) = 0 -> ((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih A) = 0))
36	19, 35	mpi 44	. . . . 5 |- (A e. (_|_` (_|_` {B})) -> ((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih A) = 0)
37		his2subt 8879	. . . . . . 7 |- ((((B .ih B) .h A) e. H~ /\ ((A .ih B) .h B) e. H~ /\ A e. H~) -> ((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih A) = ((((B .ih B) .h A) .ih A) - (((A .ih B) .h B) .ih A)))
38	4, 6, 3, 37	mp3an 913	. . . . . 6 |- ((((B .ih B) .h A) -h ((A .ih B) .h B)) .ih A) = ((((B .ih B) .h A) .ih A) - (((A .ih B) .h B) .ih A))
39		ax-his3 8872	. . . . . . . . 9 |- (((B .ih B) e. CC /\ A e. H~ /\ A e. H~) -> (((B .ih B) .h A) .ih A) = ((B .ih B) x. (A .ih A)))
40	2, 3, 3, 39	mp3an 913	. . . . . . . 8 |- (((B .ih B) .h A) .ih A) = ((B .ih B) x. (A .ih A))
41	3, 3	hicl 8869	. . . . . . . . 9 |- (A .ih A) e. CC
42	2, 41	mulcom 5295	. . . . . . . 8 |- ((B .ih B) x. (A .ih A)) = ((A .ih A) x. (B .ih B))
43	40, 42	eqtr 1487	. . . . . . 7 |- (((B .ih B) .h A) .ih A) = ((A .ih A) x. (B .ih B))
44		ax-his3 8872	. . . . . . . 8 |- (((A .ih B) e. CC /\ B e. H~ /\ A e. H~) -> (((A .ih B) .h B) .ih A) = ((A .ih B) x. (B .ih A)))
45	5, 1, 3, 44	mp3an 913	. . . . . . 7 |- (((A .ih B) .h B) .ih A) = ((A .ih B) x.