Step | Hyp | Ref
| Expression |
1 | | prodeq1 15793 |
. . . 4
โข (๐ฅ = โ
โ โ๐ โ ๐ฅ ๐ต = โ๐ โ โ
๐ต) |
2 | 1 | fveq2d 6847 |
. . 3
โข (๐ฅ = โ
โ
(absโโ๐ โ
๐ฅ ๐ต) = (absโโ๐ โ โ
๐ต)) |
3 | | prodeq1 15793 |
. . 3
โข (๐ฅ = โ
โ โ๐ โ ๐ฅ (absโ๐ต) = โ๐ โ โ
(absโ๐ต)) |
4 | 2, 3 | eqeq12d 2753 |
. 2
โข (๐ฅ = โ
โ
((absโโ๐ โ
๐ฅ ๐ต) = โ๐ โ ๐ฅ (absโ๐ต) โ (absโโ๐ โ โ
๐ต) = โ๐ โ โ
(absโ๐ต))) |
5 | | prodeq1 15793 |
. . . 4
โข (๐ฅ = ๐ฆ โ โ๐ โ ๐ฅ ๐ต = โ๐ โ ๐ฆ ๐ต) |
6 | 5 | fveq2d 6847 |
. . 3
โข (๐ฅ = ๐ฆ โ (absโโ๐ โ ๐ฅ ๐ต) = (absโโ๐ โ ๐ฆ ๐ต)) |
7 | | prodeq1 15793 |
. . 3
โข (๐ฅ = ๐ฆ โ โ๐ โ ๐ฅ (absโ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) |
8 | 6, 7 | eqeq12d 2753 |
. 2
โข (๐ฅ = ๐ฆ โ ((absโโ๐ โ ๐ฅ ๐ต) = โ๐ โ ๐ฅ (absโ๐ต) โ (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต))) |
9 | | prodeq1 15793 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ฅ ๐ต = โ๐ โ (๐ฆ โช {๐ง})๐ต) |
10 | 9 | fveq2d 6847 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (absโโ๐ โ ๐ฅ ๐ต) = (absโโ๐ โ (๐ฆ โช {๐ง})๐ต)) |
11 | | prodeq1 15793 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ฅ (absโ๐ต) = โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต)) |
12 | 10, 11 | eqeq12d 2753 |
. 2
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((absโโ๐ โ ๐ฅ ๐ต) = โ๐ โ ๐ฅ (absโ๐ต) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต))) |
13 | | prodeq1 15793 |
. . . 4
โข (๐ฅ = ๐ด โ โ๐ โ ๐ฅ ๐ต = โ๐ โ ๐ด ๐ต) |
14 | 13 | fveq2d 6847 |
. . 3
โข (๐ฅ = ๐ด โ (absโโ๐ โ ๐ฅ ๐ต) = (absโโ๐ โ ๐ด ๐ต)) |
15 | | prodeq1 15793 |
. . 3
โข (๐ฅ = ๐ด โ โ๐ โ ๐ฅ (absโ๐ต) = โ๐ โ ๐ด (absโ๐ต)) |
16 | 14, 15 | eqeq12d 2753 |
. 2
โข (๐ฅ = ๐ด โ ((absโโ๐ โ ๐ฅ ๐ต) = โ๐ โ ๐ฅ (absโ๐ต) โ (absโโ๐ โ ๐ด ๐ต) = โ๐ โ ๐ด (absโ๐ต))) |
17 | | abs1 15183 |
. . . 4
โข
(absโ1) = 1 |
18 | | prod0 15827 |
. . . . 5
โข
โ๐ โ
โ
๐ต =
1 |
19 | 18 | fveq2i 6846 |
. . . 4
โข
(absโโ๐
โ โ
๐ต) =
(absโ1) |
20 | | prod0 15827 |
. . . 4
โข
โ๐ โ
โ
(absโ๐ต) =
1 |
21 | 17, 19, 20 | 3eqtr4i 2775 |
. . 3
โข
(absโโ๐
โ โ
๐ต) =
โ๐ โ โ
(absโ๐ต) |
22 | 21 | a1i 11 |
. 2
โข (๐ โ (absโโ๐ โ โ
๐ต) = โ๐ โ โ
(absโ๐ต)) |
23 | | eqidd 2738 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต)) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
24 | | nfv 1918 |
. . . . . . . 8
โข
โฒ๐(๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) |
25 | | nfcsb1v 3881 |
. . . . . . . 8
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต |
26 | | fprodabs2.a |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ Fin) |
27 | 26 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ด โ Fin) |
28 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ฆ โ ๐ด) |
29 | | ssfi 9118 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง ๐ฆ โ ๐ด) โ ๐ฆ โ Fin) |
30 | 27, 28, 29 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ฆ โ Fin) |
31 | 30 | adantrr 716 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ฆ โ Fin) |
32 | | simprr 772 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ (๐ด โ ๐ฆ)) |
33 | 32 | eldifbd 3924 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ยฌ ๐ง โ ๐ฆ) |
34 | | simpll 766 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐) |
35 | 28 | sselda 3945 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ด) โง ๐ โ ๐ฆ) โ ๐ โ ๐ด) |
36 | 35 | adantlrr 720 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ โ ๐ด) |
37 | | fprodabs2.b |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
38 | 34, 36, 37 | syl2anc 585 |
. . . . . . . 8
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
39 | | csbeq1a 3870 |
. . . . . . . 8
โข (๐ = ๐ง โ ๐ต = โฆ๐ง / ๐โฆ๐ต) |
40 | | simpl 484 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐) |
41 | 32 | eldifad 3923 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ ๐ด) |
42 | | nfv 1918 |
. . . . . . . . . . 11
โข
โฒ๐(๐ โง ๐ง โ ๐ด) |
43 | 25 | nfel1 2924 |
. . . . . . . . . . 11
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต โ โ |
44 | 42, 43 | nfim 1900 |
. . . . . . . . . 10
โข
โฒ๐((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
45 | | eleq1w 2821 |
. . . . . . . . . . . 12
โข (๐ = ๐ง โ (๐ โ ๐ด โ ๐ง โ ๐ด)) |
46 | 45 | anbi2d 630 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ ((๐ โง ๐ โ ๐ด) โ (๐ โง ๐ง โ ๐ด))) |
47 | 39 | eleq1d 2823 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ (๐ต โ โ โ โฆ๐ง / ๐โฆ๐ต โ โ)) |
48 | 46, 47 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ ((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ))) |
49 | 44, 48, 37 | chvarfv 2234 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
50 | 40, 41, 49 | syl2anc 585 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
51 | 24, 25, 31, 32, 33, 38, 39, 50 | fprodsplitsn 15873 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
52 | 51 | adantr 482 |
. . . . . 6
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
53 | 52 | fveq2d 6847 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = (absโ(โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต))) |
54 | 24, 31, 38 | fprodclf 15876 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ต โ โ) |
55 | 54, 50 | absmuld 15340 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (absโ(โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) = ((absโโ๐ โ ๐ฆ ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
56 | 55 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (absโ(โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) = ((absโโ๐ โ ๐ฆ ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
57 | | oveq1 7365 |
. . . . . 6
โข
((absโโ๐
โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต) โ ((absโโ๐ โ ๐ฆ ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต)) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
58 | 57 | adantl 483 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ ((absโโ๐ โ ๐ฆ ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต)) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
59 | 53, 56, 58 | 3eqtrd 2781 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
60 | | nfcv 2908 |
. . . . . . 7
โข
โฒ๐abs |
61 | 60, 25 | nffv 6853 |
. . . . . 6
โข
โฒ๐(absโโฆ๐ง / ๐โฆ๐ต) |
62 | 38 | abscld 15322 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ (absโ๐ต) โ โ) |
63 | 62 | recnd 11184 |
. . . . . 6
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ (absโ๐ต) โ โ) |
64 | 39 | fveq2d 6847 |
. . . . . 6
โข (๐ = ๐ง โ (absโ๐ต) = (absโโฆ๐ง / ๐โฆ๐ต)) |
65 | 50 | abscld 15322 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (absโโฆ๐ง / ๐โฆ๐ต) โ โ) |
66 | 65 | recnd 11184 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (absโโฆ๐ง / ๐โฆ๐ต) โ โ) |
67 | 24, 61, 31, 32, 33, 63, 64, 66 | fprodsplitsn 15873 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
68 | 67 | adantr 482 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
69 | 23, 59, 68 | 3eqtr4d 2787 |
. . 3
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต)) |
70 | 69 | ex 414 |
. 2
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ((absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต))) |
71 | 4, 8, 12, 16, 22, 70, 26 | findcard2d 9111 |
1
โข (๐ โ (absโโ๐ โ ๐ด ๐ต) = โ๐ โ ๐ด (absโ๐ต)) |