Theorem nmparlem

Description: Lemma for nmpar . (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	nmpar.v	$$⊢V={\mathrm{Base}}_W$$
	nmpar.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	nmpar.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	nmpar.n	$$⊢N=\mathrm{norm}\left(W\right)$$
	nmpar.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	nmpar.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	nmpar.k	$$⊢K={\mathrm{Base}}_F$$
	nmpar.1	$$⊢\phi \to W\in \mathrm{CPreHil}$$
	nmpar.2	$$⊢\phi \to A\in V$$
	nmpar.3	$$⊢\phi \to B\in V$$
Assertion	nmparlem	$$⊢\phi \to {N\left(A\underset{\dot{}}{+}B\right)}^2+{N\left(A\underset{\dot{}}{-}B\right)}^2=2\left({N\left(A\right)}^2+{N\left(B\right)}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmpar.v	$$⊢V={\mathrm{Base}}_W$$
2		nmpar.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		nmpar.m	$$⊢\underset{\dot{}}{-}={-}_W$$
4		nmpar.n	$$⊢N=\mathrm{norm}\left(W\right)$$
5		nmpar.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
6		nmpar.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
7		nmpar.k	$$⊢K={\mathrm{Base}}_F$$
8		nmpar.1	$$⊢\phi \to W\in \mathrm{CPreHil}$$
9		nmpar.2	$$⊢\phi \to A\in V$$
10		nmpar.3	$$⊢\phi \to B\in V$$
11	5 1 2 8 9 10 9 10	cph2di	$$⊢\phi \to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)$$
12	5 1 3 8 9 10 9 10	cph2subdi	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}B\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)-\left(\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)\right)$$
13	11 12	oveq12d	$$⊢\phi \to \left(\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)\right)+\left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}B\right)\right)=\left(\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)\right)+\left(\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)\right)+\left(\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)-\left(\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)\right)\right)$$
14		cphclm	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$
15	8 14	syl	$$⊢\phi \to W\in \mathrm{CMod}$$
16	6 7	clmsscn	$$⊢W\in \mathrm{CMod}\to K\subseteq ℂ$$
17	15 16	syl	$$⊢\phi \to K\subseteq ℂ$$
18		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
19	8 18	syl	$$⊢\phi \to W\in \mathrm{PreHil}$$
20	6 5 1 7	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge A\in V\right)\to A\underset{\dot{}}{,}A\in K$$
21	19 9 9 20	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}A\in K$$
22	6 5 1 7	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge B\in V\right)\to B\underset{\dot{}}{,}B\in K$$
23	19 10 10 22	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}B\in K$$
24	6 7	clmacl	$$⊢\left(W\in \mathrm{CMod}\wedge A\underset{\dot{}}{,}A\in K\wedge B\underset{\dot{}}{,}B\in K\right)\to \left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)\in K$$
25	15 21 23 24	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)\in K$$
26	17 25	sseldd	$$⊢\phi \to \left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)\in ℂ$$
27	6 5 1 7	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{,}B\in K$$
28	19 9 10 27	syl3anc	$$⊢\phi \to A\underset{\dot{}}{,}B\in K$$
29	6 5 1 7	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge B\in V\wedge A\in V\right)\to B\underset{\dot{}}{,}A\in K$$
30	19 10 9 29	syl3anc	$$⊢\phi \to B\underset{\dot{}}{,}A\in K$$
31	6 7	clmacl	$$⊢\left(W\in \mathrm{CMod}\wedge A\underset{\dot{}}{,}B\in K\wedge B\underset{\dot{}}{,}A\in K\right)\to \left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)\in K$$
32	15 28 30 31	syl3anc	$$⊢\phi \to \left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)\in K$$
33	17 32	sseldd	$$⊢\phi \to \left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)\in ℂ$$
34	26 33 26	ppncand	$$⊢\phi \to \left(\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)\right)+\left(\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)\right)+\left(\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)-\left(\left(A\underset{\dot{}}{,}B\right)+\left(B\underset{\dot{}}{,}A\right)\right)\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
35	13 34	eqtrd	$$⊢\phi \to \left(\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)\right)+\left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}B\right)\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
36		cphlmod	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{LMod}$$
37	8 36	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
38	1 2	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{+}B\in V$$
39	37 9 10 38	syl3anc	$$⊢\phi \to A\underset{\dot{}}{+}B\in V$$
40	1 5 4	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\underset{\dot{}}{+}B\in V\right)\to {N\left(A\underset{\dot{}}{+}B\right)}^2=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)$$
41	8 39 40	syl2anc	$$⊢\phi \to {N\left(A\underset{\dot{}}{+}B\right)}^2=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)$$
42	1 3	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{-}B\in V$$
43	37 9 10 42	syl3anc	$$⊢\phi \to A\underset{\dot{}}{-}B\in V$$
44	1 5 4	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\underset{\dot{}}{-}B\in V\right)\to {N\left(A\underset{\dot{}}{-}B\right)}^2=\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}B\right)$$
45	8 43 44	syl2anc	$$⊢\phi \to {N\left(A\underset{\dot{}}{-}B\right)}^2=\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}B\right)$$
46	41 45	oveq12d	$$⊢\phi \to {N\left(A\underset{\dot{}}{+}B\right)}^2+{N\left(A\underset{\dot{}}{-}B\right)}^2=\left(\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{+}B\right)\right)+\left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{,}\left(A\underset{\dot{}}{-}B\right)\right)$$
47	1 5 4	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to {N\left(A\right)}^2=A\underset{\dot{}}{,}A$$
48	8 9 47	syl2anc	$$⊢\phi \to {N\left(A\right)}^2=A\underset{\dot{}}{,}A$$
49	1 5 4	nmsq	$$⊢\left(W\in \mathrm{CPreHil}\wedge B\in V\right)\to {N\left(B\right)}^2=B\underset{\dot{}}{,}B$$
50	8 10 49	syl2anc	$$⊢\phi \to {N\left(B\right)}^2=B\underset{\dot{}}{,}B$$
51	48 50	oveq12d	$$⊢\phi \to {N\left(A\right)}^2+{N\left(B\right)}^2=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
52	51	oveq2d	$$⊢\phi \to 2\left({N\left(A\right)}^2+{N\left(B\right)}^2\right)=2\left(\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)\right)$$
53	26	2timesd	$$⊢\phi \to 2\left(\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
54	52 53	eqtrd	$$⊢\phi \to 2\left({N\left(A\right)}^2+{N\left(B\right)}^2\right)=\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)+\left(A\underset{\dot{}}{,}A\right)+\left(B\underset{\dot{}}{,}B\right)$$
55	35 46 54	3eqtr4d	$$⊢\phi \to {N\left(A\underset{\dot{}}{+}B\right)}^2+{N\left(A\underset{\dot{}}{-}B\right)}^2=2\left({N\left(A\right)}^2+{N\left(B\right)}^2\right)$$