Theorem ubthlem8 8532

Description: Lemma for ubthi 8540. Compute x in terms of auxiliary vector Q.

Hypotheses

Ref	Expression
ubthlem7.1	|- X = (Base` U)
ubthlem7.7	|- U e. NrmCVec
ubthlem7.n	|- L = (norm` U)
ubthlem7.g	|- G = (+v` U)
ubthlem7.m	|- M = (-v` U)
ubthlem7.r	|- R = (.s` U)
ubthlem7.z	|- Z = (0v` U)
ubthlem7.q	|- Q = (pG(((r / 2) x. (1 / (L` x)))Rx))

Assertion

Ref	Expression
ubthlem8	|- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> x = (((2 / r) x. (L` x))R(QMp)))

Proof of Theorem ubthlem8

Step	Hyp	Ref	Expression
1		ubthlem7.7	. . . . 5 |- U e. NrmCVec
2		ubthlem7.1	. . . . . 6 |- X = (Base` U)
3		ubthlem7.r	. . . . . 6 |- R = (.s` U)
4	2, 3	nvsid 8244	. . . . 5 |- ((U e. NrmCVec /\ x e. X) -> (1Rx) = x)
5	1, 4	mpan 697	. . . 4 |- (x e. X -> (1Rx) = x)
6	5	ad2antrl 408	. . 3 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> (1Rx) = x)
7	6	adantl 390	. 2 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> (1Rx) = x)
8		ubthlem7.q	. . . . . 6 |- Q = (pG(((r / 2) x. (1 / (L` x)))Rx))
9	8	eqcomi 1482	. . . . 5 |- (pG(((r / 2) x. (1 / (L` x)))Rx)) = Q
10		ubthlem7.g	. . . . . . . 8 |- G = (+v` U)
11		ubthlem7.m	. . . . . . . 8 |- M = (-v` U)
12	2, 10, 11	nvsubadd 8271	. . . . . . 7 |- ((U e. NrmCVec /\ (Q e. X /\ p e. X /\ (((r / 2) x. (1 / (L` x)))Rx) e. X)) -> ((QMp) = (((r / 2) x. (1 / (L` x)))Rx) <-> (pG(((r / 2) x. (1 / (L` x)))Rx)) = Q))
13	1, 12	mpan 697	. . . . . 6 |- ((Q e. X /\ p e. X /\ (((r / 2) x. (1 / (L` x)))Rx) e. X) -> ((QMp) = (((r / 2) x. (1 / (L` x)))Rx) <-> (pG(((r / 2) x. (1 / (L` x)))Rx)) = Q))
14		ubthlem7.n	. . . . . . . 8 |- L = (norm` U)
15		ubthlem7.z	. . . . . . . 8 |- Z = (0v` U)
16	2, 1, 14, 10, 11, 3, 15, 8	ubthlem7 8531	. . . . . . 7 |- ((p e. X /\ (r e. RR /\ (x e. X /\ x =/= Z))) -> Q e. X)
17	16	adantrlr 403	. . . . . 6 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> Q e. X)
18		pm3.26 319	. . . . . 6 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> p e. X)
19	2, 3	nvscl 8243	. . . . . . . . . 10 |- ((U e. NrmCVec /\ ((r / 2) x. (1 / (L` x))) e. CC /\ x e. X) -> (((r / 2) x. (1 / (L` x)))Rx) e. X)
20	1, 19	mp3an1 905	. . . . . . . . 9 |- ((((r / 2) x. (1 / (L` x))) e. CC /\ x e. X) -> (((r / 2) x. (1 / (L` x)))Rx) e. X)
21		axmulcl 5285	. . . . . . . . . 10 |- (((r / 2) e. CC /\ (1 / (L` x)) e. CC) -> ((r / 2) x. (1 / (L` x))) e. CC)
22		rehalfclt 6036	. . . . . . . . . . 11 |- (r e. RR -> (r / 2) e. RR)
23	22	recnd 5327	. . . . . . . . . 10 |- (r e. RR -> (r / 2) e. CC)
24		recclt 5727	. . . . . . . . . . 11 |- (((L` x) e. CC /\ (L` x) =/= 0) -> (1 / (L` x)) e. CC)
25	2, 14	nvcl 8283	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ x e. X) -> (L` x) e. RR)
26	1, 25	mpan 697	. . . . . . . . . . . . 13 |- (x e. X -> (L` x) e. RR)
27	26	recnd 5327	. . . . . . . . . . . 12 |- (x e. X -> (L` x) e. CC)
28	27	adantr 391	. . . . . . . . . . 11 |- ((x e. X /\ x =/= Z) -> (L` x) e. CC)
29	2, 15, 14	nvz 8293	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ x e. X) -> ((L` x) = 0 <-> x = Z))
30	1, 29	mpan 697	. . . . . . . . . . . . 13 |- (x e. X -> ((L` x) = 0 <-> x = Z))
31	30	necon3bid 1604	. . . . . . . . . . . 12 |- (x e. X -> ((L` x) =/= 0 <-> x =/= Z))
32	31	biimpar 419	. . . . . . . . . . 11 |- ((x e. X /\ x =/= Z) -> (L` x) =/= 0)
33	24, 28, 32	sylanc 473	. . . . . . . . . 10 |- ((x e. X /\ x =/= Z) -> (1 / (L` x)) e. CC)
34	21, 23, 33	syl2an 456	. . . . . . . . 9 |- ((r e. RR /\ (x e. X /\ x =/= Z)) -> ((r / 2) x. (1 / (L` x))) e. CC)
35		simprl 416	. . . . . . . . 9 |- ((r e. RR /\ (x e. X /\ x =/= Z)) -> x e. X)
36	20, 34, 35	sylanc 473	. . . . . . . 8 |- ((r e. RR /\ (x e. X /\ x =/= Z)) -> (((r / 2) x. (1 / (L` x)))Rx) e. X)
37	36	adantlr 395	. . . . . . 7 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> (((r / 2) x. (1 / (L` x)))Rx) e. X)
38	37	adantl 390	. . . . . 6 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> (((r / 2) x. (1 / (L` x)))Rx) e. X)
39	13, 17, 18, 38	syl3anc 860	. . . . 5 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> ((QMp) = (((r / 2) x. (1 / (L` x)))Rx) <-> (pG(((r / 2) x. (1 / (L` x)))Rx)) = Q))
40	9, 39	mpbiri 194	. . . 4 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> (QMp) = (((r / 2) x. (1 / (L` x)))Rx))
41	40	opreq2d 3982	. . 3 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> (((2 / r) x. (L` x))R(QMp)) = (((2 / r) x. (L` x))R(((r / 2) x. (1 / (L` x)))Rx)))
42	2, 3	nvsass 8245	. . . . . 6 |- ((U e. NrmCVec /\ (((2 / r) x. (L` x)) e. CC /\ ((r / 2) x. (1 / (L` x))) e. CC /\ x e. X)) -> ((((2 / r) x. (L` x)) x. ((r / 2) x. (1 / (L` x))))Rx) = (((2 / r) x. (L` x))R(((r / 2) x. (1 / (L` x)))Rx)))
43	1, 42	mpan 697	. . . . 5 |- ((((2 / r) x. (L` x)) e. CC /\ ((r / 2) x. (1 / (L` x))) e. CC /\ x e. X) -> ((((2 / r) x. (L` x)) x. ((r / 2) x. (1 / (L` x))))Rx) = (((2 / r) x. (L` x))R(((r / 2) x. (1 / (L` x)))Rx)))
44		axmulcl 5285	. . . . . 6 |- (((2 / r) e. CC /\ (L` x) e. CC) -> ((2 / r) x. (L` x)) e. CC)
45		2cn 5982	. . . . . . . 8 |- 2 e. CC
46		divclt 5724	. . . . . . . 8 |- ((2 e. CC /\ r e. CC /\ r =/= 0) -> (2 / r) e. CC)
47	45, 46	mp3an1 905	. . . . . . 7 |- ((r e. CC /\ r =/= 0) -> (2 / r) e. CC)
48		pm3.26 319	. . . . . . . 8 |- ((r e. RR /\ 0 < r) -> r e. RR)
49	48	recnd 5327	. . . . . . 7 |- ((r e. RR /\ 0 < r) -> r e. CC)
50		gt0ne0t 5630	. . . . . . 7 |- ((r e. RR /\ 0 < r) -> r =/= 0)
51	47, 49, 50	sylanc 473	. . . . . 6 |- ((r e. RR /\ 0 < r) -> (2 / r) e. CC)
52	44, 51, 28	syl2an 456	. . . . 5 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> ((2 / r) x. (L` x)) e. CC)
53	23	adantr 391	. . . . . 6 |- ((r e. RR /\ 0 < r) -> (r / 2) e. CC)
54	21, 53, 33	syl2an 456	. . . . 5 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> ((r / 2) x. (1 / (L` x))) e. CC)
55		simprl 416	. . . . 5 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> x e. X)
56	43, 52, 54, 55	syl3anc 860	. . . 4 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> ((((2 / r) x. (L` x)) x. ((r / 2) x. (1 / (L` x))))Rx) = (((2 /