Theorem osumlem2 5531

Description: Lemma for osum 5538.

Hypotheses

Ref	Expression
osumlem1.1	|- A e. CH
osumlem1.2	|- B e. CH
osumlem1.3	|- B (_ (_|_` A)
osumlem1.4	|- (ph <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))

Assertion

Ref	Expression
osumlem2	|- (ph -> (((norm` (C -v x))^2) + ((norm` (D -v y))^2)) = ((norm` (R -v z))^2))

Proof of Theorem osumlem2

Step	Hyp	Ref	Expression
1		osumlem1.4	. 2 |- (ph <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))
2		pm3.27 260	. . . . . . 7 |- (((C e. A /\ D e. B) /\ R = (C +v D)) -> R = (C +v D))
3		pm3.27 260	. . . . . . 7 |- (((x e. A /\ y e. (_|_` A)) /\ z = (x +v y)) -> z = (x +v y))
4	2, 3	opreqan12d 3015	. . . . . 6 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (R -v z) = ((C +v D) -v (x +v y)))
5		osumlem1.1	. . . . . . . 8 |- A e. CH
6		osumlem1.2	. . . . . . . 8 |- B e. CH
7		osumlem1.3	. . . . . . . 8 |- B (_ (_|_` A)
8		pm4.2 148	. . . . . . . 8 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) <-> (((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))
9	5, 6, 7, 8	osumlem1 5530	. . . . . . 7 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)))
10		hvsub4t 5014	. . . . . . . . 9 |- (((C e. H~ /\ D e. H~) /\ (x e. H~ /\ y e. H~)) -> ((C +v D) -v (x +v y)) = ((C -v x) +v (D -v y)))
11	10	adantlr 310	. . . . . . . 8 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ (x e. H~ /\ y e. H~)) -> ((C +v D) -v (x +v y)) = ((C -v x) +v (D -v y)))
12	11	adantrr 312	. . . . . . 7 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((C +v D) -v (x +v y)) = ((C -v x) +v (D -v y)))
13	9, 12	syl 12	. . . . . 6 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> ((C +v D) -v (x +v y)) = ((C -v x) +v (D -v y)))
14	4, 13	eqtrd 1128	. . . . 5 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (R -v z) = ((C -v x) +v (D -v y)))
15	14	fveq2d 2836	. . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (norm` (R -v z)) = (norm` ((C -v x) +v (D -v y))))
16	15	opreq1d 3012	. . 3 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> ((norm` (R -v z))^2) = ((norm` ((C -v x) +v (D -v y)))^2))
17		normpytht 5092	. . . 4 |- (((C -v x) e. H~ /\ (D -v y) e. H~) -> (((C -v x) .i (D -v y)) = 0 -> ((norm` ((C -v x) +v (D -v y)))^2) = (((norm` (C -v x))^2) + ((norm` (D -v y))^2))))
18		hvsubclt 4998	. . . . . . . . 9 |- ((C e. H~ /\ x e. H~) -> (C -v x) e. H~)
19		hvsubclt 4998	. . . . . . . . 9 |- ((D e. H~ /\ y e. H~) -> (D -v y) e. H~)
20	18, 19	anim12i 268	. . . . . . . 8 |- (((C e. H~ /\ x e. H~) /\ (D e. H~ /\ y e. H~)) -> ((C -v x) e. H~ /\ (D -v y) e. H~))
21	20	an4s 390	. . . . . . 7 |- (((C e. H~ /\ D e. H~) /\ (x e. H~ /\ y e. H~)) -> ((C -v x) e. H~ /\ (D -v y) e. H~))
22	21	adantlr 310	. . . . . 6 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ (x e. H~ /\ y e. H~)) -> ((C -v x) e. H~ /\ (D -v y) e. H~))
23	22	adantrr 312	. . . . 5 |- ((((C e. H~ /\ D e. H~) /\ R e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> ((C -v x) e. H~ /\ (D -v y) e. H~))
24	9, 23	syl 12	. . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> ((C -v x) e. H~ /\ (D -v y) e. H~))
25	5	chshi 5132	. . . . . . . . 9 |- A e. SH
26		shocorth 5173	. . . . . . . . 9 |- (A e. SH -> (((C -v x) e. A /\ (D -v y) e. (_|_` A)) -> ((C -v x) .i (D -v y)) = 0))
27	25, 26	ax-mp 6	. . . . . . . 8 |- (((C -v x) e. A /\ (D -v y) e. (_|_` A)) -> ((C -v x) .i (D -v y)) = 0)
28		shsubclt 5125	. . . . . . . . 9 |- (A e. SH -> ((C e. A /\ x e. A) -> (C -v x) e. A))
29	25, 28	ax-mp 6	. . . . . . . 8 |- ((C e. A /\ x e. A) -> (C -v x) e. A)
30	5	chocl 5192	. . . . . . . . . . 11 |- (_|_` A) e. CH
31	30	chshi 5132	. . . . . . . . . 10 |- (_|_` A) e. SH
32		shsubclt 5125	. . . . . . . . . 10 |- ((_|_` A) e. SH -> ((D e. (_|_` A) /\ y e. (_|_` A)) -> (D -v y) e. (_|_` A)))
33	31, 32	ax-mp 6	. . . . . . . . 9 |- ((D e. (_|_` A) /\ y e. (_|_` A)) -> (D -v y) e. (_|_` A))
34	7	sseli 1504	. . . . . . . . 9 |- (D e. B -> D e. (_|_` A))
35	33, 34	sylan 343	. . . . . . . 8 |- ((D e. B /\ y e. (_|_` A)) -> (D -v y) e. (_|_` A))
36	27, 29, 35	syl2an 349	. . . . . . 7 |- (((C e. A /\ x e. A) /\ (D e. B /\ y e. (_|_` A))) -> ((C -v x) .i (D -v y)) = 0)
37	36	an4s 390	. . . . . 6 |- (((C e. A /\ D e. B) /\ (x e. A /\ y e. (_|_` A))) -> ((C -v x) .i (D -v y)) = 0)
38	37	adantlr 310	. . . . 5 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ (x e. A /\ y e. (_|_` A))) -> ((C -v x) .i (D -v y)) = 0)
39	38	adantrr 312	. . . 4 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> ((C -v x) .i (D -v y)) = 0)
40	17, 24, 39	sylc 62	. . 3 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> ((norm` ((C -v x) +v (D -v y)))^2) = (((norm` (C -v x))^2) + ((norm` (D -v y))^2)))
41	16, 40	eqtr2d 1129	. 2 |- ((((C e. A /\ D e. B) /\ R = (C +v D)) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (((norm` (C -v x))^2) + ((norm` (D -v y))^2)) = ((norm` (R -v z))^2))
42	1, 41	sylbi 174	1 |- (ph -> (((norm` (C -v x))^2) + ((norm` (D -v y))^2)) = ((norm` (R -v z))^2))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196   = wceq 1091   e. wcel 1092   (_ wss 1487  ` cfv 2422  (class class class)co 3001  0cc0 4028   + caddc 4031  2c2 4454  ^cexp 4675  H~chil 4958   +v cva 4959   -v cmv 4962   .i csp 4963  normcno 4964  SHcsh 4967  CHcch 4968  _|_cort 4969

This theorem is referenced by:  osumlem3 5532

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802