Step | Hyp | Ref
| Expression |
1 | | qrng.q |
. 2
β’ π = (βfld
βΎs β) |
2 | | qabsabv.a |
. 2
β’ π΄ = (AbsValβπ) |
3 | | ostthlem1.1 |
. 2
β’ (π β πΉ β π΄) |
4 | | ostthlem1.2 |
. 2
β’ (π β πΊ β π΄) |
5 | | eluz2nn 12816 |
. . 3
β’ (π β
(β€β₯β2) β π β β) |
6 | | fveq2 6847 |
. . . . . . 7
β’ (π = 1 β (πΉβπ) = (πΉβ1)) |
7 | | fveq2 6847 |
. . . . . . 7
β’ (π = 1 β (πΊβπ) = (πΊβ1)) |
8 | 6, 7 | eqeq12d 2753 |
. . . . . 6
β’ (π = 1 β ((πΉβπ) = (πΊβπ) β (πΉβ1) = (πΊβ1))) |
9 | 8 | imbi2d 341 |
. . . . 5
β’ (π = 1 β ((π β (πΉβπ) = (πΊβπ)) β (π β (πΉβ1) = (πΊβ1)))) |
10 | | fveq2 6847 |
. . . . . . 7
β’ (π = π¦ β (πΉβπ) = (πΉβπ¦)) |
11 | | fveq2 6847 |
. . . . . . 7
β’ (π = π¦ β (πΊβπ) = (πΊβπ¦)) |
12 | 10, 11 | eqeq12d 2753 |
. . . . . 6
β’ (π = π¦ β ((πΉβπ) = (πΊβπ) β (πΉβπ¦) = (πΊβπ¦))) |
13 | 12 | imbi2d 341 |
. . . . 5
β’ (π = π¦ β ((π β (πΉβπ) = (πΊβπ)) β (π β (πΉβπ¦) = (πΊβπ¦)))) |
14 | | fveq2 6847 |
. . . . . . 7
β’ (π = π§ β (πΉβπ) = (πΉβπ§)) |
15 | | fveq2 6847 |
. . . . . . 7
β’ (π = π§ β (πΊβπ) = (πΊβπ§)) |
16 | 14, 15 | eqeq12d 2753 |
. . . . . 6
β’ (π = π§ β ((πΉβπ) = (πΊβπ) β (πΉβπ§) = (πΊβπ§))) |
17 | 16 | imbi2d 341 |
. . . . 5
β’ (π = π§ β ((π β (πΉβπ) = (πΊβπ)) β (π β (πΉβπ§) = (πΊβπ§)))) |
18 | | fveq2 6847 |
. . . . . . 7
β’ (π = (π¦ Β· π§) β (πΉβπ) = (πΉβ(π¦ Β· π§))) |
19 | | fveq2 6847 |
. . . . . . 7
β’ (π = (π¦ Β· π§) β (πΊβπ) = (πΊβ(π¦ Β· π§))) |
20 | 18, 19 | eqeq12d 2753 |
. . . . . 6
β’ (π = (π¦ Β· π§) β ((πΉβπ) = (πΊβπ) β (πΉβ(π¦ Β· π§)) = (πΊβ(π¦ Β· π§)))) |
21 | 20 | imbi2d 341 |
. . . . 5
β’ (π = (π¦ Β· π§) β ((π β (πΉβπ) = (πΊβπ)) β (π β (πΉβ(π¦ Β· π§)) = (πΊβ(π¦ Β· π§))))) |
22 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
23 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (πΊβπ) = (πΊβπ)) |
24 | 22, 23 | eqeq12d 2753 |
. . . . . 6
β’ (π = π β ((πΉβπ) = (πΊβπ) β (πΉβπ) = (πΊβπ))) |
25 | 24 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β (πΉβπ) = (πΊβπ)) β (π β (πΉβπ) = (πΊβπ)))) |
26 | | ax-1ne0 11127 |
. . . . . . 7
β’ 1 β
0 |
27 | 1 | qrng1 26986 |
. . . . . . . 8
β’ 1 =
(1rβπ) |
28 | 1 | qrng0 26985 |
. . . . . . . 8
β’ 0 =
(0gβπ) |
29 | 2, 27, 28 | abv1z 20307 |
. . . . . . 7
β’ ((πΉ β π΄ β§ 1 β 0) β (πΉβ1) = 1) |
30 | 3, 26, 29 | sylancl 587 |
. . . . . 6
β’ (π β (πΉβ1) = 1) |
31 | 2, 27, 28 | abv1z 20307 |
. . . . . . 7
β’ ((πΊ β π΄ β§ 1 β 0) β (πΊβ1) = 1) |
32 | 4, 26, 31 | sylancl 587 |
. . . . . 6
β’ (π β (πΊβ1) = 1) |
33 | 30, 32 | eqtr4d 2780 |
. . . . 5
β’ (π β (πΉβ1) = (πΊβ1)) |
34 | | ostthlem2.3 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβπ) = (πΊβπ)) |
35 | 34 | expcom 415 |
. . . . 5
β’ (π β β β (π β (πΉβπ) = (πΊβπ))) |
36 | | jcab 519 |
. . . . . 6
β’ ((π β ((πΉβπ¦) = (πΊβπ¦) β§ (πΉβπ§) = (πΊβπ§))) β ((π β (πΉβπ¦) = (πΊβπ¦)) β§ (π β (πΉβπ§) = (πΊβπ§)))) |
37 | | oveq12 7371 |
. . . . . . . . 9
β’ (((πΉβπ¦) = (πΊβπ¦) β§ (πΉβπ§) = (πΊβπ§)) β ((πΉβπ¦) Β· (πΉβπ§)) = ((πΊβπ¦) Β· (πΊβπ§))) |
38 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β πΉ β π΄) |
39 | | eluzelz 12780 |
. . . . . . . . . . . . 13
β’ (π¦ β
(β€β₯β2) β π¦ β β€) |
40 | 39 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β π¦ β β€) |
41 | | zq 12886 |
. . . . . . . . . . . 12
β’ (π¦ β β€ β π¦ β
β) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β π¦ β β) |
43 | | eluzelz 12780 |
. . . . . . . . . . . . 13
β’ (π§ β
(β€β₯β2) β π§ β β€) |
44 | 43 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β π§ β β€) |
45 | | zq 12886 |
. . . . . . . . . . . 12
β’ (π§ β β€ β π§ β
β) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β π§ β β) |
47 | 1 | qrngbas 26983 |
. . . . . . . . . . . 12
β’ β =
(Baseβπ) |
48 | | qex 12893 |
. . . . . . . . . . . . 13
β’ β
β V |
49 | | cnfldmul 20818 |
. . . . . . . . . . . . . 14
β’ Β·
= (.rββfld) |
50 | 1, 49 | ressmulr 17195 |
. . . . . . . . . . . . 13
β’ (β
β V β Β· = (.rβπ)) |
51 | 48, 50 | ax-mp 5 |
. . . . . . . . . . . 12
β’ Β·
= (.rβπ) |
52 | 2, 47, 51 | abvmul 20304 |
. . . . . . . . . . 11
β’ ((πΉ β π΄ β§ π¦ β β β§ π§ β β) β (πΉβ(π¦ Β· π§)) = ((πΉβπ¦) Β· (πΉβπ§))) |
53 | 38, 42, 46, 52 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β (πΉβ(π¦ Β· π§)) = ((πΉβπ¦) Β· (πΉβπ§))) |
54 | 4 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β πΊ β π΄) |
55 | 2, 47, 51 | abvmul 20304 |
. . . . . . . . . . 11
β’ ((πΊ β π΄ β§ π¦ β β β§ π§ β β) β (πΊβ(π¦ Β· π§)) = ((πΊβπ¦) Β· (πΊβπ§))) |
56 | 54, 42, 46, 55 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β (πΊβ(π¦ Β· π§)) = ((πΊβπ¦) Β· (πΊβπ§))) |
57 | 53, 56 | eqeq12d 2753 |
. . . . . . . . 9
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β ((πΉβ(π¦ Β· π§)) = (πΊβ(π¦ Β· π§)) β ((πΉβπ¦) Β· (πΉβπ§)) = ((πΊβπ¦) Β· (πΊβπ§)))) |
58 | 37, 57 | syl5ibr 246 |
. . . . . . . 8
β’ ((π β§ (π¦ β (β€β₯β2)
β§ π§ β
(β€β₯β2))) β (((πΉβπ¦) = (πΊβπ¦) β§ (πΉβπ§) = (πΊβπ§)) β (πΉβ(π¦ Β· π§)) = (πΊβ(π¦ Β· π§)))) |
59 | 58 | expcom 415 |
. . . . . . 7
β’ ((π¦ β
(β€β₯β2) β§ π§ β (β€β₯β2))
β (π β (((πΉβπ¦) = (πΊβπ¦) β§ (πΉβπ§) = (πΊβπ§)) β (πΉβ(π¦ Β· π§)) = (πΊβ(π¦ Β· π§))))) |
60 | 59 | a2d 29 |
. . . . . 6
β’ ((π¦ β
(β€β₯β2) β§ π§ β (β€β₯β2))
β ((π β ((πΉβπ¦) = (πΊβπ¦) β§ (πΉβπ§) = (πΊβπ§))) β (π β (πΉβ(π¦ Β· π§)) = (πΊβ(π¦ Β· π§))))) |
61 | 36, 60 | biimtrrid 242 |
. . . . 5
β’ ((π¦ β
(β€β₯β2) β§ π§ β (β€β₯β2))
β (((π β (πΉβπ¦) = (πΊβπ¦)) β§ (π β (πΉβπ§) = (πΊβπ§))) β (π β (πΉβ(π¦ Β· π§)) = (πΊβ(π¦ Β· π§))))) |
62 | 9, 13, 17, 21, 25, 33, 35, 61 | prmind 16569 |
. . . 4
β’ (π β β β (π β (πΉβπ) = (πΊβπ))) |
63 | 62 | impcom 409 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = (πΊβπ)) |
64 | 5, 63 | sylan2 594 |
. 2
β’ ((π β§ π β (β€β₯β2))
β (πΉβπ) = (πΊβπ)) |
65 | 1, 2, 3, 4, 64 | ostthlem1 26991 |
1
β’ (π β πΉ = πΊ) |