Step | Hyp | Ref
| Expression |
1 | | stoweidlem23.3 |
. . 3
β’ π» = (π‘ β π β¦ ((πΊβπ‘) β (πΊβπ))) |
2 | | stoweidlem23.1 |
. . . . 5
β’
β²π‘π |
3 | | stoweidlem23.9 |
. . . . . . . . 9
β’ (π β πΊ β π΄) |
4 | 3 | ancli 550 |
. . . . . . . . 9
β’ (π β (π β§ πΊ β π΄)) |
5 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = πΊ β (π β π΄ β πΊ β π΄)) |
6 | 5 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π = πΊ β ((π β§ π β π΄) β (π β§ πΊ β π΄))) |
7 | | feq1 6653 |
. . . . . . . . . . 11
β’ (π = πΊ β (π:πβΆβ β πΊ:πβΆβ)) |
8 | 6, 7 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = πΊ β (((π β§ π β π΄) β π:πβΆβ) β ((π β§ πΊ β π΄) β πΊ:πβΆβ))) |
9 | | stoweidlem23.4 |
. . . . . . . . . 10
β’ ((π β§ π β π΄) β π:πβΆβ) |
10 | 8, 9 | vtoclg 3527 |
. . . . . . . . 9
β’ (πΊ β π΄ β ((π β§ πΊ β π΄) β πΊ:πβΆβ)) |
11 | 3, 4, 10 | sylc 65 |
. . . . . . . 8
β’ (π β πΊ:πβΆβ) |
12 | 11 | ffvelcdmda 7039 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πΊβπ‘) β β) |
13 | 12 | recnd 11191 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΊβπ‘) β β) |
14 | | stoweidlem23.8 |
. . . . . . . . 9
β’ (π β π β π) |
15 | 11, 14 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (π β (πΊβπ) β β) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π‘ β π) β (πΊβπ) β β) |
17 | 16 | recnd 11191 |
. . . . . 6
β’ ((π β§ π‘ β π) β (πΊβπ) β β) |
18 | 13, 17 | negsubd 11526 |
. . . . 5
β’ ((π β§ π‘ β π) β ((πΊβπ‘) + -(πΊβπ)) = ((πΊβπ‘) β (πΊβπ))) |
19 | 2, 18 | mpteq2da 5207 |
. . . 4
β’ (π β (π‘ β π β¦ ((πΊβπ‘) + -(πΊβπ))) = (π‘ β π β¦ ((πΊβπ‘) β (πΊβπ)))) |
20 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β π‘ β π) |
21 | 15 | renegcld 11590 |
. . . . . . . . 9
β’ (π β -(πΊβπ) β β) |
22 | 21 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β -(πΊβπ) β β) |
23 | | eqid 2733 |
. . . . . . . . 9
β’ (π‘ β π β¦ -(πΊβπ)) = (π‘ β π β¦ -(πΊβπ)) |
24 | 23 | fvmpt2 6963 |
. . . . . . . 8
β’ ((π‘ β π β§ -(πΊβπ) β β) β ((π‘ β π β¦ -(πΊβπ))βπ‘) = -(πΊβπ)) |
25 | 20, 22, 24 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((π‘ β π β¦ -(πΊβπ))βπ‘) = -(πΊβπ)) |
26 | 25 | oveq2d 7377 |
. . . . . 6
β’ ((π β§ π‘ β π) β ((πΊβπ‘) + ((π‘ β π β¦ -(πΊβπ))βπ‘)) = ((πΊβπ‘) + -(πΊβπ))) |
27 | 2, 26 | mpteq2da 5207 |
. . . . 5
β’ (π β (π‘ β π β¦ ((πΊβπ‘) + ((π‘ β π β¦ -(πΊβπ))βπ‘))) = (π‘ β π β¦ ((πΊβπ‘) + -(πΊβπ)))) |
28 | 21 | ancli 550 |
. . . . . . 7
β’ (π β (π β§ -(πΊβπ) β β)) |
29 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π₯ = -(πΊβπ) β (π₯ β β β -(πΊβπ) β β)) |
30 | 29 | anbi2d 630 |
. . . . . . . . 9
β’ (π₯ = -(πΊβπ) β ((π β§ π₯ β β) β (π β§ -(πΊβπ) β β))) |
31 | | stoweidlem23.2 |
. . . . . . . . . . . . . 14
β’
β²π‘πΊ |
32 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π‘π |
33 | 31, 32 | nffv 6856 |
. . . . . . . . . . . . 13
β’
β²π‘(πΊβπ) |
34 | 33 | nfneg 11405 |
. . . . . . . . . . . 12
β’
β²π‘-(πΊβπ) |
35 | 34 | nfeq2 2921 |
. . . . . . . . . . 11
β’
β²π‘ π₯ = -(πΊβπ) |
36 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π₯ = -(πΊβπ) β§ π‘ β π) β π₯ = -(πΊβπ)) |
37 | 35, 36 | mpteq2da 5207 |
. . . . . . . . . 10
β’ (π₯ = -(πΊβπ) β (π‘ β π β¦ π₯) = (π‘ β π β¦ -(πΊβπ))) |
38 | 37 | eleq1d 2819 |
. . . . . . . . 9
β’ (π₯ = -(πΊβπ) β ((π‘ β π β¦ π₯) β π΄ β (π‘ β π β¦ -(πΊβπ)) β π΄)) |
39 | 30, 38 | imbi12d 345 |
. . . . . . . 8
β’ (π₯ = -(πΊβπ) β (((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) β ((π β§ -(πΊβπ) β β) β (π‘ β π β¦ -(πΊβπ)) β π΄))) |
40 | | stoweidlem23.6 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
41 | 39, 40 | vtoclg 3527 |
. . . . . . 7
β’ (-(πΊβπ) β β β ((π β§ -(πΊβπ) β β) β (π‘ β π β¦ -(πΊβπ)) β π΄)) |
42 | 21, 28, 41 | sylc 65 |
. . . . . 6
β’ (π β (π‘ β π β¦ -(πΊβπ)) β π΄) |
43 | | stoweidlem23.5 |
. . . . . . 7
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
44 | | nfmpt1 5217 |
. . . . . . 7
β’
β²π‘(π‘ β π β¦ -(πΊβπ)) |
45 | 43, 31, 44 | stoweidlem8 44339 |
. . . . . 6
β’ ((π β§ πΊ β π΄ β§ (π‘ β π β¦ -(πΊβπ)) β π΄) β (π‘ β π β¦ ((πΊβπ‘) + ((π‘ β π β¦ -(πΊβπ))βπ‘))) β π΄) |
46 | 3, 42, 45 | mpd3an23 1464 |
. . . . 5
β’ (π β (π‘ β π β¦ ((πΊβπ‘) + ((π‘ β π β¦ -(πΊβπ))βπ‘))) β π΄) |
47 | 27, 46 | eqeltrrd 2835 |
. . . 4
β’ (π β (π‘ β π β¦ ((πΊβπ‘) + -(πΊβπ))) β π΄) |
48 | 19, 47 | eqeltrrd 2835 |
. . 3
β’ (π β (π‘ β π β¦ ((πΊβπ‘) β (πΊβπ))) β π΄) |
49 | 1, 48 | eqeltrid 2838 |
. 2
β’ (π β π» β π΄) |
50 | | stoweidlem23.7 |
. . . . . 6
β’ (π β π β π) |
51 | 11, 50 | ffvelcdmd 7040 |
. . . . 5
β’ (π β (πΊβπ) β β) |
52 | 51 | recnd 11191 |
. . . 4
β’ (π β (πΊβπ) β β) |
53 | 15 | recnd 11191 |
. . . 4
β’ (π β (πΊβπ) β β) |
54 | | stoweidlem23.10 |
. . . 4
β’ (π β (πΊβπ) β (πΊβπ)) |
55 | 52, 53, 54 | subne0d 11529 |
. . 3
β’ (π β ((πΊβπ) β (πΊβπ)) β 0) |
56 | 51, 15 | resubcld 11591 |
. . . 4
β’ (π β ((πΊβπ) β (πΊβπ)) β β) |
57 | | nfcv 2904 |
. . . . 5
β’
β²π‘π |
58 | 31, 57 | nffv 6856 |
. . . . . 6
β’
β²π‘(πΊβπ) |
59 | | nfcv 2904 |
. . . . . 6
β’
β²π‘
β |
60 | 58, 59, 33 | nfov 7391 |
. . . . 5
β’
β²π‘((πΊβπ) β (πΊβπ)) |
61 | | fveq2 6846 |
. . . . . 6
β’ (π‘ = π β (πΊβπ‘) = (πΊβπ)) |
62 | 61 | oveq1d 7376 |
. . . . 5
β’ (π‘ = π β ((πΊβπ‘) β (πΊβπ)) = ((πΊβπ) β (πΊβπ))) |
63 | 57, 60, 62, 1 | fvmptf 6973 |
. . . 4
β’ ((π β π β§ ((πΊβπ) β (πΊβπ)) β β) β (π»βπ) = ((πΊβπ) β (πΊβπ))) |
64 | 50, 56, 63 | syl2anc 585 |
. . 3
β’ (π β (π»βπ) = ((πΊβπ) β (πΊβπ))) |
65 | 15, 15 | resubcld 11591 |
. . . . 5
β’ (π β ((πΊβπ) β (πΊβπ)) β β) |
66 | 33, 59, 33 | nfov 7391 |
. . . . . 6
β’
β²π‘((πΊβπ) β (πΊβπ)) |
67 | | fveq2 6846 |
. . . . . . 7
β’ (π‘ = π β (πΊβπ‘) = (πΊβπ)) |
68 | 67 | oveq1d 7376 |
. . . . . 6
β’ (π‘ = π β ((πΊβπ‘) β (πΊβπ)) = ((πΊβπ) β (πΊβπ))) |
69 | 32, 66, 68, 1 | fvmptf 6973 |
. . . . 5
β’ ((π β π β§ ((πΊβπ) β (πΊβπ)) β β) β (π»βπ) = ((πΊβπ) β (πΊβπ))) |
70 | 14, 65, 69 | syl2anc 585 |
. . . 4
β’ (π β (π»βπ) = ((πΊβπ) β (πΊβπ))) |
71 | 53 | subidd 11508 |
. . . 4
β’ (π β ((πΊβπ) β (πΊβπ)) = 0) |
72 | 70, 71 | eqtrd 2773 |
. . 3
β’ (π β (π»βπ) = 0) |
73 | 55, 64, 72 | 3netr4d 3018 |
. 2
β’ (π β (π»βπ) β (π»βπ)) |
74 | 49, 73, 72 | 3jca 1129 |
1
β’ (π β (π» β π΄ β§ (π»βπ) β (π»βπ) β§ (π»βπ) = 0)) |