Step | Hyp | Ref
| Expression |
1 | | pjhth.2 |
. . . . . 6
β’ (π β π΄ β β) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β π΄ β β) |
3 | | pjhth.1 |
. . . . . . 7
β’ π» β
Cβ |
4 | 3 | cheli 30216 |
. . . . . 6
β’ (π₯ β π» β π₯ β β) |
5 | 4 | ad2antrl 727 |
. . . . 5
β’ ((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β π₯ β β) |
6 | | hvsubcl 30001 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β) β (π΄ ββ
π₯) β
β) |
7 | 2, 5, 6 | syl2anc 585 |
. . . 4
β’ ((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β (π΄ ββ π₯) β
β) |
8 | 2 | adantr 482 |
. . . . . 6
β’ (((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β§ π¦ β π») β π΄ β β) |
9 | | simplrl 776 |
. . . . . 6
β’ (((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β§ π¦ β π») β π₯ β π») |
10 | | simpr 486 |
. . . . . 6
β’ (((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β§ π¦ β π») β π¦ β π») |
11 | | simplrr 777 |
. . . . . 6
β’ (((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β§ π¦ β π») β βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§))) |
12 | | eqid 2737 |
. . . . . 6
β’ (((π΄ ββ
π₯)
Β·ih π¦) / ((π¦ Β·ih π¦) + 1)) = (((π΄ ββ π₯)
Β·ih π¦) / ((π¦ Β·ih π¦) + 1)) |
13 | 3, 8, 9, 10, 11, 12 | pjhthlem1 30375 |
. . . . 5
β’ (((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β§ π¦ β π») β ((π΄ ββ π₯)
Β·ih π¦) = 0) |
14 | 13 | ralrimiva 3144 |
. . . 4
β’ ((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β βπ¦ β π» ((π΄ ββ π₯)
Β·ih π¦) = 0) |
15 | 3 | chshii 30211 |
. . . . 5
β’ π» β
Sβ |
16 | | shocel 30266 |
. . . . 5
β’ (π» β
Sβ β ((π΄ ββ π₯) β (β₯βπ») β ((π΄ ββ π₯) β β β§
βπ¦ β π» ((π΄ ββ π₯)
Β·ih π¦) = 0))) |
17 | 15, 16 | ax-mp 5 |
. . . 4
β’ ((π΄ ββ
π₯) β
(β₯βπ») β
((π΄
ββ π₯) β β β§ βπ¦ β π» ((π΄ ββ π₯)
Β·ih π¦) = 0)) |
18 | 7, 14, 17 | sylanbrc 584 |
. . 3
β’ ((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β (π΄ ββ π₯) β (β₯βπ»)) |
19 | | hvpncan3 30026 |
. . . . 5
β’ ((π₯ β β β§ π΄ β β) β (π₯ +β (π΄ ββ
π₯)) = π΄) |
20 | 5, 2, 19 | syl2anc 585 |
. . . 4
β’ ((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β (π₯ +β (π΄ ββ π₯)) = π΄) |
21 | 20 | eqcomd 2743 |
. . 3
β’ ((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β π΄ = (π₯ +β (π΄ ββ π₯))) |
22 | | oveq2 7370 |
. . . 4
β’ (π¦ = (π΄ ββ π₯) β (π₯ +β π¦) = (π₯ +β (π΄ ββ π₯))) |
23 | 22 | rspceeqv 3600 |
. . 3
β’ (((π΄ ββ
π₯) β
(β₯βπ») β§
π΄ = (π₯ +β (π΄ ββ π₯))) β βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦)) |
24 | 18, 21, 23 | syl2anc 585 |
. 2
β’ ((π β§ (π₯ β π» β§ βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)))) β βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦)) |
25 | | df-hba 29953 |
. . . 4
β’ β
= (BaseSetββ¨β¨ +β ,
Β·β β©,
normββ©) |
26 | | eqid 2737 |
. . . . 5
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
27 | 26 | hhvs 30154 |
. . . 4
β’
ββ = ( βπ£ ββ¨β¨
+β , Β·β β©,
normββ©) |
28 | 26 | hhnm 30155 |
. . . 4
β’
normβ = (normCVββ¨β¨
+β , Β·β β©,
normββ©) |
29 | | eqid 2737 |
. . . . 5
β’
β¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© = β¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© |
30 | 29, 15 | hhssba 30255 |
. . . 4
β’ π» = (BaseSetββ¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β©) |
31 | 26 | hhph 30162 |
. . . . 5
β’
β¨β¨ +β , Β·β
β©, normββ© β
CPreHilOLD |
32 | 31 | a1i 11 |
. . . 4
β’ (π β β¨β¨
+β , Β·β β©,
normββ© β CPreHilOLD) |
33 | 26, 29 | hhsst 30250 |
. . . . . . 7
β’ (π» β
Sβ β β¨β¨( +β
βΎ (π» Γ π»)), (
Β·β βΎ (β Γ π»))β©, (normβ βΎ
π»)β© β
(SubSpββ¨β¨ +β ,
Β·β β©,
normββ©)) |
34 | 15, 33 | ax-mp 5 |
. . . . . 6
β’
β¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© β
(SubSpββ¨β¨ +β ,
Β·β β©,
normββ©) |
35 | 29, 3 | hhssbnOLD 30263 |
. . . . . 6
β’
β¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© β
CBan |
36 | | elin 3931 |
. . . . . 6
β’
(β¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© β
((SubSpββ¨β¨ +β ,
Β·β β©, normββ©) β©
CBan) β (β¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© β
(SubSpββ¨β¨ +β ,
Β·β β©, normββ©) β§
β¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© β
CBan)) |
37 | 34, 35, 36 | mpbir2an 710 |
. . . . 5
β’
β¨β¨( +β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© β
((SubSpββ¨β¨ +β ,
Β·β β©, normββ©) β©
CBan) |
38 | 37 | a1i 11 |
. . . 4
β’ (π β β¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© β
((SubSpββ¨β¨ +β ,
Β·β β©, normββ©) β©
CBan)) |
39 | 25, 27, 28, 30, 32, 38, 1 | minveco 29868 |
. . 3
β’ (π β β!π₯ β π» βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§))) |
40 | | reurex 3360 |
. . 3
β’
(β!π₯ β
π» βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§)) β βπ₯ β π» βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§))) |
41 | 39, 40 | syl 17 |
. 2
β’ (π β βπ₯ β π» βπ§ β π» (normββ(π΄ ββ
π₯)) β€
(normββ(π΄ ββ π§))) |
42 | 24, 41 | reximddv 3169 |
1
β’ (π β βπ₯ β π» βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦)) |