Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. 2
β’ (π·βπΉ) = (π·βπΉ) |
2 | | fveqeq2 6851 |
. . . 4
β’ (π = πΉ β ((π·βπ) = (π·βπΉ) β (π·βπΉ) = (π·βπΉ))) |
3 | | fveq2 6842 |
. . . . . . . 8
β’ (π = πΉ β (πβπ) = (πβπΉ)) |
4 | 3 | cnveqd 5831 |
. . . . . . 7
β’ (π = πΉ β β‘(πβπ) = β‘(πβπΉ)) |
5 | 4 | imaeq1d 6012 |
. . . . . 6
β’ (π = πΉ β (β‘(πβπ) β {π}) = (β‘(πβπΉ) β {π})) |
6 | 5 | fveq2d 6846 |
. . . . 5
β’ (π = πΉ β (β―β(β‘(πβπ) β {π})) = (β―β(β‘(πβπΉ) β {π}))) |
7 | | fveq2 6842 |
. . . . 5
β’ (π = πΉ β (π·βπ) = (π·βπΉ)) |
8 | 6, 7 | breq12d 5118 |
. . . 4
β’ (π = πΉ β ((β―β(β‘(πβπ) β {π})) β€ (π·βπ) β (β―β(β‘(πβπΉ) β {π})) β€ (π·βπΉ))) |
9 | 2, 8 | imbi12d 344 |
. . 3
β’ (π = πΉ β (((π·βπ) = (π·βπΉ) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β ((π·βπΉ) = (π·βπΉ) β (β―β(β‘(πβπΉ) β {π})) β€ (π·βπΉ)))) |
10 | | fta1g.1 |
. . . . . 6
β’ (π β π
β IDomn) |
11 | | isidom 20774 |
. . . . . . 7
β’ (π
β IDomn β (π
β CRing β§ π
β Domn)) |
12 | 11 | simplbi 498 |
. . . . . 6
β’ (π
β IDomn β π
β CRing) |
13 | | crngring 19976 |
. . . . . 6
β’ (π
β CRing β π
β Ring) |
14 | 10, 12, 13 | 3syl 18 |
. . . . 5
β’ (π β π
β Ring) |
15 | | fta1g.2 |
. . . . 5
β’ (π β πΉ β π΅) |
16 | | fta1g.3 |
. . . . 5
β’ (π β πΉ β 0 ) |
17 | | fta1g.d |
. . . . . 6
β’ π· = ( deg1
βπ
) |
18 | | fta1g.p |
. . . . . 6
β’ π = (Poly1βπ
) |
19 | | fta1g.z |
. . . . . 6
β’ 0 =
(0gβπ) |
20 | | fta1g.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
21 | 17, 18, 19, 20 | deg1nn0cl 25453 |
. . . . 5
β’ ((π
β Ring β§ πΉ β π΅ β§ πΉ β 0 ) β (π·βπΉ) β
β0) |
22 | 14, 15, 16, 21 | syl3anc 1371 |
. . . 4
β’ (π β (π·βπΉ) β
β0) |
23 | | eqeq2 2748 |
. . . . . . . 8
β’ (π₯ = 0 β ((π·βπ) = π₯ β (π·βπ) = 0)) |
24 | 23 | imbi1d 341 |
. . . . . . 7
β’ (π₯ = 0 β (((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β ((π·βπ) = 0 β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
25 | 24 | ralbidv 3174 |
. . . . . 6
β’ (π₯ = 0 β (βπ β π΅ ((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β βπ β π΅ ((π·βπ) = 0 β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
26 | 25 | imbi2d 340 |
. . . . 5
β’ (π₯ = 0 β ((π
β IDomn β βπ β π΅ ((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) β (π
β IDomn β βπ β π΅ ((π·βπ) = 0 β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))))) |
27 | | eqeq2 2748 |
. . . . . . . 8
β’ (π₯ = π β ((π·βπ) = π₯ β (π·βπ) = π)) |
28 | 27 | imbi1d 341 |
. . . . . . 7
β’ (π₯ = π β (((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
29 | 28 | ralbidv 3174 |
. . . . . 6
β’ (π₯ = π β (βπ β π΅ ((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
30 | 29 | imbi2d 340 |
. . . . 5
β’ (π₯ = π β ((π
β IDomn β βπ β π΅ ((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) β (π
β IDomn β βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))))) |
31 | | eqeq2 2748 |
. . . . . . . 8
β’ (π₯ = (π + 1) β ((π·βπ) = π₯ β (π·βπ) = (π + 1))) |
32 | 31 | imbi1d 341 |
. . . . . . 7
β’ (π₯ = (π + 1) β (((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β ((π·βπ) = (π + 1) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
33 | 32 | ralbidv 3174 |
. . . . . 6
β’ (π₯ = (π + 1) β (βπ β π΅ ((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β βπ β π΅ ((π·βπ) = (π + 1) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
34 | 33 | imbi2d 340 |
. . . . 5
β’ (π₯ = (π + 1) β ((π
β IDomn β βπ β π΅ ((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) β (π
β IDomn β βπ β π΅ ((π·βπ) = (π + 1) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))))) |
35 | | eqeq2 2748 |
. . . . . . . 8
β’ (π₯ = (π·βπΉ) β ((π·βπ) = π₯ β (π·βπ) = (π·βπΉ))) |
36 | 35 | imbi1d 341 |
. . . . . . 7
β’ (π₯ = (π·βπΉ) β (((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β ((π·βπ) = (π·βπΉ) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
37 | 36 | ralbidv 3174 |
. . . . . 6
β’ (π₯ = (π·βπΉ) β (βπ β π΅ ((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β βπ β π΅ ((π·βπ) = (π·βπΉ) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
38 | 37 | imbi2d 340 |
. . . . 5
β’ (π₯ = (π·βπΉ) β ((π
β IDomn β βπ β π΅ ((π·βπ) = π₯ β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) β (π
β IDomn β βπ β π΅ ((π·βπ) = (π·βπΉ) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))))) |
39 | | simprr 771 |
. . . . . . . . . . . . . 14
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (π·βπ) = 0) |
40 | | 0nn0 12428 |
. . . . . . . . . . . . . 14
β’ 0 β
β0 |
41 | 39, 40 | eqeltrdi 2845 |
. . . . . . . . . . . . 13
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (π·βπ) β
β0) |
42 | 12, 13 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π
β IDomn β π
β Ring) |
43 | | simpl 483 |
. . . . . . . . . . . . . 14
β’ ((π β π΅ β§ (π·βπ) = 0) β π β π΅) |
44 | 17, 18, 19, 20 | deg1nn0clb 25455 |
. . . . . . . . . . . . . 14
β’ ((π
β Ring β§ π β π΅) β (π β 0 β (π·βπ) β
β0)) |
45 | 42, 43, 44 | syl2an 596 |
. . . . . . . . . . . . 13
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (π β 0 β (π·βπ) β
β0)) |
46 | 41, 45 | mpbird 256 |
. . . . . . . . . . . 12
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β π β 0 ) |
47 | | simplrr 776 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β (π·βπ) = 0) |
48 | | 0le0 12254 |
. . . . . . . . . . . . . . . . 17
β’ 0 β€
0 |
49 | 47, 48 | eqbrtrdi 5144 |
. . . . . . . . . . . . . . . 16
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β (π·βπ) β€ 0) |
50 | 42 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β π
β Ring) |
51 | | simplrl 775 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β π β π΅) |
52 | | eqid 2736 |
. . . . . . . . . . . . . . . . . 18
β’
(algScβπ) =
(algScβπ) |
53 | 17, 18, 20, 52 | deg1le0 25476 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Ring β§ π β π΅) β ((π·βπ) β€ 0 β π = ((algScβπ)β((coe1βπ)β0)))) |
54 | 50, 51, 53 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β ((π·βπ) β€ 0 β π = ((algScβπ)β((coe1βπ)β0)))) |
55 | 49, 54 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β π = ((algScβπ)β((coe1βπ)β0))) |
56 | 55 | fveq2d 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β (πβπ) = (πβ((algScβπ)β((coe1βπ)β0)))) |
57 | 12 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β π
β CRing) |
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β π
β CRing) |
59 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(coe1βπ) = (coe1βπ) |
60 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(Baseβπ
) =
(Baseβπ
) |
61 | 59, 20, 18, 60 | coe1f 21582 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π΅ β (coe1βπ):β0βΆ(Baseβπ
)) |
62 | 51, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β (coe1βπ):β0βΆ(Baseβπ
)) |
63 | | ffvelcdm 7032 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((coe1βπ):β0βΆ(Baseβπ
) β§ 0 β
β0) β ((coe1βπ)β0) β (Baseβπ
)) |
64 | 62, 40, 63 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β ((coe1βπ)β0) β
(Baseβπ
)) |
65 | | fta1g.o |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (eval1βπ
) |
66 | 65, 18, 60, 52 | evl1sca 21700 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β CRing β§
((coe1βπ)β0) β (Baseβπ
)) β (πβ((algScβπ)β((coe1βπ)β0))) =
((Baseβπ
) Γ
{((coe1βπ)β0)})) |
67 | 58, 64, 66 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β (πβ((algScβπ)β((coe1βπ)β0))) =
((Baseβπ
) Γ
{((coe1βπ)β0)})) |
68 | 56, 67 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β (πβπ) = ((Baseβπ
) Γ {((coe1βπ)β0)})) |
69 | 68 | fveq1d 6844 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β ((πβπ)βπ₯) = (((Baseβπ
) Γ {((coe1βπ)β0)})βπ₯)) |
70 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π
βs
(Baseβπ
)) = (π
βs
(Baseβπ
)) |
71 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . 20
β’
(Baseβ(π
βs (Baseβπ
))) = (Baseβ(π
βs (Baseβπ
))) |
72 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β π
β IDomn) |
73 | | fvexd 6857 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (Baseβπ
) β V) |
74 | 65, 18, 70, 60 | evl1rhm 21698 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π
β CRing β π β (π RingHom (π
βs (Baseβπ
)))) |
75 | 20, 71 | rhmf 20158 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π RingHom (π
βs (Baseβπ
))) β π:π΅βΆ(Baseβ(π
βs (Baseβπ
)))) |
76 | 57, 74, 75 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β π:π΅βΆ(Baseβ(π
βs (Baseβπ
)))) |
77 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β π β π΅) |
78 | 76, 77 | ffvelcdmd 7036 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (πβπ) β (Baseβ(π
βs (Baseβπ
)))) |
79 | 70, 60, 71, 72, 73, 78 | pwselbas 17371 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (πβπ):(Baseβπ
)βΆ(Baseβπ
)) |
80 | | ffn 6668 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ):(Baseβπ
)βΆ(Baseβπ
) β (πβπ) Fn (Baseβπ
)) |
81 | | fniniseg 7010 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ) Fn (Baseβπ
) β (π₯ β (β‘(πβπ) β {π}) β (π₯ β (Baseβπ
) β§ ((πβπ)βπ₯) = π))) |
82 | 79, 80, 81 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (π₯ β (β‘(πβπ) β {π}) β (π₯ β (Baseβπ
) β§ ((πβπ)βπ₯) = π))) |
83 | 82 | simplbda 500 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β ((πβπ)βπ₯) = π) |
84 | 82 | simprbda 499 |
. . . . . . . . . . . . . . . . . 18
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β π₯ β (Baseβπ
)) |
85 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . 19
β’
((coe1βπ)β0) β V |
86 | 85 | fvconst2 7153 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (Baseβπ
) β (((Baseβπ
) Γ
{((coe1βπ)β0)})βπ₯) = ((coe1βπ)β0)) |
87 | 84, 86 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β (((Baseβπ
) Γ {((coe1βπ)β0)})βπ₯) =
((coe1βπ)β0)) |
88 | 69, 83, 87 | 3eqtr3rd 2785 |
. . . . . . . . . . . . . . . 16
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β ((coe1βπ)β0) = π) |
89 | 88 | fveq2d 6846 |
. . . . . . . . . . . . . . 15
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β ((algScβπ)β((coe1βπ)β0)) =
((algScβπ)βπ)) |
90 | | fta1g.w |
. . . . . . . . . . . . . . . . 17
β’ π = (0gβπ
) |
91 | 18, 52, 90, 19 | ply1scl0 21661 |
. . . . . . . . . . . . . . . 16
β’ (π
β Ring β
((algScβπ)βπ) = 0 ) |
92 | 50, 91 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β ((algScβπ)βπ) = 0 ) |
93 | 55, 89, 92 | 3eqtrd 2780 |
. . . . . . . . . . . . . 14
β’ (((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β§ π₯ β (β‘(πβπ) β {π})) β π = 0 ) |
94 | 93 | ex 413 |
. . . . . . . . . . . . 13
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (π₯ β (β‘(πβπ) β {π}) β π = 0 )) |
95 | 94 | necon3ad 2956 |
. . . . . . . . . . . 12
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (π β 0 β Β¬ π₯ β (β‘(πβπ) β {π}))) |
96 | 46, 95 | mpd 15 |
. . . . . . . . . . 11
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β Β¬ π₯ β (β‘(πβπ) β {π})) |
97 | 96 | eq0rdv 4364 |
. . . . . . . . . 10
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (β‘(πβπ) β {π}) = β
) |
98 | 97 | fveq2d 6846 |
. . . . . . . . 9
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (β―β(β‘(πβπ) β {π})) =
(β―ββ
)) |
99 | | hash0 14267 |
. . . . . . . . 9
β’
(β―ββ
) = 0 |
100 | 98, 99 | eqtrdi 2792 |
. . . . . . . 8
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (β―β(β‘(πβπ) β {π})) = 0) |
101 | 48, 39 | breqtrrid 5143 |
. . . . . . . 8
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β 0 β€ (π·βπ)) |
102 | 100, 101 | eqbrtrd 5127 |
. . . . . . 7
β’ ((π
β IDomn β§ (π β π΅ β§ (π·βπ) = 0)) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) |
103 | 102 | expr 457 |
. . . . . 6
β’ ((π
β IDomn β§ π β π΅) β ((π·βπ) = 0 β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) |
104 | 103 | ralrimiva 3143 |
. . . . 5
β’ (π
β IDomn β
βπ β π΅ ((π·βπ) = 0 β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) |
105 | | fveqeq2 6851 |
. . . . . . . . . 10
β’ (π = π β ((π·βπ) = π β (π·βπ) = π)) |
106 | | fveq2 6842 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
107 | 106 | cnveqd 5831 |
. . . . . . . . . . . . 13
β’ (π = π β β‘(πβπ) = β‘(πβπ)) |
108 | 107 | imaeq1d 6012 |
. . . . . . . . . . . 12
β’ (π = π β (β‘(πβπ) β {π}) = (β‘(πβπ) β {π})) |
109 | 108 | fveq2d 6846 |
. . . . . . . . . . 11
β’ (π = π β (β―β(β‘(πβπ) β {π})) = (β―β(β‘(πβπ) β {π}))) |
110 | | fveq2 6842 |
. . . . . . . . . . 11
β’ (π = π β (π·βπ) = (π·βπ)) |
111 | 109, 110 | breq12d 5118 |
. . . . . . . . . 10
β’ (π = π β ((β―β(β‘(πβπ) β {π})) β€ (π·βπ) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) |
112 | 105, 111 | imbi12d 344 |
. . . . . . . . 9
β’ (π = π β (((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
113 | 112 | cbvralvw 3225 |
. . . . . . . 8
β’
(βπ β
π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) |
114 | | simprr 771 |
. . . . . . . . . . . . . . . 16
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β (π·βπ) = (π + 1)) |
115 | | peano2nn0 12453 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π + 1) β
β0) |
116 | 115 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β (π + 1) β
β0) |
117 | 114, 116 | eqeltrd 2837 |
. . . . . . . . . . . . . . 15
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β (π·βπ) β
β0) |
118 | 117 | nn0ge0d 12476 |
. . . . . . . . . . . . . 14
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β 0 β€ (π·βπ)) |
119 | | fveq2 6842 |
. . . . . . . . . . . . . . . 16
β’ ((β‘(πβπ) β {π}) = β
β (β―β(β‘(πβπ) β {π})) =
(β―ββ
)) |
120 | 119, 99 | eqtrdi 2792 |
. . . . . . . . . . . . . . 15
β’ ((β‘(πβπ) β {π}) = β
β (β―β(β‘(πβπ) β {π})) = 0) |
121 | 120 | breq1d 5115 |
. . . . . . . . . . . . . 14
β’ ((β‘(πβπ) β {π}) = β
β ((β―β(β‘(πβπ) β {π})) β€ (π·βπ) β 0 β€ (π·βπ))) |
122 | 118, 121 | syl5ibrcom 246 |
. . . . . . . . . . . . 13
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β ((β‘(πβπ) β {π}) = β
β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) |
123 | 122 | a1dd 50 |
. . . . . . . . . . . 12
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β ((β‘(πβπ) β {π}) = β
β (βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
124 | | n0 4306 |
. . . . . . . . . . . . 13
β’ ((β‘(πβπ) β {π}) β β
β βπ₯ π₯ β (β‘(πβπ) β {π})) |
125 | | simplll 773 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β§ (π₯ β (β‘(πβπ) β {π}) β§ βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) β π
β IDomn) |
126 | | simplrl 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β§ (π₯ β (β‘(πβπ) β {π}) β§ βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) β π β π΅) |
127 | | eqid 2736 |
. . . . . . . . . . . . . . . 16
β’
(var1βπ
) = (var1βπ
) |
128 | | eqid 2736 |
. . . . . . . . . . . . . . . 16
β’
(-gβπ) = (-gβπ) |
129 | | eqid 2736 |
. . . . . . . . . . . . . . . 16
β’
((var1βπ
)(-gβπ)((algScβπ)βπ₯)) = ((var1βπ
)(-gβπ)((algScβπ)βπ₯)) |
130 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β§ (π₯ β (β‘(πβπ) β {π}) β§ βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) β π β β0) |
131 | | simplrr 776 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β§ (π₯ β (β‘(πβπ) β {π}) β§ βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) β (π·βπ) = (π + 1)) |
132 | | simprl 769 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β§ (π₯ β (β‘(πβπ) β {π}) β§ βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) β π₯ β (β‘(πβπ) β {π})) |
133 | | simprr 771 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β§ (π₯ β (β‘(πβπ) β {π}) β§ βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) β βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) |
134 | 18, 20, 17, 65, 90, 19, 125, 126, 60, 127, 128, 52, 129, 130, 131, 132, 133 | fta1glem2 25531 |
. . . . . . . . . . . . . . 15
β’ ((((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β§ (π₯ β (β‘(πβπ) β {π}) β§ βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) |
135 | 134 | exp32 421 |
. . . . . . . . . . . . . 14
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β (π₯ β (β‘(πβπ) β {π}) β (βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
136 | 135 | exlimdv 1936 |
. . . . . . . . . . . . 13
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β (βπ₯ π₯ β (β‘(πβπ) β {π}) β (βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
137 | 124, 136 | biimtrid 241 |
. . . . . . . . . . . 12
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β ((β‘(πβπ) β {π}) β β
β (βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
138 | 123, 137 | pm2.61dne 3031 |
. . . . . . . . . . 11
β’ (((π
β IDomn β§ π β β0)
β§ (π β π΅ β§ (π·βπ) = (π + 1))) β (βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) |
139 | 138 | expr 457 |
. . . . . . . . . 10
β’ (((π
β IDomn β§ π β β0)
β§ π β π΅) β ((π·βπ) = (π + 1) β (βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
140 | 139 | com23 86 |
. . . . . . . . 9
β’ (((π
β IDomn β§ π β β0)
β§ π β π΅) β (βπ β π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β ((π·βπ) = (π + 1) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
141 | 140 | ralrimdva 3151 |
. . . . . . . 8
β’ ((π
β IDomn β§ π β β0)
β (βπ β
π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β βπ β π΅ ((π·βπ) = (π + 1) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
142 | 113, 141 | biimtrid 241 |
. . . . . . 7
β’ ((π
β IDomn β§ π β β0)
β (βπ β
π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β βπ β π΅ ((π·βπ) = (π + 1) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
143 | 142 | expcom 414 |
. . . . . 6
β’ (π β β0
β (π
β IDomn
β (βπ β
π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)) β βπ β π΅ ((π·βπ) = (π + 1) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))))) |
144 | 143 | a2d 29 |
. . . . 5
β’ (π β β0
β ((π
β IDomn
β βπ β
π΅ ((π·βπ) = π β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) β (π
β IDomn β βπ β π΅ ((π·βπ) = (π + 1) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))))) |
145 | 26, 30, 34, 38, 104, 144 | nn0ind 12598 |
. . . 4
β’ ((π·βπΉ) β β0 β (π
β IDomn β
βπ β π΅ ((π·βπ) = (π·βπΉ) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ)))) |
146 | 22, 10, 145 | sylc 65 |
. . 3
β’ (π β βπ β π΅ ((π·βπ) = (π·βπΉ) β (β―β(β‘(πβπ) β {π})) β€ (π·βπ))) |
147 | 9, 146, 15 | rspcdva 3582 |
. 2
β’ (π β ((π·βπΉ) = (π·βπΉ) β (β―β(β‘(πβπΉ) β {π})) β€ (π·βπΉ))) |
148 | 1, 147 | mpi 20 |
1
β’ (π β (β―β(β‘(πβπΉ) β {π})) β€ (π·βπΉ)) |