Step | Hyp | Ref
| Expression |
1 | | iftrue 4497 |
. . . . 5
โข (๐ โ ๐ด โ if(๐ โ ๐ด, ๐ถ, 1) = ๐ถ) |
2 | 1 | prodeq2i 15809 |
. . . 4
โข
โ๐ โ
๐ด if(๐ โ ๐ด, ๐ถ, 1) = โ๐ โ ๐ด ๐ถ |
3 | | ssun1 4137 |
. . . . . 6
โข ๐ด โ (๐ด โช ๐ต) |
4 | | fprodsplit.2 |
. . . . . 6
โข (๐ โ ๐ = (๐ด โช ๐ต)) |
5 | 3, 4 | sseqtrrid 4002 |
. . . . 5
โข (๐ โ ๐ด โ ๐) |
6 | 1 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ if(๐ โ ๐ด, ๐ถ, 1) = ๐ถ) |
7 | 5 | sselda 3949 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ ๐ โ ๐) |
8 | | fprodsplit.4 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐) โ ๐ถ โ โ) |
9 | 7, 8 | syldan 592 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ) |
10 | 6, 9 | eqeltrd 2838 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ if(๐ โ ๐ด, ๐ถ, 1) โ โ) |
11 | | eldifn 4092 |
. . . . . . 7
โข (๐ โ (๐ โ ๐ด) โ ยฌ ๐ โ ๐ด) |
12 | 11 | iffalsed 4502 |
. . . . . 6
โข (๐ โ (๐ โ ๐ด) โ if(๐ โ ๐ด, ๐ถ, 1) = 1) |
13 | 12 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ (๐ โ ๐ด)) โ if(๐ โ ๐ด, ๐ถ, 1) = 1) |
14 | | fprodsplit.3 |
. . . . 5
โข (๐ โ ๐ โ Fin) |
15 | 5, 10, 13, 14 | fprodss 15838 |
. . . 4
โข (๐ โ โ๐ โ ๐ด if(๐ โ ๐ด, ๐ถ, 1) = โ๐ โ ๐ if(๐ โ ๐ด, ๐ถ, 1)) |
16 | 2, 15 | eqtr3id 2791 |
. . 3
โข (๐ โ โ๐ โ ๐ด ๐ถ = โ๐ โ ๐ if(๐ โ ๐ด, ๐ถ, 1)) |
17 | | iftrue 4497 |
. . . . 5
โข (๐ โ ๐ต โ if(๐ โ ๐ต, ๐ถ, 1) = ๐ถ) |
18 | 17 | prodeq2i 15809 |
. . . 4
โข
โ๐ โ
๐ต if(๐ โ ๐ต, ๐ถ, 1) = โ๐ โ ๐ต ๐ถ |
19 | | ssun2 4138 |
. . . . . 6
โข ๐ต โ (๐ด โช ๐ต) |
20 | 19, 4 | sseqtrrid 4002 |
. . . . 5
โข (๐ โ ๐ต โ ๐) |
21 | 17 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ต) โ if(๐ โ ๐ต, ๐ถ, 1) = ๐ถ) |
22 | 20 | sselda 3949 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ ๐ โ ๐) |
23 | 22, 8 | syldan 592 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ต) โ ๐ถ โ โ) |
24 | 21, 23 | eqeltrd 2838 |
. . . . 5
โข ((๐ โง ๐ โ ๐ต) โ if(๐ โ ๐ต, ๐ถ, 1) โ โ) |
25 | | eldifn 4092 |
. . . . . . 7
โข (๐ โ (๐ โ ๐ต) โ ยฌ ๐ โ ๐ต) |
26 | 25 | iffalsed 4502 |
. . . . . 6
โข (๐ โ (๐ โ ๐ต) โ if(๐ โ ๐ต, ๐ถ, 1) = 1) |
27 | 26 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ (๐ โ ๐ต)) โ if(๐ โ ๐ต, ๐ถ, 1) = 1) |
28 | 20, 24, 27, 14 | fprodss 15838 |
. . . 4
โข (๐ โ โ๐ โ ๐ต if(๐ โ ๐ต, ๐ถ, 1) = โ๐ โ ๐ if(๐ โ ๐ต, ๐ถ, 1)) |
29 | 18, 28 | eqtr3id 2791 |
. . 3
โข (๐ โ โ๐ โ ๐ต ๐ถ = โ๐ โ ๐ if(๐ โ ๐ต, ๐ถ, 1)) |
30 | 16, 29 | oveq12d 7380 |
. 2
โข (๐ โ (โ๐ โ ๐ด ๐ถ ยท โ๐ โ ๐ต ๐ถ) = (โ๐ โ ๐ if(๐ โ ๐ด, ๐ถ, 1) ยท โ๐ โ ๐ if(๐ โ ๐ต, ๐ถ, 1))) |
31 | | ax-1cn 11116 |
. . . 4
โข 1 โ
โ |
32 | | ifcl 4536 |
. . . 4
โข ((๐ถ โ โ โง 1 โ
โ) โ if(๐ โ
๐ด, ๐ถ, 1) โ โ) |
33 | 8, 31, 32 | sylancl 587 |
. . 3
โข ((๐ โง ๐ โ ๐) โ if(๐ โ ๐ด, ๐ถ, 1) โ โ) |
34 | | ifcl 4536 |
. . . 4
โข ((๐ถ โ โ โง 1 โ
โ) โ if(๐ โ
๐ต, ๐ถ, 1) โ โ) |
35 | 8, 31, 34 | sylancl 587 |
. . 3
โข ((๐ โง ๐ โ ๐) โ if(๐ โ ๐ต, ๐ถ, 1) โ โ) |
36 | 14, 33, 35 | fprodmul 15850 |
. 2
โข (๐ โ โ๐ โ ๐ (if(๐ โ ๐ด, ๐ถ, 1) ยท if(๐ โ ๐ต, ๐ถ, 1)) = (โ๐ โ ๐ if(๐ โ ๐ด, ๐ถ, 1) ยท โ๐ โ ๐ if(๐ โ ๐ต, ๐ถ, 1))) |
37 | 4 | eleq2d 2824 |
. . . . . 6
โข (๐ โ (๐ โ ๐ โ ๐ โ (๐ด โช ๐ต))) |
38 | | elun 4113 |
. . . . . 6
โข (๐ โ (๐ด โช ๐ต) โ (๐ โ ๐ด โจ ๐ โ ๐ต)) |
39 | 37, 38 | bitrdi 287 |
. . . . 5
โข (๐ โ (๐ โ ๐ โ (๐ โ ๐ด โจ ๐ โ ๐ต))) |
40 | 39 | biimpa 478 |
. . . 4
โข ((๐ โง ๐ โ ๐) โ (๐ โ ๐ด โจ ๐ โ ๐ต)) |
41 | | fprodsplit.1 |
. . . . . . . . 9
โข (๐ โ (๐ด โฉ ๐ต) = โ
) |
42 | | disjel 4421 |
. . . . . . . . 9
โข (((๐ด โฉ ๐ต) = โ
โง ๐ โ ๐ด) โ ยฌ ๐ โ ๐ต) |
43 | 41, 42 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ด) โ ยฌ ๐ โ ๐ต) |
44 | 43 | iffalsed 4502 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ด) โ if(๐ โ ๐ต, ๐ถ, 1) = 1) |
45 | 6, 44 | oveq12d 7380 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (if(๐ โ ๐ด, ๐ถ, 1) ยท if(๐ โ ๐ต, ๐ถ, 1)) = (๐ถ ยท 1)) |
46 | 9 | mulid1d 11179 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ด) โ (๐ถ ยท 1) = ๐ถ) |
47 | 45, 46 | eqtrd 2777 |
. . . . 5
โข ((๐ โง ๐ โ ๐ด) โ (if(๐ โ ๐ด, ๐ถ, 1) ยท if(๐ โ ๐ต, ๐ถ, 1)) = ๐ถ) |
48 | 43 | ex 414 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐ด โ ยฌ ๐ โ ๐ต)) |
49 | 48 | con2d 134 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐ต โ ยฌ ๐ โ ๐ด)) |
50 | 49 | imp 408 |
. . . . . . . 8
โข ((๐ โง ๐ โ ๐ต) โ ยฌ ๐ โ ๐ด) |
51 | 50 | iffalsed 4502 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ if(๐ โ ๐ด, ๐ถ, 1) = 1) |
52 | 51, 21 | oveq12d 7380 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ต) โ (if(๐ โ ๐ด, ๐ถ, 1) ยท if(๐ โ ๐ต, ๐ถ, 1)) = (1 ยท ๐ถ)) |
53 | 23 | mulid2d 11180 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ต) โ (1 ยท ๐ถ) = ๐ถ) |
54 | 52, 53 | eqtrd 2777 |
. . . . 5
โข ((๐ โง ๐ โ ๐ต) โ (if(๐ โ ๐ด, ๐ถ, 1) ยท if(๐ โ ๐ต, ๐ถ, 1)) = ๐ถ) |
55 | 47, 54 | jaodan 957 |
. . . 4
โข ((๐ โง (๐ โ ๐ด โจ ๐ โ ๐ต)) โ (if(๐ โ ๐ด, ๐ถ, 1) ยท if(๐ โ ๐ต, ๐ถ, 1)) = ๐ถ) |
56 | 40, 55 | syldan 592 |
. . 3
โข ((๐ โง ๐ โ ๐) โ (if(๐ โ ๐ด, ๐ถ, 1) ยท if(๐ โ ๐ต, ๐ถ, 1)) = ๐ถ) |
57 | 56 | prodeq2dv 15813 |
. 2
โข (๐ โ โ๐ โ ๐ (if(๐ โ ๐ด, ๐ถ, 1) ยท if(๐ โ ๐ต, ๐ถ, 1)) = โ๐ โ ๐ ๐ถ) |
58 | 30, 36, 57 | 3eqtr2rd 2784 |
1
โข (๐ โ โ๐ โ ๐ ๐ถ = (โ๐ โ ๐ด ๐ถ ยท โ๐ โ ๐ต ๐ถ)) |