MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pjthlem1 Structured version   Visualization version   GIF version

Theorem pjthlem1 22891
Description: Lemma for pjth 22893. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 17-Oct-2015.)
Hypotheses
Ref Expression
pjthlem.v 𝑉 = (Base‘𝑊)
pjthlem.n 𝑁 = (norm‘𝑊)
pjthlem.p + = (+g𝑊)
pjthlem.m = (-g𝑊)
pjthlem.h , = (·𝑖𝑊)
pjthlem.l 𝐿 = (LSubSp‘𝑊)
pjthlem.1 (𝜑𝑊 ∈ ℂHil)
pjthlem.2 (𝜑𝑈𝐿)
pjthlem.4 (𝜑𝐴𝑉)
pjthlem.5 (𝜑𝐵𝑈)
pjthlem.7 (𝜑 → ∀𝑥𝑈 (𝑁𝐴) ≤ (𝑁‘(𝐴 𝑥)))
pjthlem.8 𝑇 = ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))
Assertion
Ref Expression
pjthlem1 (𝜑 → (𝐴 , 𝐵) = 0)
Distinct variable groups:   𝑥,   𝑥,𝐴   𝑥,𝐵   𝑥,𝑁   𝜑,𝑥   𝑥,𝑈   𝑥,𝑉   𝑥,𝑇   𝑥,𝑊
Allowed substitution hints:   + (𝑥)   , (𝑥)   𝐿(𝑥)

Proof of Theorem pjthlem1
StepHypRef Expression
1 pjthlem.1 . . . 4 (𝜑𝑊 ∈ ℂHil)
2 hlcph 22831 . . . 4 (𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil)
31, 2syl 17 . . 3 (𝜑𝑊 ∈ ℂPreHil)
4 pjthlem.4 . . 3 (𝜑𝐴𝑉)
5 pjthlem.2 . . . . 5 (𝜑𝑈𝐿)
6 pjthlem.v . . . . . 6 𝑉 = (Base‘𝑊)
7 pjthlem.l . . . . . 6 𝐿 = (LSubSp‘𝑊)
86, 7lssss 18662 . . . . 5 (𝑈𝐿𝑈𝑉)
95, 8syl 17 . . . 4 (𝜑𝑈𝑉)
10 pjthlem.5 . . . 4 (𝜑𝐵𝑈)
119, 10sseldd 3473 . . 3 (𝜑𝐵𝑉)
12 pjthlem.h . . . 4 , = (·𝑖𝑊)
136, 12cphipcl 22669 . . 3 ((𝑊 ∈ ℂPreHil ∧ 𝐴𝑉𝐵𝑉) → (𝐴 , 𝐵) ∈ ℂ)
143, 4, 11, 13syl3anc 1317 . 2 (𝜑 → (𝐴 , 𝐵) ∈ ℂ)
1514abscld 13882 . . . 4 (𝜑 → (abs‘(𝐴 , 𝐵)) ∈ ℝ)
1615recnd 9823 . . 3 (𝜑 → (abs‘(𝐴 , 𝐵)) ∈ ℂ)
1715resqcld 12765 . . . . . . 7 (𝜑 → ((abs‘(𝐴 , 𝐵))↑2) ∈ ℝ)
1817renegcld 10208 . . . . . 6 (𝜑 → -((abs‘(𝐴 , 𝐵))↑2) ∈ ℝ)
196, 12reipcl 22675 . . . . . . . 8 ((𝑊 ∈ ℂPreHil ∧ 𝐵𝑉) → (𝐵 , 𝐵) ∈ ℝ)
203, 11, 19syl2anc 690 . . . . . . 7 (𝜑 → (𝐵 , 𝐵) ∈ ℝ)
21 2re 10845 . . . . . . 7 2 ∈ ℝ
22 readdcl 9774 . . . . . . 7 (((𝐵 , 𝐵) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝐵 , 𝐵) + 2) ∈ ℝ)
2320, 21, 22sylancl 692 . . . . . 6 (𝜑 → ((𝐵 , 𝐵) + 2) ∈ ℝ)
24 0red 9796 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
25 peano2re 9960 . . . . . . . 8 ((𝐵 , 𝐵) ∈ ℝ → ((𝐵 , 𝐵) + 1) ∈ ℝ)
2620, 25syl 17 . . . . . . 7 (𝜑 → ((𝐵 , 𝐵) + 1) ∈ ℝ)
276, 12ipge0 22676 . . . . . . . . 9 ((𝑊 ∈ ℂPreHil ∧ 𝐵𝑉) → 0 ≤ (𝐵 , 𝐵))
283, 11, 27syl2anc 690 . . . . . . . 8 (𝜑 → 0 ≤ (𝐵 , 𝐵))
2920ltp1d 10704 . . . . . . . 8 (𝜑 → (𝐵 , 𝐵) < ((𝐵 , 𝐵) + 1))
3024, 20, 26, 28, 29lelttrd 9946 . . . . . . 7 (𝜑 → 0 < ((𝐵 , 𝐵) + 1))
3126ltp1d 10704 . . . . . . . 8 (𝜑 → ((𝐵 , 𝐵) + 1) < (((𝐵 , 𝐵) + 1) + 1))
3220recnd 9823 . . . . . . . . . 10 (𝜑 → (𝐵 , 𝐵) ∈ ℂ)
33 ax-1cn 9749 . . . . . . . . . . 11 1 ∈ ℂ
34 addass 9778 . . . . . . . . . . 11 (((𝐵 , 𝐵) ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐵 , 𝐵) + 1) + 1) = ((𝐵 , 𝐵) + (1 + 1)))
3533, 33, 34mp3an23 1407 . . . . . . . . . 10 ((𝐵 , 𝐵) ∈ ℂ → (((𝐵 , 𝐵) + 1) + 1) = ((𝐵 , 𝐵) + (1 + 1)))
3632, 35syl 17 . . . . . . . . 9 (𝜑 → (((𝐵 , 𝐵) + 1) + 1) = ((𝐵 , 𝐵) + (1 + 1)))
37 df-2 10834 . . . . . . . . . 10 2 = (1 + 1)
3837oveq2i 6437 . . . . . . . . 9 ((𝐵 , 𝐵) + 2) = ((𝐵 , 𝐵) + (1 + 1))
3936, 38syl6reqr 2567 . . . . . . . 8 (𝜑 → ((𝐵 , 𝐵) + 2) = (((𝐵 , 𝐵) + 1) + 1))
4031, 39breqtrrd 4509 . . . . . . 7 (𝜑 → ((𝐵 , 𝐵) + 1) < ((𝐵 , 𝐵) + 2))
4124, 26, 23, 30, 40lttrd 9949 . . . . . 6 (𝜑 → 0 < ((𝐵 , 𝐵) + 2))
42 cphlmod 22652 . . . . . . . . . . . . . 14 (𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod)
433, 42syl 17 . . . . . . . . . . . . 13 (𝜑𝑊 ∈ LMod)
44 pjthlem.8 . . . . . . . . . . . . . 14 𝑇 = ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))
45 hlphl 22832 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ ℂHil → 𝑊 ∈ PreHil)
461, 45syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑊 ∈ PreHil)
47 eqid 2514 . . . . . . . . . . . . . . . . 17 (Scalar‘𝑊) = (Scalar‘𝑊)
48 eqid 2514 . . . . . . . . . . . . . . . . 17 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
4947, 12, 6, 48ipcl 19703 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ PreHil ∧ 𝐴𝑉𝐵𝑉) → (𝐴 , 𝐵) ∈ (Base‘(Scalar‘𝑊)))
5046, 4, 11, 49syl3anc 1317 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 , 𝐵) ∈ (Base‘(Scalar‘𝑊)))
5147, 48hlress 22835 . . . . . . . . . . . . . . . . 17 (𝑊 ∈ ℂHil → ℝ ⊆ (Base‘(Scalar‘𝑊)))
521, 51syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ℝ ⊆ (Base‘(Scalar‘𝑊)))
5352, 26sseldd 3473 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 , 𝐵) + 1) ∈ (Base‘(Scalar‘𝑊)))
5420, 28ge0p1rpd 11644 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 , 𝐵) + 1) ∈ ℝ+)
5554rpne0d 11619 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 , 𝐵) + 1) ≠ 0)
5647, 48cphdivcl 22660 . . . . . . . . . . . . . . 15 ((𝑊 ∈ ℂPreHil ∧ ((𝐴 , 𝐵) ∈ (Base‘(Scalar‘𝑊)) ∧ ((𝐵 , 𝐵) + 1) ∈ (Base‘(Scalar‘𝑊)) ∧ ((𝐵 , 𝐵) + 1) ≠ 0)) → ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1)) ∈ (Base‘(Scalar‘𝑊)))
573, 50, 53, 55, 56syl13anc 1319 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1)) ∈ (Base‘(Scalar‘𝑊)))
5844, 57syl5eqel 2596 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ (Base‘(Scalar‘𝑊)))
59 eqid 2514 . . . . . . . . . . . . . 14 ( ·𝑠𝑊) = ( ·𝑠𝑊)
6047, 59, 48, 7lssvscl 18680 . . . . . . . . . . . . 13 (((𝑊 ∈ LMod ∧ 𝑈𝐿) ∧ (𝑇 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝐵𝑈)) → (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑈)
6143, 5, 58, 10, 60syl22anc 1318 . . . . . . . . . . . 12 (𝜑 → (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑈)
62 pjthlem.7 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝑈 (𝑁𝐴) ≤ (𝑁‘(𝐴 𝑥)))
63 oveq2 6434 . . . . . . . . . . . . . . 15 (𝑥 = (𝑇( ·𝑠𝑊)𝐵) → (𝐴 𝑥) = (𝐴 (𝑇( ·𝑠𝑊)𝐵)))
6463fveq2d 5991 . . . . . . . . . . . . . 14 (𝑥 = (𝑇( ·𝑠𝑊)𝐵) → (𝑁‘(𝐴 𝑥)) = (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵))))
6564breq2d 4493 . . . . . . . . . . . . 13 (𝑥 = (𝑇( ·𝑠𝑊)𝐵) → ((𝑁𝐴) ≤ (𝑁‘(𝐴 𝑥)) ↔ (𝑁𝐴) ≤ (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))))
6665rspcv 3182 . . . . . . . . . . . 12 ((𝑇( ·𝑠𝑊)𝐵) ∈ 𝑈 → (∀𝑥𝑈 (𝑁𝐴) ≤ (𝑁‘(𝐴 𝑥)) → (𝑁𝐴) ≤ (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))))
6761, 62, 66sylc 62 . . . . . . . . . . 11 (𝜑 → (𝑁𝐴) ≤ (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵))))
68 cphngp 22651 . . . . . . . . . . . . . 14 (𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp)
693, 68syl 17 . . . . . . . . . . . . 13 (𝜑𝑊 ∈ NrmGrp)
70 pjthlem.n . . . . . . . . . . . . . 14 𝑁 = (norm‘𝑊)
716, 70nmcl 22131 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmGrp ∧ 𝐴𝑉) → (𝑁𝐴) ∈ ℝ)
7269, 4, 71syl2anc 690 . . . . . . . . . . . 12 (𝜑 → (𝑁𝐴) ∈ ℝ)
736, 47, 59, 48lmodvscl 18610 . . . . . . . . . . . . . . 15 ((𝑊 ∈ LMod ∧ 𝑇 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝐵𝑉) → (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉)
7443, 58, 11, 73syl3anc 1317 . . . . . . . . . . . . . 14 (𝜑 → (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉)
75 pjthlem.m . . . . . . . . . . . . . . 15 = (-g𝑊)
766, 75lmodvsubcl 18635 . . . . . . . . . . . . . 14 ((𝑊 ∈ LMod ∧ 𝐴𝑉 ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉) → (𝐴 (𝑇( ·𝑠𝑊)𝐵)) ∈ 𝑉)
7743, 4, 74, 76syl3anc 1317 . . . . . . . . . . . . 13 (𝜑 → (𝐴 (𝑇( ·𝑠𝑊)𝐵)) ∈ 𝑉)
786, 70nmcl 22131 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmGrp ∧ (𝐴 (𝑇( ·𝑠𝑊)𝐵)) ∈ 𝑉) → (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵))) ∈ ℝ)
7969, 77, 78syl2anc 690 . . . . . . . . . . . 12 (𝜑 → (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵))) ∈ ℝ)
806, 70nmge0 22132 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmGrp ∧ 𝐴𝑉) → 0 ≤ (𝑁𝐴))
8169, 4, 80syl2anc 690 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑁𝐴))
826, 70nmge0 22132 . . . . . . . . . . . . 13 ((𝑊 ∈ NrmGrp ∧ (𝐴 (𝑇( ·𝑠𝑊)𝐵)) ∈ 𝑉) → 0 ≤ (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵))))
8369, 77, 82syl2anc 690 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵))))
8472, 79, 81, 83le2sqd 12774 . . . . . . . . . . 11 (𝜑 → ((𝑁𝐴) ≤ (𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵))) ↔ ((𝑁𝐴)↑2) ≤ ((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2)))
8567, 84mpbid 220 . . . . . . . . . 10 (𝜑 → ((𝑁𝐴)↑2) ≤ ((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2))
8679resqcld 12765 . . . . . . . . . . 11 (𝜑 → ((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) ∈ ℝ)
8772resqcld 12765 . . . . . . . . . . 11 (𝜑 → ((𝑁𝐴)↑2) ∈ ℝ)
8886, 87subge0d 10366 . . . . . . . . . 10 (𝜑 → (0 ≤ (((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) − ((𝑁𝐴)↑2)) ↔ ((𝑁𝐴)↑2) ≤ ((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2)))
8985, 88mpbird 245 . . . . . . . . 9 (𝜑 → 0 ≤ (((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) − ((𝑁𝐴)↑2)))
90 2z 11150 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
91 rpexpcl 12609 . . . . . . . . . . . . . . . 16 ((((𝐵 , 𝐵) + 1) ∈ ℝ+ ∧ 2 ∈ ℤ) → (((𝐵 , 𝐵) + 1)↑2) ∈ ℝ+)
9254, 90, 91sylancl 692 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵 , 𝐵) + 1)↑2) ∈ ℝ+)
9317, 92rerpdivcld 11645 . . . . . . . . . . . . . 14 (𝜑 → (((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) ∈ ℝ)
9493, 23remulcld 9825 . . . . . . . . . . . . 13 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)) ∈ ℝ)
9594recnd 9823 . . . . . . . . . . . 12 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)) ∈ ℂ)
9695negcld 10130 . . . . . . . . . . 11 (𝜑 → -((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)) ∈ ℂ)
976, 12cphipcl 22669 . . . . . . . . . . . 12 ((𝑊 ∈ ℂPreHil ∧ 𝐴𝑉𝐴𝑉) → (𝐴 , 𝐴) ∈ ℂ)
983, 4, 4, 97syl3anc 1317 . . . . . . . . . . 11 (𝜑 → (𝐴 , 𝐴) ∈ ℂ)
9996, 98pncand 10144 . . . . . . . . . 10 (𝜑 → ((-((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)) + (𝐴 , 𝐴)) − (𝐴 , 𝐴)) = -((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)))
1006, 12, 70nmsq 22672 . . . . . . . . . . . . . 14 ((𝑊 ∈ ℂPreHil ∧ (𝐴 (𝑇( ·𝑠𝑊)𝐵)) ∈ 𝑉) → ((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) = ((𝐴 (𝑇( ·𝑠𝑊)𝐵)) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))))
1013, 77, 100syl2anc 690 . . . . . . . . . . . . 13 (𝜑 → ((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) = ((𝐴 (𝑇( ·𝑠𝑊)𝐵)) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))))
10212, 6, 75cphsubdir 22685 . . . . . . . . . . . . . 14 ((𝑊 ∈ ℂPreHil ∧ (𝐴𝑉 ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉 ∧ (𝐴 (𝑇( ·𝑠𝑊)𝐵)) ∈ 𝑉)) → ((𝐴 (𝑇( ·𝑠𝑊)𝐵)) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) = ((𝐴 , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) − ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵)))))
1033, 4, 74, 77, 102syl13anc 1319 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 (𝑇( ·𝑠𝑊)𝐵)) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) = ((𝐴 , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) − ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵)))))
10412, 6, 75cphsubdi 22686 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ ℂPreHil ∧ (𝐴𝑉𝐴𝑉 ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉)) → (𝐴 , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) = ((𝐴 , 𝐴) − (𝐴 , (𝑇( ·𝑠𝑊)𝐵))))
1053, 4, 4, 74, 104syl13anc 1319 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) = ((𝐴 , 𝐴) − (𝐴 , (𝑇( ·𝑠𝑊)𝐵))))
106105oveq1d 6441 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) − ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵)))) = (((𝐴 , 𝐴) − (𝐴 , (𝑇( ·𝑠𝑊)𝐵))) − ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵)))))
1076, 12cphipcl 22669 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ ℂPreHil ∧ 𝐴𝑉 ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉) → (𝐴 , (𝑇( ·𝑠𝑊)𝐵)) ∈ ℂ)
1083, 4, 74, 107syl3anc 1317 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 , (𝑇( ·𝑠𝑊)𝐵)) ∈ ℂ)
10912, 6, 75cphsubdi 22686 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ ℂPreHil ∧ ((𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉𝐴𝑉 ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉)) → ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) = (((𝑇( ·𝑠𝑊)𝐵) , 𝐴) − ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵))))
1103, 74, 4, 74, 109syl13anc 1319 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) = (((𝑇( ·𝑠𝑊)𝐵) , 𝐴) − ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵))))
1116, 12cphipcl 22669 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ ℂPreHil ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉𝐴𝑉) → ((𝑇( ·𝑠𝑊)𝐵) , 𝐴) ∈ ℂ)
1123, 74, 4, 111syl3anc 1317 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑇( ·𝑠𝑊)𝐵) , 𝐴) ∈ ℂ)
1136, 12cphipcl 22669 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ ℂPreHil ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉 ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉) → ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵)) ∈ ℂ)
1143, 74, 74, 113syl3anc 1317 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵)) ∈ ℂ)
115112, 114subcld 10143 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝑇( ·𝑠𝑊)𝐵) , 𝐴) − ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵))) ∈ ℂ)
116110, 115eqeltrd 2592 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) ∈ ℂ)
11798, 108, 116subsub4d 10174 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 , 𝐴) − (𝐴 , (𝑇( ·𝑠𝑊)𝐵))) − ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵)))) = ((𝐴 , 𝐴) − ((𝐴 , (𝑇( ·𝑠𝑊)𝐵)) + ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))))))
11893recnd 9823 . . . . . . . . . . . . . . . . 17 (𝜑 → (((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) ∈ ℂ)
11926recnd 9823 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 , 𝐵) + 1) ∈ ℂ)
120 1cnd 9811 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℂ)
121118, 119, 120adddid 9819 . . . . . . . . . . . . . . . 16 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (((𝐵 , 𝐵) + 1) + 1)) = (((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)) + ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · 1)))
12239oveq2d 6442 . . . . . . . . . . . . . . . 16 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (((𝐵 , 𝐵) + 1) + 1)))
12312, 6, 47, 48, 59cphassr 22689 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ ℂPreHil ∧ (𝑇 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝐴𝑉𝐵𝑉)) → (𝐴 , (𝑇( ·𝑠𝑊)𝐵)) = ((∗‘𝑇) · (𝐴 , 𝐵)))
1243, 58, 4, 11, 123syl13anc 1319 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 , (𝑇( ·𝑠𝑊)𝐵)) = ((∗‘𝑇) · (𝐴 , 𝐵)))
12514, 119, 55divcld 10550 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1)) ∈ ℂ)
12644, 125syl5eqel 2596 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑇 ∈ ℂ)
127126cjcld 13643 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∗‘𝑇) ∈ ℂ)
128127, 14mulcomd 9816 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((∗‘𝑇) · (𝐴 , 𝐵)) = ((𝐴 , 𝐵) · (∗‘𝑇)))
12914cjcld 13643 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (∗‘(𝐴 , 𝐵)) ∈ ℂ)
13014, 129, 119, 55divassd 10585 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴 , 𝐵) · (∗‘(𝐴 , 𝐵))) / ((𝐵 , 𝐵) + 1)) = ((𝐴 , 𝐵) · ((∗‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1))))
13114absvalsqd 13888 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((abs‘(𝐴 , 𝐵))↑2) = ((𝐴 , 𝐵) · (∗‘(𝐴 , 𝐵))))
132131oveq1d 6441 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((abs‘(𝐴 , 𝐵))↑2) / ((𝐵 , 𝐵) + 1)) = (((𝐴 , 𝐵) · (∗‘(𝐴 , 𝐵))) / ((𝐵 , 𝐵) + 1)))
13344fveq2i 5990 . . . . . . . . . . . . . . . . . . . . . 22 (∗‘𝑇) = (∗‘((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1)))
13414, 119, 55cjdivd 13670 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (∗‘((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))) = ((∗‘(𝐴 , 𝐵)) / (∗‘((𝐵 , 𝐵) + 1))))
13526cjred 13673 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (∗‘((𝐵 , 𝐵) + 1)) = ((𝐵 , 𝐵) + 1))
136135oveq2d 6442 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((∗‘(𝐴 , 𝐵)) / (∗‘((𝐵 , 𝐵) + 1))) = ((∗‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1)))
137134, 136eqtrd 2548 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (∗‘((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))) = ((∗‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1)))
138133, 137syl5eq 2560 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (∗‘𝑇) = ((∗‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1)))
139138oveq2d 6442 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐴 , 𝐵) · (∗‘𝑇)) = ((𝐴 , 𝐵) · ((∗‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1))))
140130, 132, 1393eqtr4rd 2559 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 , 𝐵) · (∗‘𝑇)) = (((abs‘(𝐴 , 𝐵))↑2) / ((𝐵 , 𝐵) + 1)))
141124, 128, 1403eqtrd 2552 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 , (𝑇( ·𝑠𝑊)𝐵)) = (((abs‘(𝐴 , 𝐵))↑2) / ((𝐵 , 𝐵) + 1)))
14217recnd 9823 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((abs‘(𝐴 , 𝐵))↑2) ∈ ℂ)
143142, 119mulcomd 9816 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((abs‘(𝐴 , 𝐵))↑2) · ((𝐵 , 𝐵) + 1)) = (((𝐵 , 𝐵) + 1) · ((abs‘(𝐴 , 𝐵))↑2)))
144119sqvald 12735 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐵 , 𝐵) + 1)↑2) = (((𝐵 , 𝐵) + 1) · ((𝐵 , 𝐵) + 1)))
145143, 144oveq12d 6444 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) · ((𝐵 , 𝐵) + 1)) / (((𝐵 , 𝐵) + 1)↑2)) = ((((𝐵 , 𝐵) + 1) · ((abs‘(𝐴 , 𝐵))↑2)) / (((𝐵 , 𝐵) + 1) · ((𝐵 , 𝐵) + 1))))
146142, 119, 119, 55, 55divcan5d 10576 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((𝐵 , 𝐵) + 1) · ((abs‘(𝐴 , 𝐵))↑2)) / (((𝐵 , 𝐵) + 1) · ((𝐵 , 𝐵) + 1))) = (((abs‘(𝐴 , 𝐵))↑2) / ((𝐵 , 𝐵) + 1)))
147145, 146eqtr2d 2549 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((abs‘(𝐴 , 𝐵))↑2) / ((𝐵 , 𝐵) + 1)) = ((((abs‘(𝐴 , 𝐵))↑2) · ((𝐵 , 𝐵) + 1)) / (((𝐵 , 𝐵) + 1)↑2)))
14892rpcnd 11616 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐵 , 𝐵) + 1)↑2) ∈ ℂ)
14992rpne0d 11619 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐵 , 𝐵) + 1)↑2) ≠ 0)
150142, 119, 148, 149div23d 10587 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) · ((𝐵 , 𝐵) + 1)) / (((𝐵 , 𝐵) + 1)↑2)) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)))
151141, 147, 1503eqtrd 2552 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 , (𝑇( ·𝑠𝑊)𝐵)) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)))
15293, 26remulcld 9825 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)) ∈ ℝ)
153151, 152eqeltrd 2592 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐴 , (𝑇( ·𝑠𝑊)𝐵)) ∈ ℝ)
154153cjred 13673 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∗‘(𝐴 , (𝑇( ·𝑠𝑊)𝐵))) = (𝐴 , (𝑇( ·𝑠𝑊)𝐵)))
15512, 6cphipcj 22677 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ ℂPreHil ∧ 𝐴𝑉 ∧ (𝑇( ·𝑠𝑊)𝐵) ∈ 𝑉) → (∗‘(𝐴 , (𝑇( ·𝑠𝑊)𝐵))) = ((𝑇( ·𝑠𝑊)𝐵) , 𝐴))
1563, 4, 74, 155syl3anc 1317 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (∗‘(𝐴 , (𝑇( ·𝑠𝑊)𝐵))) = ((𝑇( ·𝑠𝑊)𝐵) , 𝐴))
157154, 156, 1513eqtr3d 2556 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑇( ·𝑠𝑊)𝐵) , 𝐴) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)))
15812, 6, 47, 48, 59cph2ass 22690 . . . . . . . . . . . . . . . . . . . . 21 ((𝑊 ∈ ℂPreHil ∧ (𝑇 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑇 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝐵𝑉𝐵𝑉)) → ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵)) = ((𝑇 · (∗‘𝑇)) · (𝐵 , 𝐵)))
1593, 58, 58, 11, 11, 158syl122anc 1326 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵)) = ((𝑇 · (∗‘𝑇)) · (𝐵 , 𝐵)))
16044fveq2i 5990 . . . . . . . . . . . . . . . . . . . . . . . 24 (abs‘𝑇) = (abs‘((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1)))
16114, 119, 55absdivd 13901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (abs‘((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))) = ((abs‘(𝐴 , 𝐵)) / (abs‘((𝐵 , 𝐵) + 1))))
16254rpge0d 11618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 0 ≤ ((𝐵 , 𝐵) + 1))
16326, 162absidd 13868 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (abs‘((𝐵 , 𝐵) + 1)) = ((𝐵 , 𝐵) + 1))
164163oveq2d 6442 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((abs‘(𝐴 , 𝐵)) / (abs‘((𝐵 , 𝐵) + 1))) = ((abs‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1)))
165161, 164eqtrd 2548 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (abs‘((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))) = ((abs‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1)))
166160, 165syl5eq 2560 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (abs‘𝑇) = ((abs‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1)))
167166oveq1d 6441 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((abs‘𝑇)↑2) = (((abs‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1))↑2))
168126absvalsqd 13888 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((abs‘𝑇)↑2) = (𝑇 · (∗‘𝑇)))
16916, 119, 55sqdivd 12751 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((abs‘(𝐴 , 𝐵)) / ((𝐵 , 𝐵) + 1))↑2) = (((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)))
170167, 168, 1693eqtr3d 2556 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑇 · (∗‘𝑇)) = (((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)))
171170oveq1d 6441 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑇 · (∗‘𝑇)) · (𝐵 , 𝐵)) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (𝐵 , 𝐵)))
172159, 171eqtrd 2548 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵)) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (𝐵 , 𝐵)))
173157, 172oveq12d 6444 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑇( ·𝑠𝑊)𝐵) , 𝐴) − ((𝑇( ·𝑠𝑊)𝐵) , (𝑇( ·𝑠𝑊)𝐵))) = (((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)) − ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (𝐵 , 𝐵))))
174 pncan2 10039 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵 , 𝐵) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐵 , 𝐵) + 1) − (𝐵 , 𝐵)) = 1)
17532, 33, 174sylancl 692 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐵 , 𝐵) + 1) − (𝐵 , 𝐵)) = 1)
176175oveq2d 6442 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (((𝐵 , 𝐵) + 1) − (𝐵 , 𝐵))) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · 1))
177118, 119, 32subdid 10236 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (((𝐵 , 𝐵) + 1) − (𝐵 , 𝐵))) = (((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)) − ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (𝐵 , 𝐵))))
178176, 177eqtr3d 2550 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · 1) = (((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)) − ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · (𝐵 , 𝐵))))
179173, 110, 1783eqtr4d 2558 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · 1))
180151, 179oveq12d 6444 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 , (𝑇( ·𝑠𝑊)𝐵)) + ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵)))) = (((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 1)) + ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · 1)))
181121, 122, 1803eqtr4rd 2559 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 , (𝑇( ·𝑠𝑊)𝐵)) + ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵)))) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)))
182181oveq2d 6442 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 , 𝐴) − ((𝐴 , (𝑇( ·𝑠𝑊)𝐵)) + ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵))))) = ((𝐴 , 𝐴) − ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2))))
183106, 117, 1823eqtrd 2552 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 , (𝐴 (𝑇( ·𝑠𝑊)𝐵))) − ((𝑇( ·𝑠𝑊)𝐵) , (𝐴 (𝑇( ·𝑠𝑊)𝐵)))) = ((𝐴 , 𝐴) − ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2))))
184101, 103, 1833eqtrd 2552 . . . . . . . . . . . 12 (𝜑 → ((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) = ((𝐴 , 𝐴) − ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2))))
18598, 95negsubd 10149 . . . . . . . . . . . 12 (𝜑 → ((𝐴 , 𝐴) + -((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2))) = ((𝐴 , 𝐴) − ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2))))
18698, 96addcomd 9989 . . . . . . . . . . . 12 (𝜑 → ((𝐴 , 𝐴) + -((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2))) = (-((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)) + (𝐴 , 𝐴)))
187184, 185, 1863eqtr2d 2554 . . . . . . . . . . 11 (𝜑 → ((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) = (-((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)) + (𝐴 , 𝐴)))
1886, 12, 70nmsq 22672 . . . . . . . . . . . 12 ((𝑊 ∈ ℂPreHil ∧ 𝐴𝑉) → ((𝑁𝐴)↑2) = (𝐴 , 𝐴))
1893, 4, 188syl2anc 690 . . . . . . . . . . 11 (𝜑 → ((𝑁𝐴)↑2) = (𝐴 , 𝐴))
190187, 189oveq12d 6444 . . . . . . . . . 10 (𝜑 → (((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) − ((𝑁𝐴)↑2)) = ((-((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)) + (𝐴 , 𝐴)) − (𝐴 , 𝐴)))
19123renegcld 10208 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 , 𝐵) + 2) ∈ ℝ)
192191recnd 9823 . . . . . . . . . . . 12 (𝜑 → -((𝐵 , 𝐵) + 2) ∈ ℂ)
193142, 192, 148, 149div23d 10587 . . . . . . . . . . 11 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)) / (((𝐵 , 𝐵) + 1)↑2)) = ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · -((𝐵 , 𝐵) + 2)))
19423recnd 9823 . . . . . . . . . . . 12 (𝜑 → ((𝐵 , 𝐵) + 2) ∈ ℂ)
195118, 194mulneg2d 10234 . . . . . . . . . . 11 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · -((𝐵 , 𝐵) + 2)) = -((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)))
196193, 195eqtrd 2548 . . . . . . . . . 10 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)) / (((𝐵 , 𝐵) + 1)↑2)) = -((((abs‘(𝐴 , 𝐵))↑2) / (((𝐵 , 𝐵) + 1)↑2)) · ((𝐵 , 𝐵) + 2)))
19799, 190, 1963eqtr4rd 2559 . . . . . . . . 9 (𝜑 → ((((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)) / (((𝐵 , 𝐵) + 1)↑2)) = (((𝑁‘(𝐴 (𝑇( ·𝑠𝑊)𝐵)))↑2) − ((𝑁𝐴)↑2)))
19889, 197breqtrrd 4509 . . . . . . . 8 (𝜑 → 0 ≤ ((((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)) / (((𝐵 , 𝐵) + 1)↑2)))
19917, 191remulcld 9825 . . . . . . . . 9 (𝜑 → (((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)) ∈ ℝ)
200199, 92ge0divd 11652 . . . . . . . 8 (𝜑 → (0 ≤ (((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)) ↔ 0 ≤ ((((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)) / (((𝐵 , 𝐵) + 1)↑2))))
201198, 200mpbird 245 . . . . . . 7 (𝜑 → 0 ≤ (((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)))
202 mulneg12 10219 . . . . . . . 8 ((((abs‘(𝐴 , 𝐵))↑2) ∈ ℂ ∧ ((𝐵 , 𝐵) + 2) ∈ ℂ) → (-((abs‘(𝐴 , 𝐵))↑2) · ((𝐵 , 𝐵) + 2)) = (((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)))
203142, 194, 202syl2anc 690 . . . . . . 7 (𝜑 → (-((abs‘(𝐴 , 𝐵))↑2) · ((𝐵 , 𝐵) + 2)) = (((abs‘(𝐴 , 𝐵))↑2) · -((𝐵 , 𝐵) + 2)))
204201, 203breqtrrd 4509 . . . . . 6 (𝜑 → 0 ≤ (-((abs‘(𝐴 , 𝐵))↑2) · ((𝐵 , 𝐵) + 2)))
205 prodge02 10620 . . . . . 6 (((-((abs‘(𝐴 , 𝐵))↑2) ∈ ℝ ∧ ((𝐵 , 𝐵) + 2) ∈ ℝ) ∧ (0 < ((𝐵 , 𝐵) + 2) ∧ 0 ≤ (-((abs‘(𝐴 , 𝐵))↑2) · ((𝐵 , 𝐵) + 2)))) → 0 ≤ -((abs‘(𝐴 , 𝐵))↑2))
20618, 23, 41, 204, 205syl22anc 1318 . . . . 5 (𝜑 → 0 ≤ -((abs‘(𝐴 , 𝐵))↑2))
20717le0neg1d 10348 . . . . 5 (𝜑 → (((abs‘(𝐴 , 𝐵))↑2) ≤ 0 ↔ 0 ≤ -((abs‘(𝐴 , 𝐵))↑2)))
208206, 207mpbird 245 . . . 4 (𝜑 → ((abs‘(𝐴 , 𝐵))↑2) ≤ 0)
20915sqge0d 12766 . . . 4 (𝜑 → 0 ≤ ((abs‘(𝐴 , 𝐵))↑2))
210 0re 9795 . . . . 5 0 ∈ ℝ
211 letri3 9873 . . . . 5 ((((abs‘(𝐴 , 𝐵))↑2) ∈ ℝ ∧ 0 ∈ ℝ) → (((abs‘(𝐴 , 𝐵))↑2) = 0 ↔ (((abs‘(𝐴 , 𝐵))↑2) ≤ 0 ∧ 0 ≤ ((abs‘(𝐴 , 𝐵))↑2))))
21217, 210, 211sylancl 692 . . . 4 (𝜑 → (((abs‘(𝐴 , 𝐵))↑2) = 0 ↔ (((abs‘(𝐴 , 𝐵))↑2) ≤ 0 ∧ 0 ≤ ((abs‘(𝐴 , 𝐵))↑2))))
213208, 209, 212mpbir2and 958 . . 3 (𝜑 → ((abs‘(𝐴 , 𝐵))↑2) = 0)
21416, 213sqeq0d 12737 . 2 (𝜑 → (abs‘(𝐴 , 𝐵)) = 0)
21514, 214abs00d 13892 1 (𝜑 → (𝐴 , 𝐵) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  wne 2684  wral 2800  wss 3444   class class class wbr 4481  cfv 5689  (class class class)co 6426  cc 9689  cr 9690  0cc0 9691  1c1 9692   + caddc 9694   · cmul 9696   < clt 9829  cle 9830  cmin 10017  -cneg 10018   / cdiv 10433  2c2 10825  cz 11118  +crp 11574  cexp 12590  ccj 13543  abscabs 13681  Basecbs 15579  +gcplusg 15652  Scalarcsca 15655   ·𝑠 cvsca 15656  ·𝑖cip 15657  -gcsg 17139  LModclmod 18593  LSubSpclss 18657  PreHilcphl 19694  normcnm 22093  NrmGrpcngp 22094  ℂPreHilccph 22644  ℂHilchl 22802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-inf2 8297  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768  ax-pre-sup 9769  ax-addf 9770  ax-mulf 9771
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-iin 4356  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-of 6671  df-om 6834  df-1st 6934  df-2nd 6935  df-supp 7058  df-tpos 7114  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-2o 7324  df-oadd 7327  df-er 7505  df-map 7622  df-ixp 7671  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-fsupp 8035  df-fi 8076  df-sup 8107  df-inf 8108  df-oi 8174  df-card 8524  df-cda 8749  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-div 10434  df-nn 10776  df-2 10834  df-3 10835  df-4 10836  df-5 10837  df-6 10838  df-7 10839  df-8 10840  df-9 10841  df-n0 11048  df-z 11119  df-dec 11234  df-uz 11428  df-q 11531  df-rp 11575  df-xneg 11688  df-xadd 11689  df-xmul 11690  df-ioo 11919  df-ico 11921  df-icc 11922  df-fz 12066  df-fzo 12203  df-seq 12532  df-exp 12591  df-hash 12848  df-cj 13546  df-re 13547  df-im 13548  df-sqrt 13682  df-abs 13683  df-struct 15581  df-ndx 15582  df-slot 15583  df-base 15584  df-sets 15585  df-ress 15586  df-plusg 15665  df-mulr 15666  df-starv 15667  df-sca 15668  df-vsca 15669  df-ip 15670  df-tset 15671  df-ple 15672  df-ds 15675  df-unif 15676  df-hom 15677  df-cco 15678  df-rest 15790  df-topn 15791  df-0g 15809  df-gsum 15810  df-topgen 15811  df-pt 15812  df-prds 15815  df-xrs 15869  df-qtop 15875  df-imas 15876  df-xps 15879  df-mre 15961  df-mrc 15962  df-acs 15964  df-mgm 16957  df-sgrp 16999  df-mnd 17010  df-mhm 17050  df-submnd 17051  df-grp 17140  df-minusg 17141  df-sbg 17142  df-mulg 17256  df-subg 17306  df-ghm 17373  df-cntz 17465  df-cmn 17926  df-mgp 18220  df-ur 18232  df-ring 18279  df-cring 18280  df-oppr 18353  df-dvdsr 18371  df-unit 18372  df-invr 18402  df-dvr 18413  df-rnghom 18445  df-drng 18479  df-subrg 18508  df-staf 18575  df-srng 18576  df-lmod 18595  df-lss 18658  df-lmhm 18747  df-lvec 18828  df-sra 18897  df-rgmod 18898  df-psmet 19463  df-xmet 19464  df-met 19465  df-bl 19466  df-mopn 19467  df-fbas 19468  df-fg 19469  df-cnfld 19472  df-phl 19696  df-top 20424  df-bases 20425  df-topon 20426  df-topsp 20427  df-cld 20536  df-ntr 20537  df-cls 20538  df-nei 20615  df-cn 20744  df-cnp 20745  df-haus 20832  df-cmp 20903  df-tx 21078  df-hmeo 21271  df-fil 21363  df-flim 21456  df-fcls 21458  df-xms 21837  df-ms 21838  df-tms 21839  df-nm 22099  df-ngp 22100  df-nlm 22103  df-cncf 22412  df-clm 22594  df-cph 22646  df-cfil 22725  df-cmet 22727  df-cms 22803  df-bn 22804  df-hl 22805
This theorem is referenced by:  pjthlem2  22892
  Copyright terms: Public domain W3C validator