Theorem h1de2b 5459

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
h1de2b	|- (-. B = 0v -> (A e. (_|_` (_|_` {B})) <-> A = (((A .i B) / (B .i B)) .s B)))

Proof of Theorem h1de2b

Step	Hyp	Ref	Expression
1		df-ne 1192	. . 3 |- ((B .i B) =/= 0 <-> -. (B .i B) = 0)
2		h1de2.2	. . . . 5 |- B e. H~
3		his6 5057	. . . . 5 |- (B e. H~ -> ((B .i B) = 0 <-> B = 0v))
4	2, 3	ax-mp 6	. . . 4 |- ((B .i B) = 0 <-> B = 0v)
5	4	negbii 162	. . 3 |- (-. (B .i B) = 0 <-> -. B = 0v)
6	1, 5	bitr 151	. 2 |- ((B .i B) =/= 0 <-> -. B = 0v)
7		h1de2.1	. . . . . . . 8 |- A e. H~
8	7, 2	h1de2 5458	. . . . . . 7 |- (A e. (_|_` (_|_` {B})) -> ((B .i B) .s A) = ((A .i B) .s B))
9	8	adantl 305	. . . . . 6 |- (((B .i B) =/= 0 /\ A e. (_|_` (_|_` {B}))) -> ((B .i B) .s A) = ((A .i B) .s B))
10	9	opreq2d 3013	. . . . 5 |- (((B .i B) =/= 0 /\ A e. (_|_` (_|_` {B}))) -> ((1 / (B .i B)) .s ((B .i B) .s A)) = ((1 / (B .i B)) .s ((A .i B) .s B)))
11		1cn 4101	. . . . . . . . . 10 |- 1 e. CC
12	2, 2	hicl 5044	. . . . . . . . . 10 |- (B .i B) e. CC
13	11, 12	divclz 4222	. . . . . . . . 9 |- ((B .i B) =/= 0 -> (1 / (B .i B)) e. CC)
14		ax-hvmulass 4992	. . . . . . . . . . 11 |- (((1 / (B .i B)) e. CC /\ (B .i B) e. CC /\ A e. H~) -> (((1 / (B .i B)) x. (B .i B)) .s A) = ((1 / (B .i B)) .s ((B .i B) .s A)))
15	12, 14	mp3an2 640	. . . . . . . . . 10 |- (((1 / (B .i B)) e. CC /\ A e. H~) -> (((1 / (B .i B)) x. (B .i B)) .s A) = ((1 / (B .i B)) .s ((B .i B) .s A)))
16	7, 15	mpan2 519	. . . . . . . . 9 |- ((1 / (B .i B)) e. CC -> (((1 / (B .i B)) x. (B .i B)) .s A) = ((1 / (B .i B)) .s ((B .i B) .s A)))
17	13, 16	syl 12	. . . . . . . 8 |- ((B .i B) =/= 0 -> (((1 / (B .i B)) x. (B .i B)) .s A) = ((1 / (B .i B)) .s ((B .i B) .s A)))
18	12, 11	divcan1z 4226	. . . . . . . . 9 |- ((B .i B) =/= 0 -> ((1 / (B .i B)) x. (B .i B)) = 1)
19	18	opreq1d 3012	. . . . . . . 8 |- ((B .i B) =/= 0 -> (((1 / (B .i B)) x. (B .i B)) .s A) = (1 .s A))
20	17, 19	eqtr3d 1130	. . . . . . 7 |- ((B .i B) =/= 0 -> ((1 / (B .i B)) .s ((B .i B) .s A)) = (1 .s A))
21		ax-hvmulid 4991	. . . . . . . 8 |- (A e. H~ -> (1 .s A) = A)
22	7, 21	ax-mp 6	. . . . . . 7 |- (1 .s A) = A
23	20, 22	syl6eq 1140	. . . . . 6 |- ((B .i B) =/= 0 -> ((1 / (B .i B)) .s ((B .i B) .s A)) = A)
24	23	adantr 306	. . . . 5 |- (((B .i B) =/= 0 /\ A e. (_|_` (_|_` {B}))) -> ((1 / (B .i B)) .s ((B .i B) .s A)) = A)
25	7, 2	hicl 5044	. . . . . . . . . 10 |- (A .i B) e. CC
26		ax-hvmulass 4992	. . . . . . . . . 10 |- (((1 / (B .i B)) e. CC /\ (A .i B) e. CC /\ B e. H~) -> (((1 / (B .i B)) x. (A .i B)) .s B) = ((1 / (B .i B)) .s ((A .i B) .s B)))
27	25, 26	mp3an2 640	. . . . . . . . 9 |- (((1 / (B .i B)) e. CC /\ B e. H~) -> (((1 / (B .i B)) x. (A .i B)) .s B) = ((1 / (B .i B)) .s ((A .i B) .s B)))
28	2, 27	mpan2 519	. . . . . . . 8 |- ((1 / (B .i B)) e. CC -> (((1 / (B .i B)) x. (A .i B)) .s B) = ((1 / (B .i B)) .s ((A .i B) .s B)))
29	13, 28	syl 12	. . . . . . 7 |- ((B .i B) =/= 0 -> (((1 / (B .i B)) x. (A .i B)) .s B) = ((1 / (B .i B)) .s ((A .i B) .s B)))
30		axmulcom 4071	. . . . . . . . . . 11 |- (((1 / (B .i B)) e. CC /\ (A .i B) e. CC) -> ((1 / (B .i B)) x. (A .i B)) = ((A .i B) x. (1 / (B .i B))))
31	25, 30	mpan2 519	. . . . . . . . . 10 |- ((1 / (B .i B)) e. CC -> ((1 / (B .i B)) x. (A .i B)) = ((A .i B) x. (1 / (B .i B))))
32	13, 31	syl 12	. . . . . . . . 9 |- ((B .i B) =/= 0 -> ((1 / (B .i B)) x. (A .i B)) = ((A .i B) x. (1 / (B .i B))))
33	25, 12	divrecz 4237	. . . . . . . . 9 |- ((B .i B) =/= 0 -> ((A .i B) / (B .i B)) = ((A .i B) x. (1 / (B .i B))))
34	32, 33	eqtr4d 1131	. . . . . . . 8 |- ((B .i B) =/= 0 -> ((1 / (B .i B)) x. (A .i B)) = ((A .i B) / (B .i B)))
35	34	opreq1d 3012	. . . . . . 7 |- ((B .i B) =/= 0 -> (((1 / (B .i B)) x. (A .i B)) .s B) = (((A .i B) / (B .i B)) .s B))
36	29, 35	eqtr3d 1130	. . . . . 6 |- ((B .i B) =/= 0 -> ((1 / (B .i B)) .s ((A .i B) .s B)) = (((A .i B) / (B .i B)) .s B))
37	36	adantr 306	. . . . 5 |- (((B .i B) =/= 0 /\ A e. (_|_` (_|_` {B}))) -> ((1 / (B .i B)) .s ((A .i B) .s B)) = (((A .i B) / (B .i B)) .s B))
38	10, 24, 37	3eqtr3d 1133	. . . 4 |- (((B .i B) =/= 0 /\ A e. (_|_` (_|_` {B}))) -> A = (((A .i B) / (B .i B)) .s B))
39	38	exp 291	. . 3 |- ((B .i B) =/= 0 -> (A e. (_|_` (_|_` {B})) -> A = (((A .i B) / (B .i B)) .s B)))
40		eleq1 1149	. . . . 5 |- (A = (((A .i B) / (B .i B)) .s B) -> (A e. (_|_` (_|_` {B})) <-> (((A .i B) / (B .i B)) .s B) e. (_|_` (_|_` {B}))))
41	25, 12	divclz 4222	. . . . . 6 |- ((B .i B) =/= 0 -> ((A .i B) / (B .i B)) e. CC)
42		h1did 5456	. . . . . . . 8 |- (B e. H~ -> B e. (_|_` (_|_` {B})))
43	2, 42	ax-mp 6	. . . . . . 7 |- B e. (_|_` (_|_` {B}))
44		snssi 1851	. . . . . . . . . . . 12 |- (B e. H~ -> {B} (_ H~)
45	2, 44	ax-mp 6	. . . . . . . . . . 11 |- {B} (_ H~
46	45	occl 5188	. . . . . . . . . 10 |- (_|_` {B}) e. CH
47	46	chocl 5192	. . . . . . . . 9 |- (_|_` (_|_` {B})) e. CH
48	47	chshi 5132	. . . . . . . 8 |- (_|_` (_|_` {B})) e. SH
49		shmulclt 5124	. . . . . . . 8 |- ((_|_` (_|_` {B})) e. SH -> ((((A .i B) / (B .i B)) e. CC /\ B e. (_|_` (_|_` {B}))) -> (((A .i B) / (B .i B)) .s B) e. (_|_` (_|_` {B}))))
50	48, 49	ax-mp 6	. . . . . . 7 |- ((((A .i B) / (B .i B)) e. CC /\ B e. (_|_` (_|_` {B}))) -> (((A .i B) / (B .i B)) .s B) e. (_|_` (_|_` {B})))
51	43, 50	mpan2 519	. . . . . 6 |- (((A .i B) / (B .i B)) e. CC -> (((A .i B) / (B .i B)) .s B) e. (_|_` (_|_` {B})))
52	41, 51	syl 12	. . . . 5 |- ((B .i B) =/= 0 -> (((A .i B) / (B .i B)) .s B) e. (_|_` (_|_` {B})))
53	40, 52	syl5bir 184	. . . 4 |- (A = (((A .i B) / (B .i B)) .s B) -> ((B .i B) =/= 0 -> A e. (_|_` (_|_` {B}))))
54	53	com12 13	. . 3 |- ((B .i B) =/= 0 -> (A = (((A .i B) / (B .i B)) .s B) -> A e. (_|_` (_|_` {B}))))
55	39, 54	impbid 397	. 2 |- ((B .i B) =/= 0 -> (A e. (_|_` (_|_` {B})) <-> A = (((A .i B) / (B .i B)) .s B)))
56	6, 55	sylbir 176	1 |- (-.