ncvspi

Description: The norm of a vector plus the imaginary scalar product of another. (Contributed by NM, 2-Feb-2007) (Revised by AV, 8-Oct-2021)

	Ref	Expression
Hypotheses	ncvsprp.v	$⊢ V = {Base}_{W}$
	ncvsprp.n	$⊢ N = norm (W)$
	ncvsprp.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	ncvsdif.p	$⊢ \underset{˙}{+} = +_{W}$
	ncvspi.f	$⊢ F = Scalar (W)$
	ncvspi.k	$⊢ K = {Base}_{F}$
Assertion	ncvspi	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = N (B \underset{˙}{+} ((- i) \underset{˙}{\cdot} A))$

Proof

Step	Hyp	Ref	Expression
1		ncvsprp.v	$⊢ V = {Base}_{W}$
2		ncvsprp.n	$⊢ N = norm (W)$
3		ncvsprp.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		ncvsdif.p	$⊢ \underset{˙}{+} = +_{W}$
5		ncvspi.f	$⊢ F = Scalar (W)$
6		ncvspi.k	$⊢ K = {Base}_{F}$
7		elin	$⊢ W \in (NrmVec \cap ℂVec) \leftrightarrow (W \in NrmVec \land W \in ℂVec)$
8		nvcnlm	$⊢ W \in NrmVec \to W \in NrmMod$
9		nlmngp	$⊢ W \in NrmMod \to W \in NrmGrp$
10	8 9	syl	$⊢ W \in NrmVec \to W \in NrmGrp$
11	10	adantr	$⊢ (W \in NrmVec \land W \in ℂVec) \to W \in NrmGrp$
12	7 11	sylbi	$⊢ W \in (NrmVec \cap ℂVec) \to W \in NrmGrp$
13	12	3ad2ant1	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to W \in NrmGrp$
14		nvclmod	$⊢ W \in NrmVec \to W \in LMod$
15		lmodgrp	$⊢ W \in LMod \to W \in Grp$
16	14 15	syl	$⊢ W \in NrmVec \to W \in Grp$
17	16	adantr	$⊢ (W \in NrmVec \land W \in ℂVec) \to W \in Grp$
18	7 17	sylbi	$⊢ W \in (NrmVec \cap ℂVec) \to W \in Grp$
19	18	3ad2ant1	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to W \in Grp$
20		simp2l	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to A \in V$
21		id	$⊢ W \in ℂVec \to W \in ℂVec$
22	21	cvsclm	$⊢ W \in ℂVec \to W \in CMod$
23	7 22	simplbiim	$⊢ W \in (NrmVec \cap ℂVec) \to W \in CMod$
24	23	3ad2ant1	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to W \in CMod$
25		simp3	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to i \in K$
26		simp2r	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to B \in V$
27	1 5 3 6	clmvscl	$⊢ (W \in CMod \land i \in K \land B \in V) \to i \underset{˙}{\cdot} B \in V$
28	24 25 26 27	syl3anc	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to i \underset{˙}{\cdot} B \in V$
29	1 4	grpcl	$⊢ (W \in Grp \land A \in V \land i \underset{˙}{\cdot} B \in V) \to A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in V$
30	19 20 28 29	syl3anc	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in V$
31	1 2	nmcl	$⊢ (W \in NrmGrp \land A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in V) \to N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in ℝ$
32	13 30 31	syl2anc	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in ℝ$
33	32	recnd	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) \in ℂ$
34	33	mulid2d	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to 1 N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))$
35		ax-icn	$⊢ i \in ℂ$
36	35	absnegi	$⊢ \|- i\| = \|i\|$
37		absi	$⊢ \|i\| = 1$
38	36 37	eqtri	$⊢ \|- i\| = 1$
39	38	oveq1i	$⊢ \|- i\| N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = 1 N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))$
40		simp1	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to W \in (NrmVec \cap ℂVec)$
41	5 6	clmneg	$⊢ (W \in CMod \land i \in K) \to - i = {inv}_{g} (F) (i)$
42	22 41	sylan	$⊢ (W \in ℂVec \land i \in K) \to - i = {inv}_{g} (F) (i)$
43	5	clmfgrp	$⊢ W \in CMod \to F \in Grp$
44	22 43	syl	$⊢ W \in ℂVec \to F \in Grp$
45		eqid	$⊢ {inv}_{g} (F) = {inv}_{g} (F)$
46	6 45	grpinvcl	$⊢ (F \in Grp \land i \in K) \to {inv}_{g} (F) (i) \in K$
47	44 46	sylan	$⊢ (W \in ℂVec \land i \in K) \to {inv}_{g} (F) (i) \in K$
48	42 47	eqeltrd	$⊢ (W \in ℂVec \land i \in K) \to - i \in K$
49	48	ex	$⊢ W \in ℂVec \to (i \in K \to - i \in K)$
50	7 49	simplbiim	$⊢ W \in (NrmVec \cap ℂVec) \to (i \in K \to - i \in K)$
51	50	imp	$⊢ (W \in (NrmVec \cap ℂVec) \land i \in K) \to - i \in K$
52	51	3adant2	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to - i \in K$
53	1 2 3 5 6	ncvsprp	$⊢ (W \in (NrmVec \cap ℂVec) \land - i \in K \land A \underset{˙}{+} (i \underset{˙}{\cdot} B) \in V) \to N ((- i) \underset{˙}{\cdot} (A \underset{˙}{+} (i \underset{˙}{\cdot} B))) = \|- i\| N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))$
54	40 52 30 53	syl3anc	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to N ((- i) \underset{˙}{\cdot} (A \underset{˙}{+} (i \underset{˙}{\cdot} B))) = \|- i\| N (A \underset{˙}{+} (i \underset{˙}{\cdot} B))$
55	1 5 3 6 4	clmvsdi	$⊢ (W \in CMod \land (- i \in K \land A \in V \land i \underset{˙}{\cdot} B \in V)) \to (- i) \underset{˙}{\cdot} (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = ((- i) \underset{˙}{\cdot} A) \underset{˙}{+} ((- i) \underset{˙}{\cdot} (i \underset{˙}{\cdot} B))$
56	24 52 20 28 55	syl13anc	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to (- i) \underset{˙}{\cdot} (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = ((- i) \underset{˙}{\cdot} A) \underset{˙}{+} ((- i) \underset{˙}{\cdot} (i \underset{˙}{\cdot} B))$
57	35 35	mulneg1i	$⊢ (- i) i = - i i$
58		ixi	$⊢ i i = - 1$
59	58	negeqi	$⊢ - i i = - -1$
60		negneg1e1	$⊢ - -1 = 1$
61	59 60	eqtri	$⊢ - i i = 1$
62	57 61	eqtri	$⊢ (- i) i = 1$
63	62	oveq1i	$⊢ (- i) i \underset{˙}{\cdot} B = 1 \underset{˙}{\cdot} B$
64	1 5 3 6	clmvsass	$⊢ (W \in CMod \land (- i \in K \land i \in K \land B \in V)) \to (- i) i \underset{˙}{\cdot} B = (- i) \underset{˙}{\cdot} (i \underset{˙}{\cdot} B)$
65	24 52 25 26 64	syl13anc	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to (- i) i \underset{˙}{\cdot} B = (- i) \underset{˙}{\cdot} (i \underset{˙}{\cdot} B)$
66		simpr	$⊢ (A \in V \land B \in V) \to B \in V$
67	23 66	anim12i	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V)) \to (W \in CMod \land B \in V)$
68	67	3adant3	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to (W \in CMod \land B \in V)$
69	1 3	clmvs1	$⊢ (W \in CMod \land B \in V) \to 1 \underset{˙}{\cdot} B = B$
70	68 69	syl	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to 1 \underset{˙}{\cdot} B = B$
71	63 65 70	3eqtr3a	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to (- i) \underset{˙}{\cdot} (i \underset{˙}{\cdot} B) = B$
72	71	oveq2d	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to ((- i) \underset{˙}{\cdot} A) \underset{˙}{+} ((- i) \underset{˙}{\cdot} (i \underset{˙}{\cdot} B)) = ((- i) \underset{˙}{\cdot} A) \underset{˙}{+} B$
73		clmabl	$⊢ W \in CMod \to W \in Abel$
74	22 73	syl	$⊢ W \in ℂVec \to W \in Abel$
75	7 74	simplbiim	$⊢ W \in (NrmVec \cap ℂVec) \to W \in Abel$
76	75	3ad2ant1	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to W \in Abel$
77	1 5 3 6	clmvscl	$⊢ (W \in CMod \land - i \in K \land A \in V) \to (- i) \underset{˙}{\cdot} A \in V$
78	24 52 20 77	syl3anc	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to (- i) \underset{˙}{\cdot} A \in V$
79	1 4	ablcom	$⊢ (W \in Abel \land (- i) \underset{˙}{\cdot} A \in V \land B \in V) \to ((- i) \underset{˙}{\cdot} A) \underset{˙}{+} B = B \underset{˙}{+} ((- i) \underset{˙}{\cdot} A)$
80	76 78 26 79	syl3anc	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to ((- i) \underset{˙}{\cdot} A) \underset{˙}{+} B = B \underset{˙}{+} ((- i) \underset{˙}{\cdot} A)$
81	56 72 80	3eqtrd	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to (- i) \underset{˙}{\cdot} (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = B \underset{˙}{+} ((- i) \underset{˙}{\cdot} A)$
82	81	fveq2d	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to N ((- i) \underset{˙}{\cdot} (A \underset{˙}{+} (i \underset{˙}{\cdot} B))) = N (B \underset{˙}{+} ((- i) \underset{˙}{\cdot} A))$
83	54 82	eqtr3d	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to \|- i\| N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = N (B \underset{˙}{+} ((- i) \underset{˙}{\cdot} A))$
84	39 83	syl5eqr	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to 1 N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = N (B \underset{˙}{+} ((- i) \underset{˙}{\cdot} A))$
85	34 84	eqtr3d	$⊢ (W \in (NrmVec \cap ℂVec) \land (A \in V \land B \in V) \land i \in K) \to N (A \underset{˙}{+} (i \underset{˙}{\cdot} B)) = N (B \underset{˙}{+} ((- i) \underset{˙}{\cdot} A))$

Metamath Proof Explorer

Theorem ncvspi

Proof