Theorem sspival 8397

Description: The inner product on a subspace in terms of the inner product on the parent space.

Hypotheses

Ref	Expression
sspi.y	|- Y = (Base` W)
sspi.p	|- P = (.i` U)
sspi.q	|- Q = (.i` W)
sspi.h	|- H = (SubSp` U)

Assertion

Ref	Expression
sspival	|- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ B e. Y)) -> (AQB) = (APB))

Proof of Theorem sspival

Step	Hyp	Ref	Expression
1		sspi.y	. . . . . . . . . . . . . . . 16 |- Y = (Base` W)
2		eqid 1475	. . . . . . . . . . . . . . . 16 |- (.s` W) = (.s` W)
3	1, 2	nvscl 8247	. . . . . . . . . . . . . . 15 |- ((W e. NrmCVec /\ (i^k) e. CC /\ B e. Y) -> ((i^k)(.s` W)B) e. Y)
4	3	3expib 836	. . . . . . . . . . . . . 14 |- (W e. NrmCVec -> (((i^k) e. CC /\ B e. Y) -> ((i^k)(.s` W)B) e. Y))
5	4	anim2d 561	. . . . . . . . . . . . 13 |- (W e. NrmCVec -> ((A e. Y /\ ((i^k) e. CC /\ B e. Y)) -> (A e. Y /\ ((i^k)(.s` W)B) e. Y)))
6	5	imp 350	. . . . . . . . . . . 12 |- ((W e. NrmCVec /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> (A e. Y /\ ((i^k)(.s` W)B) e. Y))
7		eqid 1475	. . . . . . . . . . . . . 14 |- (+v` W) = (+v` W)
8	1, 7	nvgcl 8239	. . . . . . . . . . . . 13 |- ((W e. NrmCVec /\ A e. Y /\ ((i^k)(.s` W)B) e. Y) -> (A(+v` W)((i^k)(.s` W)B)) e. Y)
9	8	3expb 834	. . . . . . . . . . . 12 |- ((W e. NrmCVec /\ (A e. Y /\ ((i^k)(.s` W)B) e. Y)) -> (A(+v` W)((i^k)(.s` W)B)) e. Y)
10	6, 9	syldan 467	. . . . . . . . . . 11 |- ((W e. NrmCVec /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> (A(+v` W)((i^k)(.s` W)B)) e. Y)
11		sspi.h	. . . . . . . . . . . 12 |- H = (SubSp` U)
12	11	sspnv 8385	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ W e. H) -> W e. NrmCVec)
13	10, 12	sylan 448	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> (A(+v` W)((i^k)(.s` W)B)) e. Y)
14		eqid 1475	. . . . . . . . . . . 12 |- (norm` U) = (norm` U)
15		eqid 1475	. . . . . . . . . . . 12 |- (norm` W) = (norm` W)
16	1, 14, 15, 11	sspnval 8396	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ W e. H /\ (A(+v` W)((i^k)(.s` W)B)) e. Y) -> ((norm` W)` (A(+v` W)((i^k)(.s` W)B))) = ((norm` U)` (A(+v` W)((i^k)(.s` W)B))))
17	16	3expa 833	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. H) /\ (A(+v` W)((i^k)(.s` W)B)) e. Y) -> ((norm` W)` (A(+v` W)((i^k)(.s` W)B))) = ((norm` U)` (A(+v` W)((i^k)(.s` W)B))))
18	13, 17	syldan 467	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> ((norm` W)` (A(+v` W)((i^k)(.s` W)B))) = ((norm` U)` (A(+v` W)((i^k)(.s` W)B))))
19	12, 4	syl 10	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ W e. H) -> (((i^k) e. CC /\ B e. Y) -> ((i^k)(.s` W)B) e. Y))
20	19	anim2d 561	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ W e. H) -> ((A e. Y /\ ((i^k) e. CC /\ B e. Y)) -> (A e. Y /\ ((i^k)(.s` W)B) e. Y)))
21	20	imp 350	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> (A e. Y /\ ((i^k)(.s` W)B) e. Y))
22		eqid 1475	. . . . . . . . . . . . 13 |- (+v` U) = (+v` U)
23	1, 22, 7, 11	sspgval 8388	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k)(.s` W)B) e. Y)) -> (A(+v` W)((i^k)(.s` W)B)) = (A(+v` U)((i^k)(.s` W)B)))
24	21, 23	syldan 467	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> (A(+v` W)((i^k)(.s` W)B)) = (A(+v` U)((i^k)(.s` W)B)))
25		eqid 1475	. . . . . . . . . . . . . 14 |- (.s` U) = (.s` U)
26	1, 25, 2, 11	sspsval 8390	. . . . . . . . . . . . 13 |- (((U e. NrmCVec /\ W e. H) /\ ((i^k) e. CC /\ B e. Y)) -> ((i^k)(.s` W)B) = ((i^k)(.s` U)B))
27	26	adantrl 394	. . . . . . . . . . . 12 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> ((i^k)(.s` W)B) = ((i^k)(.s` U)B))
28	27	opreq2d 3976	. . . . . . . . . . 11 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> (A(+v` U)((i^k)(.s` W)B)) = (A(+v` U)((i^k)(.s` U)B)))
29	24, 28	eqtrd 1507	. . . . . . . . . 10 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> (A(+v` W)((i^k)(.s` W)B)) = (A(+v` U)((i^k)(.s` U)B)))
30	29	fveq2d 3728	. . . . . . . . 9 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> ((norm` U)` (A(+v` W)((i^k)(.s` W)B))) = ((norm` U)` (A(+v` U)((i^k)(.s` U)B))))
31	18, 30	eqtrd 1507	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ ((i^k) e. CC /\ B e. Y))) -> ((norm` W)` (A(+v` W)((i^k)(.s` W)B))) = ((norm` U)` (A(+v` U)((i^k)(.s` U)B))))
32		elfznnt 6494	. . . . . . . . . . . . 13 |- (k e. (1...4) -> k e. NN)
33		nnnn0t 6106	. . . . . . . . . . . . 13 |- (k e. NN -> k e. NN0)
34		axicn 5270	. . . . . . . . . . . . . 14 |- i e. CC
35		expclt 6581	. . . . . . . . . . . . . 14 |- ((i e. CC /\ k e. NN0) -> (i^k) e. CC)
36	34, 35	mpan 695	. . . . . . . . . . . . 13 |- (k e. NN0 -> (i^k) e. CC)
37	32, 33, 36	3syl 20	. . . . . . . . . . . 12 |- (k e. (1...4) -> (i^k) e. CC)
38	37	anim1i 334	. . . . . . . . . . 11 |- ((k e. (1...4) /\ B e. Y) -> ((i^k) e. CC /\ B e. Y))
39	38	anim2i 335	. . . . . . . . . 10 |- ((A e. Y /\ (k e. (1...4) /\ B e. Y)) -> (A e. Y /\ ((i^k) e. CC /\ B e. Y)))
40	39	anassrs 441	. . . . . . . . 9 |- (((A e. Y /\ k e. (1...4)) /\ B e. Y) -> (A e. Y /\ ((i^k) e. CC /\ B e. Y)))
41	40	an1rs 489	. . . . . . . 8 |- (((A e. Y /\ B e. Y) /\ k e. (1...4)) -> (A e. Y /\ ((i^k) e. CC /\ B e. Y)))
42	31, 41	sylan2 451	. . . . . . 7 |- (((U e. NrmCVec /\ W e. H) /\ ((A e. Y /\ B e. Y) /\ k e. (1...4))) -> ((norm` W)` (A(+v` W)((i^k)(.s` W)B))) = ((norm` U)` (A(+v` U)((i^k)(.s` U)B))))
43	42	anassrs 441	. . . . . 6 |- ((((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ B e. Y)) /\ k e. (1...4)) -> ((norm` W)` (A(+v` W)((i^k)(.s` W)B))) = ((norm` U)` (A(+v` U)((i^k)(.s` U)B))))
44	43	opreq1d 3975	. . . . 5 |- ((((U e. NrmCVec /\ W e. H) /\ (A e. Y /\ B e. Y)) /\ k e. (1...4)) -> (((norm` W)` (A(+v` W)((i^k)(.s` W)B)))