Step | Hyp | Ref
| Expression |
1 | | 1t1e1 9070 |
. . . . 5
β’ (1
Β· 1) = 1 |
2 | | prod0 11592 |
. . . . . 6
β’
βπ β
β
π΅ =
1 |
3 | | prod0 11592 |
. . . . . 6
β’
βπ β
β
πΆ =
1 |
4 | 2, 3 | oveq12i 5886 |
. . . . 5
β’
(βπ β
β
π΅ Β·
βπ β β
πΆ) = (1 Β·
1) |
5 | | prod0 11592 |
. . . . 5
β’
βπ β
β
(π΅ Β· πΆ) = 1 |
6 | 1, 4, 5 | 3eqtr4ri 2209 |
. . . 4
β’
βπ β
β
(π΅ Β· πΆ) = (βπ β β
π΅ Β· βπ β β
πΆ) |
7 | | prodeq1 11560 |
. . . 4
β’ (π΄ = β
β βπ β π΄ (π΅ Β· πΆ) = βπ β β
(π΅ Β· πΆ)) |
8 | | prodeq1 11560 |
. . . . 5
β’ (π΄ = β
β βπ β π΄ π΅ = βπ β β
π΅) |
9 | | prodeq1 11560 |
. . . . 5
β’ (π΄ = β
β βπ β π΄ πΆ = βπ β β
πΆ) |
10 | 8, 9 | oveq12d 5892 |
. . . 4
β’ (π΄ = β
β (βπ β π΄ π΅ Β· βπ β π΄ πΆ) = (βπ β β
π΅ Β· βπ β β
πΆ)) |
11 | 6, 7, 10 | 3eqtr4a 2236 |
. . 3
β’ (π΄ = β
β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ)) |
12 | 11 | a1i 9 |
. 2
β’ (π β (π΄ = β
β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ))) |
13 | | simprl 529 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
14 | | nnuz 9562 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
15 | 13, 14 | eleqtrdi 2270 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
16 | | elnnuz 9563 |
. . . . . . . . . . . 12
β’ (π β β β π β
(β€β₯β1)) |
17 | 16 | biimpri 133 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β1) β π β β) |
18 | 17 | adantl 277 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β π β
β) |
19 | | fprodmul.2 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β π΅ β β) |
20 | 19 | fmpttd 5671 |
. . . . . . . . . . . . . . 15
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
21 | 20 | adantr 276 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π΅):π΄βΆβ) |
22 | | f1of 5461 |
. . . . . . . . . . . . . . 15
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
23 | 22 | ad2antll 491 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
24 | | fco 5381 |
. . . . . . . . . . . . . 14
β’ (((π β π΄ β¦ π΅):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
25 | 21, 23, 24 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
26 | 25 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
27 | | simpr 110 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
π β€ (β―βπ΄)) |
28 | | simplr 528 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
π β
(β€β₯β1)) |
29 | 13 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(β―βπ΄) β
β) |
30 | 29 | nnzd 9373 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(β―βπ΄) β
β€) |
31 | | elfz5 10016 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β1) β§ (β―βπ΄) β β€) β (π β (1...(β―βπ΄)) β π β€ (β―βπ΄))) |
32 | 28, 30, 31 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(π β
(1...(β―βπ΄))
β π β€
(β―βπ΄))) |
33 | 27, 32 | mpbird 167 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
π β
(1...(β―βπ΄))) |
34 | 26, 33 | ffvelcdmd 5652 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(((π β π΄ β¦ π΅) β π)βπ) β β) |
35 | | 1cnd 7972 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ Β¬ π β€
(β―βπ΄)) β 1
β β) |
36 | 18 | nnzd 9373 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β π β
β€) |
37 | 13 | adantr 276 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β (β―βπ΄)
β β) |
38 | 37 | nnzd 9373 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β (β―βπ΄)
β β€) |
39 | | zdcle 9328 |
. . . . . . . . . . . 12
β’ ((π β β€ β§
(β―βπ΄) β
β€) β DECID π β€ (β―βπ΄)) |
40 | 36, 38, 39 | syl2anc 411 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β DECID π β€ (β―βπ΄)) |
41 | 34, 35, 40 | ifcldadc 3563 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) β β) |
42 | | breq1 4006 |
. . . . . . . . . . . 12
β’ (π = π β (π β€ (β―βπ΄) β π β€ (β―βπ΄))) |
43 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π = π β (((π β π΄ β¦ π΅) β π)βπ) = (((π β π΄ β¦ π΅) β π)βπ)) |
44 | 42, 43 | ifbieq1d 3556 |
. . . . . . . . . . 11
β’ (π = π β if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) = if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1)) |
45 | | eqid 2177 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1)) = (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1)) |
46 | 44, 45 | fvmptg 5592 |
. . . . . . . . . 10
β’ ((π β β β§ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) β β) β ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1))βπ) = if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1)) |
47 | 18, 41, 46 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1))βπ) = if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1)) |
48 | 47, 41 | eqeltrd 2254 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1))βπ) β β) |
49 | | fprodmul.3 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β πΆ β β) |
50 | 49 | fmpttd 5671 |
. . . . . . . . . . . . . . 15
β’ (π β (π β π΄ β¦ πΆ):π΄βΆβ) |
51 | 50 | adantr 276 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ πΆ):π΄βΆβ) |
52 | | fco 5381 |
. . . . . . . . . . . . . 14
β’ (((π β π΄ β¦ πΆ):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ πΆ) β π):(1...(β―βπ΄))βΆβ) |
53 | 51, 23, 52 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ πΆ) β π):(1...(β―βπ΄))βΆβ) |
54 | 53 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
((π β π΄ β¦ πΆ) β π):(1...(β―βπ΄))βΆβ) |
55 | 54, 33 | ffvelcdmd 5652 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(((π β π΄ β¦ πΆ) β π)βπ) β β) |
56 | 55, 35, 40 | ifcldadc 3563 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β if(π β€
(β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1) β β) |
57 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π = π β (((π β π΄ β¦ πΆ) β π)βπ) = (((π β π΄ β¦ πΆ) β π)βπ)) |
58 | 42, 57 | ifbieq1d 3556 |
. . . . . . . . . . 11
β’ (π = π β if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1) = if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)) |
59 | | eqid 2177 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)) = (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)) |
60 | 58, 59 | fvmptg 5592 |
. . . . . . . . . 10
β’ ((π β β β§ if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1) β β) β ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))βπ) = if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)) |
61 | 18, 56, 60 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))βπ) = if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)) |
62 | 61, 56 | eqeltrd 2254 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))βπ) β β) |
63 | 23 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
π:(1...(β―βπ΄))βΆπ΄) |
64 | 63, 33 | ffvelcdmd 5652 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(πβπ) β π΄) |
65 | | csbov12g 5913 |
. . . . . . . . . . . . . 14
β’ ((πβπ) β π΄ β β¦(πβπ) / πβ¦(π΅ Β· πΆ) = (β¦(πβπ) / πβ¦π΅ Β· β¦(πβπ) / πβ¦πΆ)) |
66 | 64, 65 | syl 14 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
β¦(πβπ) / πβ¦(π΅ Β· πΆ) = (β¦(πβπ) / πβ¦π΅ Β· β¦(πβπ) / πβ¦πΆ)) |
67 | 19, 49 | mulcld 7977 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΄) β (π΅ Β· πΆ) β β) |
68 | 67 | ralrimiva 2550 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ β π΄ (π΅ Β· πΆ) β β) |
69 | 68 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
βπ β π΄ (π΅ Β· πΆ) β β) |
70 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . 17
β’
β²πβ¦(πβπ) / πβ¦(π΅ Β· πΆ) |
71 | 70 | nfel1 2330 |
. . . . . . . . . . . . . . . 16
β’
β²πβ¦(πβπ) / πβ¦(π΅ Β· πΆ) β β |
72 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β (π΅ Β· πΆ) = β¦(πβπ) / πβ¦(π΅ Β· πΆ)) |
73 | 72 | eleq1d 2246 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β ((π΅ Β· πΆ) β β β
β¦(πβπ) / πβ¦(π΅ Β· πΆ) β β)) |
74 | 71, 73 | rspc 2835 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β π΄ β (βπ β π΄ (π΅ Β· πΆ) β β β
β¦(πβπ) / πβ¦(π΅ Β· πΆ) β β)) |
75 | 64, 69, 74 | sylc 62 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
β¦(πβπ) / πβ¦(π΅ Β· πΆ) β β) |
76 | | eqid 2177 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β¦ (π΅ Β· πΆ)) = (π β π΄ β¦ (π΅ Β· πΆ)) |
77 | 76 | fvmpts 5594 |
. . . . . . . . . . . . . 14
β’ (((πβπ) β π΄ β§ β¦(πβπ) / πβ¦(π΅ Β· πΆ) β β) β ((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ)) = β¦(πβπ) / πβ¦(π΅ Β· πΆ)) |
78 | 64, 75, 77 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ)) = β¦(πβπ) / πβ¦(π΅ Β· πΆ)) |
79 | 19 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ β π΄ π΅ β β) |
80 | 79 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
βπ β π΄ π΅ β β) |
81 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . 18
β’
β²πβ¦(πβπ) / πβ¦π΅ |
82 | 81 | nfel1 2330 |
. . . . . . . . . . . . . . . . 17
β’
β²πβ¦(πβπ) / πβ¦π΅ β β |
83 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β π΅ = β¦(πβπ) / πβ¦π΅) |
84 | 83 | eleq1d 2246 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β (π΅ β β β β¦(πβπ) / πβ¦π΅ β β)) |
85 | 82, 84 | rspc 2835 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β π΄ β (βπ β π΄ π΅ β β β β¦(πβπ) / πβ¦π΅ β β)) |
86 | 64, 80, 85 | sylc 62 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
β¦(πβπ) / πβ¦π΅ β β) |
87 | | eqid 2177 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
88 | 87 | fvmpts 5594 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) β π΄ β§ β¦(πβπ) / πβ¦π΅ β β) β ((π β π΄ β¦ π΅)β(πβπ)) = β¦(πβπ) / πβ¦π΅) |
89 | 64, 86, 88 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
((π β π΄ β¦ π΅)β(πβπ)) = β¦(πβπ) / πβ¦π΅) |
90 | 49 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ β π΄ πΆ β β) |
91 | 90 | ad3antrrr 492 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
βπ β π΄ πΆ β β) |
92 | | nfcsb1v 3090 |
. . . . . . . . . . . . . . . . . 18
β’
β²πβ¦(πβπ) / πβ¦πΆ |
93 | 92 | nfel1 2330 |
. . . . . . . . . . . . . . . . 17
β’
β²πβ¦(πβπ) / πβ¦πΆ β β |
94 | | csbeq1a 3066 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβπ) β πΆ = β¦(πβπ) / πβ¦πΆ) |
95 | 94 | eleq1d 2246 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβπ) β (πΆ β β β β¦(πβπ) / πβ¦πΆ β β)) |
96 | 93, 95 | rspc 2835 |
. . . . . . . . . . . . . . . 16
β’ ((πβπ) β π΄ β (βπ β π΄ πΆ β β β β¦(πβπ) / πβ¦πΆ β β)) |
97 | 64, 91, 96 | sylc 62 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
β¦(πβπ) / πβ¦πΆ β β) |
98 | | eqid 2177 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ πΆ) = (π β π΄ β¦ πΆ) |
99 | 98 | fvmpts 5594 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) β π΄ β§ β¦(πβπ) / πβ¦πΆ β β) β ((π β π΄ β¦ πΆ)β(πβπ)) = β¦(πβπ) / πβ¦πΆ) |
100 | 64, 97, 99 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
((π β π΄ β¦ πΆ)β(πβπ)) = β¦(πβπ) / πβ¦πΆ) |
101 | 89, 100 | oveq12d 5892 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(((π β π΄ β¦ π΅)β(πβπ)) Β· ((π β π΄ β¦ πΆ)β(πβπ))) = (β¦(πβπ) / πβ¦π΅ Β· β¦(πβπ) / πβ¦πΆ)) |
102 | 66, 78, 101 | 3eqtr4d 2220 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) Β· ((π β π΄ β¦ πΆ)β(πβπ)))) |
103 | | fvco3 5587 |
. . . . . . . . . . . . 13
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ) = ((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ))) |
104 | 63, 33, 103 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ) = ((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ))) |
105 | | fvco3 5587 |
. . . . . . . . . . . . . 14
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
106 | 63, 33, 105 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
107 | | fvco3 5587 |
. . . . . . . . . . . . . 14
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
108 | 63, 33, 107 | syl2anc 411 |
. . . . . . . . . . . . 13
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(((π β π΄ β¦ πΆ) β π)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
109 | 106, 108 | oveq12d 5892 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
((((π β π΄ β¦ π΅) β π)βπ) Β· (((π β π΄ β¦ πΆ) β π)βπ)) = (((π β π΄ β¦ π΅)β(πβπ)) Β· ((π β π΄ β¦ πΆ)β(πβπ)))) |
110 | 102, 104,
109 | 3eqtr4d 2220 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ) = ((((π β π΄ β¦ π΅) β π)βπ) Β· (((π β π΄ β¦ πΆ) β π)βπ))) |
111 | 27 | iftrued 3541 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1) = (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ)) |
112 | 27 | iftrued 3541 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) = (((π β π΄ β¦ π΅) β π)βπ)) |
113 | 27 | iftrued 3541 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
if(π β€
(β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1) = (((π β π΄ β¦ πΆ) β π)βπ)) |
114 | 112, 113 | oveq12d 5892 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) Β· if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)) = ((((π β π΄ β¦ π΅) β π)βπ) Β· (((π β π΄ β¦ πΆ) β π)βπ))) |
115 | 110, 111,
114 | 3eqtr4d 2220 |
. . . . . . . . . 10
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1) = (if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) Β· if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))) |
116 | 1 | eqcomi 2181 |
. . . . . . . . . . 11
β’ 1 = (1
Β· 1) |
117 | | simpr 110 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ Β¬ π β€
(β―βπ΄)) β
Β¬ π β€
(β―βπ΄)) |
118 | 117 | iffalsed 3544 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ Β¬ π β€
(β―βπ΄)) β
if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1) = 1) |
119 | 117 | iffalsed 3544 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ Β¬ π β€
(β―βπ΄)) β
if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) = 1) |
120 | 117 | iffalsed 3544 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ Β¬ π β€
(β―βπ΄)) β
if(π β€
(β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1) = 1) |
121 | 119, 120 | oveq12d 5892 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ Β¬ π β€
(β―βπ΄)) β
(if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) Β· if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)) = (1 Β· 1)) |
122 | 116, 118,
121 | 3eqtr4a 2236 |
. . . . . . . . . 10
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ Β¬ π β€
(β―βπ΄)) β
if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1) = (if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) Β· if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))) |
123 | | exmiddc 836 |
. . . . . . . . . . 11
β’
(DECID π β€ (β―βπ΄) β (π β€ (β―βπ΄) β¨ Β¬ π β€ (β―βπ΄))) |
124 | 40, 123 | syl 14 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β (π β€
(β―βπ΄) β¨
Β¬ π β€
(β―βπ΄))) |
125 | 115, 122,
124 | mpjaodan 798 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1) = (if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) Β· if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))) |
126 | 78, 75 | eqeltrd 2254 |
. . . . . . . . . . . 12
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ)) β β) |
127 | 104, 126 | eqeltrd 2254 |
. . . . . . . . . . 11
β’ ((((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β§ π β€
(β―βπ΄)) β
(((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ) β β) |
128 | 127, 35, 40 | ifcldadc 3563 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1) β β) |
129 | | fveq2 5515 |
. . . . . . . . . . . 12
β’ (π = π β (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ) = (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ)) |
130 | 42, 129 | ifbieq1d 3556 |
. . . . . . . . . . 11
β’ (π = π β if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1) = if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1)) |
131 | | eqid 2177 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1)) = (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1)) |
132 | 130, 131 | fvmptg 5592 |
. . . . . . . . . 10
β’ ((π β β β§ if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1) β β) β ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1))βπ) = if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1)) |
133 | 18, 128, 132 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1))βπ) = if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1)) |
134 | 47, 61 | oveq12d 5892 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β (((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1))βπ) Β· ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))βπ)) = (if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1) Β· if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))) |
135 | 125, 133,
134 | 3eqtr4d 2220 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (β€β₯β1))
β ((π β β
β¦ if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1))βπ) = (((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1))βπ) Β· ((π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1))βπ))) |
136 | 15, 48, 62, 135 | prod3fmul 11548 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (seq1( Β· ,
(π β β β¦
if(π β€
(β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1)))β(β―βπ΄)) = ((seq1( Β· , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1)))β(β―βπ΄)) Β· (seq1( Β· ,
(π β β β¦
if(π β€
(β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)))β(β―βπ΄)))) |
137 | | fveq2 5515 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ (π΅ Β· πΆ))βπ) = ((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ))) |
138 | | simprr 531 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
139 | 67 | fmpttd 5671 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ (π΅ Β· πΆ)):π΄βΆβ) |
140 | 139 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ (π΅ Β· πΆ)):π΄βΆβ) |
141 | 140 | ffvelcdmda 5651 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ (π΅ Β· πΆ))βπ) β β) |
142 | | fvco3 5587 |
. . . . . . . . 9
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ) = ((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ))) |
143 | 23, 142 | sylan 283 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ) = ((π β π΄ β¦ (π΅ Β· πΆ))β(πβπ))) |
144 | 137, 13, 138, 141, 143 | fprodseq 11590 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ (π΅ Β· πΆ))βπ) = (seq1( Β· , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ (π΅ Β· πΆ)) β π)βπ), 1)))β(β―βπ΄))) |
145 | | fveq2 5515 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
146 | 21 | ffvelcdmda 5651 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
147 | | fvco3 5587 |
. . . . . . . . . 10
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
148 | 23, 147 | sylan 283 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
149 | 145, 13, 138, 146, 148 | fprodseq 11590 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( Β· , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1)))β(β―βπ΄))) |
150 | | fveq2 5515 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΄ β¦ πΆ)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
151 | 51 | ffvelcdmda 5651 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) β β) |
152 | | fvco3 5587 |
. . . . . . . . . 10
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
153 | 23, 152 | sylan 283 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
154 | 150, 13, 138, 151, 153 | fprodseq 11590 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = (seq1( Β· , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)))β(β―βπ΄))) |
155 | 149, 154 | oveq12d 5892 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (βπ β π΄ ((π β π΄ β¦ π΅)βπ) Β· βπ β π΄ ((π β π΄ β¦ πΆ)βπ)) = ((seq1( Β· , (π β β β¦ if(π β€ (β―βπ΄), (((π β π΄ β¦ π΅) β π)βπ), 1)))β(β―βπ΄)) Β· (seq1( Β· ,
(π β β β¦
if(π β€
(β―βπ΄), (((π β π΄ β¦ πΆ) β π)βπ), 1)))β(β―βπ΄)))) |
156 | 136, 144,
155 | 3eqtr4d 2220 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ (π΅ Β· πΆ))βπ) = (βπ β π΄ ((π β π΄ β¦ π΅)βπ) Β· βπ β π΄ ((π β π΄ β¦ πΆ)βπ))) |
157 | | prodfct 11594 |
. . . . . . . 8
β’
(βπ β
π΄ (π΅ Β· πΆ) β β β βπ β π΄ ((π β π΄ β¦ (π΅ Β· πΆ))βπ) = βπ β π΄ (π΅ Β· πΆ)) |
158 | 68, 157 | syl 14 |
. . . . . . 7
β’ (π β βπ β π΄ ((π β π΄ β¦ (π΅ Β· πΆ))βπ) = βπ β π΄ (π΅ Β· πΆ)) |
159 | 158 | adantr 276 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ (π΅ Β· πΆ))βπ) = βπ β π΄ (π΅ Β· πΆ)) |
160 | | prodfct 11594 |
. . . . . . . . 9
β’
(βπ β
π΄ π΅ β β β βπ β π΄ ((π β π΄ β¦ π΅)βπ) = βπ β π΄ π΅) |
161 | 79, 160 | syl 14 |
. . . . . . . 8
β’ (π β βπ β π΄ ((π β π΄ β¦ π΅)βπ) = βπ β π΄ π΅) |
162 | | prodfct 11594 |
. . . . . . . . 9
β’
(βπ β
π΄ πΆ β β β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΄ πΆ) |
163 | 90, 162 | syl 14 |
. . . . . . . 8
β’ (π β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΄ πΆ) |
164 | 161, 163 | oveq12d 5892 |
. . . . . . 7
β’ (π β (βπ β π΄ ((π β π΄ β¦ π΅)βπ) Β· βπ β π΄ ((π β π΄ β¦ πΆ)βπ)) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ)) |
165 | 164 | adantr 276 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (βπ β π΄ ((π β π΄ β¦ π΅)βπ) Β· βπ β π΄ ((π β π΄ β¦ πΆ)βπ)) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ)) |
166 | 156, 159,
165 | 3eqtr3d 2218 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ)) |
167 | 166 | expr 375 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ))) |
168 | 167 | exlimdv 1819 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ))) |
169 | 168 | expimpd 363 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ))) |
170 | | fprodmul.1 |
. . 3
β’ (π β π΄ β Fin) |
171 | | fz1f1o 11382 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
172 | 170, 171 | syl 14 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
173 | 12, 169, 172 | mpjaod 718 |
1
β’ (π β βπ β π΄ (π΅ Β· πΆ) = (βπ β π΄ π΅ Β· βπ β π΄ πΆ)) |