Theorem nvpi 10647

Description: The norm of a vector plus the imaginary scalar product of another.

Hypotheses

Ref	Expression
nvdif.1	|- X = (BaseSet` U)
nvdif.2	|- G = (+v` U)
nvdif.4	|- S = (.s` U)
nvdif.6	|- N = (norm` U)

Assertion

Ref	Expression
nvpi	|- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(_iSB))) = (N` (BG(-u_iSA))))

Proof of Theorem nvpi

Step	Hyp	Ref	Expression
1		simp1 1148	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> U e. NrmCVec)
2		ax-icn 6888	. . . . . . . 8 |- _i e. CC
3		nvdif.1	. . . . . . . . 9 |- X = (BaseSet` U)
4		nvdif.4	. . . . . . . . 9 |- S = (.s` U)
5	3, 4	nvscl 10600	. . . . . . . 8 |- ((U e. NrmCVec /\ _i e. CC /\ B e. X) -> (_iSB) e. X)
6	2, 5	mp3an2 1482	. . . . . . 7 |- ((U e. NrmCVec /\ B e. X) -> (_iSB) e. X)
7	6	3adant2 1167	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (_iSB) e. X)
8		nvdif.2	. . . . . . 7 |- G = (+v` U)
9	3, 8	nvgcl 10592	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ (_iSB) e. X) -> (AG(_iSB)) e. X)
10	7, 9	syld3an3 1422	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (AG(_iSB)) e. X)
11		nvdif.6	. . . . . 6 |- N = (norm` U)
12	3, 11	nvcl 10640	. . . . 5 |- ((U e. NrmCVec /\ (AG(_iSB)) e. X) -> (N` (AG(_iSB))) e. RR)
13	1, 10, 12	syl11anc 755	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(_iSB))) e. RR)
14	13	recnd 6921	. . 3 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(_iSB))) e. CC)
15		mulid2 7059	. . 3 |- ((N` (AG(_iSB))) e. CC -> (1 x. (N` (AG(_iSB)))) = (N` (AG(_iSB))))
16	14, 15	syl 13	. 2 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (1 x. (N` (AG(_iSB)))) = (N` (AG(_iSB))))
17	2	absnegi 8595	. . . . 5 |- (abs` -u_i) = (abs` _i)
18		absi 8630	. . . . 5 |- (abs` _i) = 1
19	17, 18	eqtri 2190	. . . 4 |- (abs` -u_i) = 1
20	19	opreq1i 5028	. . 3 |- ((abs` -u_i) x. (N` (AG(_iSB)))) = (1 x. (N` (AG(_iSB))))
21	2	negcli 7124	. . . . . 6 |- -u_i e. CC
22	3, 4, 11	nvs 10643	. . . . . 6 |- ((U e. NrmCVec /\ -u_i e. CC /\ (AG(_iSB)) e. X) -> (N` (-u_iS(AG(_iSB)))) = ((abs` -u_i) x. (N` (AG(_iSB)))))
23	21, 22	mp3an2 1482	. . . . 5 |- ((U e. NrmCVec /\ (AG(_iSB)) e. X) -> (N` (-u_iS(AG(_iSB)))) = ((abs` -u_i) x. (N` (AG(_iSB)))))
24	1, 10, 23	syl11anc 755	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (-u_iS(AG(_iSB)))) = ((abs` -u_i) x. (N` (AG(_iSB)))))
25		simp2 1149	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> A e. X)
26	3, 8, 4	nvdi 10604	. . . . . . . 8 |- ((U e. NrmCVec /\ (-u_i e. CC /\ A e. X /\ (_iSB) e. X)) -> (-u_iS(AG(_iSB))) = ((-u_iSA)G(-u_iS(_iSB))))
27	21, 26	mp3anr1 1491	. . . . . . 7 |- ((U e. NrmCVec /\ (A e. X /\ (_iSB) e. X)) -> (-u_iS(AG(_iSB))) = ((-u_iSA)G(-u_iS(_iSB))))
28	1, 25, 7, 27	syl12anc 1375	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-u_iS(AG(_iSB))) = ((-u_iSA)G(-u_iS(_iSB))))
29	3, 4	nvsass 10602	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (-u_i e. CC /\ _i e. CC /\ B e. X)) -> ((-u_i x. _i)SB) = (-u_iS(_iSB)))
30	21, 29	mp3anr1 1491	. . . . . . . . . 10 |- ((U e. NrmCVec /\ (_i e. CC /\ B e. X)) -> ((-u_i x. _i)SB) = (-u_iS(_iSB)))
31	2, 30	mpanr1 792	. . . . . . . . 9 |- ((U e. NrmCVec /\ B e. X) -> ((-u_i x. _i)SB) = (-u_iS(_iSB)))
32	2, 2	mulneg1i 7184	. . . . . . . . . . . 12 |- (-u_i x. _i) = -u(_i x. _i)
33		ixi 7307	. . . . . . . . . . . . 13 |- (_i x. _i) = -u1
34	33	negeqi 7115	. . . . . . . . . . . 12 |- -u(_i x. _i) = -u-u1
35		ax-1cn 6887	. . . . . . . . . . . . 13 |- 1 e. CC
36	35	negnegi 7145	. . . . . . . . . . . 12 |- -u-u1 = 1
37	32, 34, 36	3eqtri 2194	. . . . . . . . . . 11 |- (-u_i x. _i) = 1
38	37	opreq1i 5028	. . . . . . . . . 10 |- ((-u_i x. _i)SB) = (1SB)
39	3, 4	nvsid 10601	. . . . . . . . . 10 |- ((U e. NrmCVec /\ B e. X) -> (1SB) = B)
40	38, 39	syl5eq 2214	. . . . . . . . 9 |- ((U e. NrmCVec /\ B e. X) -> ((-u_i x. _i)SB) = B)
41	31, 40	eqtr3d 2204	. . . . . . . 8 |- ((U e. NrmCVec /\ B e. X) -> (-u_iS(_iSB)) = B)
42	41	3adant2 1167	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-u_iS(_iSB)) = B)
43	42	opreq2d 5033	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((-u_iSA)G(-u_iS(_iSB))) = ((-u_iSA)GB))
44	3, 4	nvscl 10600	. . . . . . . . 9 |- ((U e. NrmCVec /\ -u_i e. CC /\ A e. X) -> (-u_iSA) e. X)
45	21, 44	mp3an2 1482	. . . . . . . 8 |- ((U e. NrmCVec /\ A e. X) -> (-u_iSA) e. X)
46	45	3adant3 1168	. . . . . . 7 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-u_iSA) e. X)
47	3, 8	nvcom 10593	. . . . . . 7 |- ((U e. NrmCVec /\ (-u_iSA) e. X /\ B e. X) -> ((-u_iSA)GB) = (BG(-u_iSA)))
48	46, 47	syld3an2 1424	. . . . . 6 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((-u_iSA)GB) = (BG(-u_iSA)))
49	28, 43, 48	3eqtrd 2206	. . . . 5 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (-u_iS(AG(_iSB))) = (BG(-u_iSA)))
50	49	fveq2d 4808	. . . 4 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (-u_iS(AG(_iSB)))) = (N` (BG(-u_iSA))))
51	24, 50	eqtr3d 2204	. . 3 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> ((abs` -u_i) x. (N` (AG(_iSB)))) = (N` (BG(-u_iSA))))
52	20, 51	syl5eqr 2218	. 2 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (1 x. (N` (AG(_iSB)))) = (N` (BG(-u_iSA))))
53	16, 52	eqtr3d 2204	1 |- ((U e. NrmCVec /\ A e. X /\ B e. X) -> (N` (AG(_iSB))) = (N` (BG(-u_iSA))))

Syntax hints:   -> wi 3   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617  ` cfv 4163  (class class class)co 5020  CCcc 6827  RRcr 6828  1c1 6830  _ici 6831   x. cmul 6834  -ucneg 7092  abscabs 8500  NrmCVeccnv 10556  +vcpv 10557  BaseSetcba 10558  .scns 10559  normcnm 10562

This theorem is referenced by:  ipcj 10727

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906  ax-pre-sup 6907

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-id 3779  df-po 3784  df-so 3796  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-1st 5166  df-2nd 5167  df-iota 5259  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-sup 5932  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-div 7325  df-sqr 8420  df-re 8501  df-im 8502  df-cj 8503  df-abs 8504  df-grpo 10334  df-gid 10335  df-ablo 10429  df-vc 10518  df-nv 10564  df-va 10567  df-ba 10568  df-sm 10569  df-0v 10570  df-nm 10572

Copyright terms: Public domain