Step | Hyp | Ref
| Expression |
1 | | prodeq1 15858 |
. . . 4
โข (๐ฅ = โ
โ โ๐ โ ๐ฅ ๐ต = โ๐ โ โ
๐ต) |
2 | 1 | fveq2d 6896 |
. . 3
โข (๐ฅ = โ
โ
(absโโ๐ โ
๐ฅ ๐ต) = (absโโ๐ โ โ
๐ต)) |
3 | | prodeq1 15858 |
. . 3
โข (๐ฅ = โ
โ โ๐ โ ๐ฅ (absโ๐ต) = โ๐ โ โ
(absโ๐ต)) |
4 | 2, 3 | eqeq12d 2747 |
. 2
โข (๐ฅ = โ
โ
((absโโ๐ โ
๐ฅ ๐ต) = โ๐ โ ๐ฅ (absโ๐ต) โ (absโโ๐ โ โ
๐ต) = โ๐ โ โ
(absโ๐ต))) |
5 | | prodeq1 15858 |
. . . 4
โข (๐ฅ = ๐ฆ โ โ๐ โ ๐ฅ ๐ต = โ๐ โ ๐ฆ ๐ต) |
6 | 5 | fveq2d 6896 |
. . 3
โข (๐ฅ = ๐ฆ โ (absโโ๐ โ ๐ฅ ๐ต) = (absโโ๐ โ ๐ฆ ๐ต)) |
7 | | prodeq1 15858 |
. . 3
โข (๐ฅ = ๐ฆ โ โ๐ โ ๐ฅ (absโ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) |
8 | 6, 7 | eqeq12d 2747 |
. 2
โข (๐ฅ = ๐ฆ โ ((absโโ๐ โ ๐ฅ ๐ต) = โ๐ โ ๐ฅ (absโ๐ต) โ (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต))) |
9 | | prodeq1 15858 |
. . . 4
โข (๐ฅ = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ฅ ๐ต = โ๐ โ (๐ฆ โช {๐ง})๐ต) |
10 | 9 | fveq2d 6896 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ (absโโ๐ โ ๐ฅ ๐ต) = (absโโ๐ โ (๐ฆ โช {๐ง})๐ต)) |
11 | | prodeq1 15858 |
. . 3
โข (๐ฅ = (๐ฆ โช {๐ง}) โ โ๐ โ ๐ฅ (absโ๐ต) = โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต)) |
12 | 10, 11 | eqeq12d 2747 |
. 2
โข (๐ฅ = (๐ฆ โช {๐ง}) โ ((absโโ๐ โ ๐ฅ ๐ต) = โ๐ โ ๐ฅ (absโ๐ต) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต))) |
13 | | prodeq1 15858 |
. . . 4
โข (๐ฅ = ๐ด โ โ๐ โ ๐ฅ ๐ต = โ๐ โ ๐ด ๐ต) |
14 | 13 | fveq2d 6896 |
. . 3
โข (๐ฅ = ๐ด โ (absโโ๐ โ ๐ฅ ๐ต) = (absโโ๐ โ ๐ด ๐ต)) |
15 | | prodeq1 15858 |
. . 3
โข (๐ฅ = ๐ด โ โ๐ โ ๐ฅ (absโ๐ต) = โ๐ โ ๐ด (absโ๐ต)) |
16 | 14, 15 | eqeq12d 2747 |
. 2
โข (๐ฅ = ๐ด โ ((absโโ๐ โ ๐ฅ ๐ต) = โ๐ โ ๐ฅ (absโ๐ต) โ (absโโ๐ โ ๐ด ๐ต) = โ๐ โ ๐ด (absโ๐ต))) |
17 | | abs1 15249 |
. . . 4
โข
(absโ1) = 1 |
18 | | prod0 15892 |
. . . . 5
โข
โ๐ โ
โ
๐ต =
1 |
19 | 18 | fveq2i 6895 |
. . . 4
โข
(absโโ๐
โ โ
๐ต) =
(absโ1) |
20 | | prod0 15892 |
. . . 4
โข
โ๐ โ
โ
(absโ๐ต) =
1 |
21 | 17, 19, 20 | 3eqtr4i 2769 |
. . 3
โข
(absโโ๐
โ โ
๐ต) =
โ๐ โ โ
(absโ๐ต) |
22 | 21 | a1i 11 |
. 2
โข (๐ โ (absโโ๐ โ โ
๐ต) = โ๐ โ โ
(absโ๐ต)) |
23 | | eqidd 2732 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต)) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
24 | | nfv 1916 |
. . . . . . . 8
โข
โฒ๐(๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) |
25 | | nfcsb1v 3919 |
. . . . . . . 8
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต |
26 | | fprodabs2.a |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ Fin) |
27 | 26 | adantr 480 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ด โ Fin) |
28 | | simpr 484 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ฆ โ ๐ด) |
29 | | ssfi 9176 |
. . . . . . . . . 10
โข ((๐ด โ Fin โง ๐ฆ โ ๐ด) โ ๐ฆ โ Fin) |
30 | 27, 28, 29 | syl2anc 583 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ ๐ด) โ ๐ฆ โ Fin) |
31 | 30 | adantrr 714 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ฆ โ Fin) |
32 | | simprr 770 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ (๐ด โ ๐ฆ)) |
33 | 32 | eldifbd 3962 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ยฌ ๐ง โ ๐ฆ) |
34 | | simpll 764 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐) |
35 | 28 | sselda 3983 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ด) โง ๐ โ ๐ฆ) โ ๐ โ ๐ด) |
36 | 35 | adantlrr 718 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ โ ๐ด) |
37 | | fprodabs2.b |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
38 | 34, 36, 37 | syl2anc 583 |
. . . . . . . 8
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ ๐ต โ โ) |
39 | | csbeq1a 3908 |
. . . . . . . 8
โข (๐ = ๐ง โ ๐ต = โฆ๐ง / ๐โฆ๐ต) |
40 | | simpl 482 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐) |
41 | 32 | eldifad 3961 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ๐ง โ ๐ด) |
42 | | nfv 1916 |
. . . . . . . . . . 11
โข
โฒ๐(๐ โง ๐ง โ ๐ด) |
43 | 25 | nfel1 2918 |
. . . . . . . . . . 11
โข
โฒ๐โฆ๐ง / ๐โฆ๐ต โ โ |
44 | 42, 43 | nfim 1898 |
. . . . . . . . . 10
โข
โฒ๐((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
45 | | eleq1w 2815 |
. . . . . . . . . . . 12
โข (๐ = ๐ง โ (๐ โ ๐ด โ ๐ง โ ๐ด)) |
46 | 45 | anbi2d 628 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ ((๐ โง ๐ โ ๐ด) โ (๐ โง ๐ง โ ๐ด))) |
47 | 39 | eleq1d 2817 |
. . . . . . . . . . 11
โข (๐ = ๐ง โ (๐ต โ โ โ โฆ๐ง / ๐โฆ๐ต โ โ)) |
48 | 46, 47 | imbi12d 343 |
. . . . . . . . . 10
โข (๐ = ๐ง โ (((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ ((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ))) |
49 | 44, 48, 37 | chvarfv 2232 |
. . . . . . . . 9
โข ((๐ โง ๐ง โ ๐ด) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
50 | 40, 41, 49 | syl2anc 583 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โฆ๐ง / ๐โฆ๐ต โ โ) |
51 | 24, 25, 31, 32, 33, 38, 39, 50 | fprodsplitsn 15938 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
52 | 51 | adantr 480 |
. . . . . 6
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ โ๐ โ (๐ฆ โช {๐ง})๐ต = (โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) |
53 | 52 | fveq2d 6896 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = (absโ(โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต))) |
54 | 24, 31, 38 | fprodclf 15941 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ ๐ฆ ๐ต โ โ) |
55 | 54, 50 | absmuld 15406 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (absโ(โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) = ((absโโ๐ โ ๐ฆ ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
56 | 55 | adantr 480 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (absโ(โ๐ โ ๐ฆ ๐ต ยท โฆ๐ง / ๐โฆ๐ต)) = ((absโโ๐ โ ๐ฆ ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
57 | | oveq1 7419 |
. . . . . 6
โข
((absโโ๐
โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต) โ ((absโโ๐ โ ๐ฆ ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต)) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
58 | 57 | adantl 481 |
. . . . 5
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ ((absโโ๐ โ ๐ฆ ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต)) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
59 | 53, 56, 58 | 3eqtrd 2775 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
60 | | nfcv 2902 |
. . . . . . 7
โข
โฒ๐abs |
61 | 60, 25 | nffv 6902 |
. . . . . 6
โข
โฒ๐(absโโฆ๐ง / ๐โฆ๐ต) |
62 | 38 | abscld 15388 |
. . . . . . 7
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ (absโ๐ต) โ โ) |
63 | 62 | recnd 11247 |
. . . . . 6
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง ๐ โ ๐ฆ) โ (absโ๐ต) โ โ) |
64 | 39 | fveq2d 6896 |
. . . . . 6
โข (๐ = ๐ง โ (absโ๐ต) = (absโโฆ๐ง / ๐โฆ๐ต)) |
65 | 50 | abscld 15388 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (absโโฆ๐ง / ๐โฆ๐ต) โ โ) |
66 | 65 | recnd 11247 |
. . . . . 6
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ (absโโฆ๐ง / ๐โฆ๐ต) โ โ) |
67 | 24, 61, 31, 32, 33, 63, 64, 66 | fprodsplitsn 15938 |
. . . . 5
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
68 | 67 | adantr 480 |
. . . 4
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต) = (โ๐ โ ๐ฆ (absโ๐ต) ยท (absโโฆ๐ง / ๐โฆ๐ต))) |
69 | 23, 59, 68 | 3eqtr4d 2781 |
. . 3
โข (((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โง (absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต)) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต)) |
70 | 69 | ex 412 |
. 2
โข ((๐ โง (๐ฆ โ ๐ด โง ๐ง โ (๐ด โ ๐ฆ))) โ ((absโโ๐ โ ๐ฆ ๐ต) = โ๐ โ ๐ฆ (absโ๐ต) โ (absโโ๐ โ (๐ฆ โช {๐ง})๐ต) = โ๐ โ (๐ฆ โช {๐ง})(absโ๐ต))) |
71 | 4, 8, 12, 16, 22, 70, 26 | findcard2d 9169 |
1
โข (๐ โ (absโโ๐ โ ๐ด ๐ต) = โ๐ โ ๐ด (absโ๐ต)) |