Step | Hyp | Ref
| Expression |
1 | | prodeq1 15799 |
. . . 4
โข (๐ค = โ
โ โ๐ โ ๐ค ๐ถ = โ๐ โ โ
๐ถ) |
2 | 1 | mpteq2dv 5212 |
. . 3
โข (๐ค = โ
โ (๐ฅ โ ๐ด โฆ โ๐ โ ๐ค ๐ถ) = (๐ฅ โ ๐ด โฆ โ๐ โ โ
๐ถ)) |
3 | 2 | eleq1d 2823 |
. 2
โข (๐ค = โ
โ ((๐ฅ โ ๐ด โฆ โ๐ โ ๐ค ๐ถ) โ (๐ดโcnโโ) โ (๐ฅ โ ๐ด โฆ โ๐ โ โ
๐ถ) โ (๐ดโcnโโ))) |
4 | | prodeq1 15799 |
. . . 4
โข (๐ค = ๐ง โ โ๐ โ ๐ค ๐ถ = โ๐ โ ๐ง ๐ถ) |
5 | 4 | mpteq2dv 5212 |
. . 3
โข (๐ค = ๐ง โ (๐ฅ โ ๐ด โฆ โ๐ โ ๐ค ๐ถ) = (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ)) |
6 | 5 | eleq1d 2823 |
. 2
โข (๐ค = ๐ง โ ((๐ฅ โ ๐ด โฆ โ๐ โ ๐ค ๐ถ) โ (๐ดโcnโโ) โ (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ))) |
7 | | prodeq1 15799 |
. . . 4
โข (๐ค = (๐ง โช {๐ฆ}) โ โ๐ โ ๐ค ๐ถ = โ๐ โ (๐ง โช {๐ฆ})๐ถ) |
8 | 7 | mpteq2dv 5212 |
. . 3
โข (๐ค = (๐ง โช {๐ฆ}) โ (๐ฅ โ ๐ด โฆ โ๐ โ ๐ค ๐ถ) = (๐ฅ โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})๐ถ)) |
9 | 8 | eleq1d 2823 |
. 2
โข (๐ค = (๐ง โช {๐ฆ}) โ ((๐ฅ โ ๐ด โฆ โ๐ โ ๐ค ๐ถ) โ (๐ดโcnโโ) โ (๐ฅ โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})๐ถ) โ (๐ดโcnโโ))) |
10 | | prodeq1 15799 |
. . . 4
โข (๐ค = ๐ต โ โ๐ โ ๐ค ๐ถ = โ๐ โ ๐ต ๐ถ) |
11 | 10 | mpteq2dv 5212 |
. . 3
โข (๐ค = ๐ต โ (๐ฅ โ ๐ด โฆ โ๐ โ ๐ค ๐ถ) = (๐ฅ โ ๐ด โฆ โ๐ โ ๐ต ๐ถ)) |
12 | 11 | eleq1d 2823 |
. 2
โข (๐ค = ๐ต โ ((๐ฅ โ ๐ด โฆ โ๐ โ ๐ค ๐ถ) โ (๐ดโcnโโ) โ (๐ฅ โ ๐ด โฆ โ๐ โ ๐ต ๐ถ) โ (๐ดโcnโโ))) |
13 | | prod0 15833 |
. . . . 5
โข
โ๐ โ
โ
๐ถ =
1 |
14 | 13 | a1i 11 |
. . . 4
โข (๐ โ โ๐ โ โ
๐ถ = 1) |
15 | 14 | mpteq2dv 5212 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ โ๐ โ โ
๐ถ) = (๐ฅ โ ๐ด โฆ 1)) |
16 | | fprodcncf.a |
. . . 4
โข (๐ โ ๐ด โ โ) |
17 | | 1cnd 11157 |
. . . 4
โข (๐ โ 1 โ
โ) |
18 | | ssidd 3972 |
. . . 4
โข (๐ โ โ โ
โ) |
19 | 16, 17, 18 | constcncfg 44187 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ 1) โ (๐ดโcnโโ)) |
20 | 15, 19 | eqeltrd 2838 |
. 2
โข (๐ โ (๐ฅ โ ๐ด โฆ โ๐ โ โ
๐ถ) โ (๐ดโcnโโ)) |
21 | | nfcv 2908 |
. . . . . 6
โข
โฒ๐ขโ๐ โ (๐ง โช {๐ฆ})๐ถ |
22 | | nfcv 2908 |
. . . . . . 7
โข
โฒ๐ฅ(๐ง โช {๐ฆ}) |
23 | | nfcsb1v 3885 |
. . . . . . 7
โข
โฒ๐ฅโฆ๐ข / ๐ฅโฆ๐ถ |
24 | 22, 23 | nfcprod 15801 |
. . . . . 6
โข
โฒ๐ฅโ๐ โ (๐ง โช {๐ฆ})โฆ๐ข / ๐ฅโฆ๐ถ |
25 | | csbeq1a 3874 |
. . . . . . . 8
โข (๐ฅ = ๐ข โ ๐ถ = โฆ๐ข / ๐ฅโฆ๐ถ) |
26 | 25 | adantr 482 |
. . . . . . 7
โข ((๐ฅ = ๐ข โง ๐ โ (๐ง โช {๐ฆ})) โ ๐ถ = โฆ๐ข / ๐ฅโฆ๐ถ) |
27 | 26 | prodeq2dv 15813 |
. . . . . 6
โข (๐ฅ = ๐ข โ โ๐ โ (๐ง โช {๐ฆ})๐ถ = โ๐ โ (๐ง โช {๐ฆ})โฆ๐ข / ๐ฅโฆ๐ถ) |
28 | 21, 24, 27 | cbvmpt 5221 |
. . . . 5
โข (๐ฅ โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})๐ถ) = (๐ข โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})โฆ๐ข / ๐ฅโฆ๐ถ) |
29 | 28 | a1i 11 |
. . . 4
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ)) โ (๐ฅ โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})๐ถ) = (๐ข โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})โฆ๐ข / ๐ฅโฆ๐ถ)) |
30 | | nfv 1918 |
. . . . . . . 8
โข
โฒ๐((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) |
31 | | nfcsb1v 3885 |
. . . . . . . 8
โข
โฒ๐โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ |
32 | | fprodcncf.b |
. . . . . . . . . . . 12
โข (๐ โ ๐ต โ Fin) |
33 | 32 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ ๐ต) โ ๐ต โ Fin) |
34 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โง ๐ง โ ๐ต) โ ๐ง โ ๐ต) |
35 | | ssfi 9124 |
. . . . . . . . . . 11
โข ((๐ต โ Fin โง ๐ง โ ๐ต) โ ๐ง โ Fin) |
36 | 33, 34, 35 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โง ๐ง โ ๐ต) โ ๐ง โ Fin) |
37 | 36 | adantrr 716 |
. . . . . . . . 9
โข ((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โ ๐ง โ Fin) |
38 | 37 | adantr 482 |
. . . . . . . 8
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โ ๐ง โ Fin) |
39 | | vex 3452 |
. . . . . . . . 9
โข ๐ฆ โ V |
40 | 39 | a1i 11 |
. . . . . . . 8
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โ ๐ฆ โ V) |
41 | | eldifn 4092 |
. . . . . . . . . 10
โข (๐ฆ โ (๐ต โ ๐ง) โ ยฌ ๐ฆ โ ๐ง) |
42 | 41 | ad2antll 728 |
. . . . . . . . 9
โข ((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โ ยฌ ๐ฆ โ ๐ง) |
43 | 42 | adantr 482 |
. . . . . . . 8
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โ ยฌ ๐ฆ โ ๐ง) |
44 | | simplll 774 |
. . . . . . . . 9
โข ((((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โง ๐ โ ๐ง) โ ๐) |
45 | | simplr 768 |
. . . . . . . . 9
โข ((((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โง ๐ โ ๐ง) โ ๐ข โ ๐ด) |
46 | 34 | adantrr 716 |
. . . . . . . . . . 11
โข ((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โ ๐ง โ ๐ต) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โง ๐ โ ๐ง) โ ๐ง โ ๐ต) |
48 | | simpr 486 |
. . . . . . . . . 10
โข ((((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โง ๐ โ ๐ง) โ ๐ โ ๐ง) |
49 | 47, 48 | sseldd 3950 |
. . . . . . . . 9
โข ((((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โง ๐ โ ๐ง) โ ๐ โ ๐ต) |
50 | | nfv 1918 |
. . . . . . . . . . 11
โข
โฒ๐ฅ(๐ โง ๐ข โ ๐ด โง ๐ โ ๐ต) |
51 | 23 | nfel1 2924 |
. . . . . . . . . . 11
โข
โฒ๐ฅโฆ๐ข / ๐ฅโฆ๐ถ โ โ |
52 | 50, 51 | nfim 1900 |
. . . . . . . . . 10
โข
โฒ๐ฅ((๐ โง ๐ข โ ๐ด โง ๐ โ ๐ต) โ โฆ๐ข / ๐ฅโฆ๐ถ โ โ) |
53 | | eleq1w 2821 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ข โ (๐ฅ โ ๐ด โ ๐ข โ ๐ด)) |
54 | 53 | 3anbi2d 1442 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ข โ ((๐ โง ๐ฅ โ ๐ด โง ๐ โ ๐ต) โ (๐ โง ๐ข โ ๐ด โง ๐ โ ๐ต))) |
55 | 25 | eleq1d 2823 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ข โ (๐ถ โ โ โ โฆ๐ข / ๐ฅโฆ๐ถ โ โ)) |
56 | 54, 55 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ฅ = ๐ข โ (((๐ โง ๐ฅ โ ๐ด โง ๐ โ ๐ต) โ ๐ถ โ โ) โ ((๐ โง ๐ข โ ๐ด โง ๐ โ ๐ต) โ โฆ๐ข / ๐ฅโฆ๐ถ โ โ))) |
57 | | fprodcncf.c |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด โง ๐ โ ๐ต) โ ๐ถ โ โ) |
58 | 52, 56, 57 | chvarfv 2234 |
. . . . . . . . 9
โข ((๐ โง ๐ข โ ๐ด โง ๐ โ ๐ต) โ โฆ๐ข / ๐ฅโฆ๐ถ โ โ) |
59 | 44, 45, 49, 58 | syl3anc 1372 |
. . . . . . . 8
โข ((((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โง ๐ โ ๐ง) โ โฆ๐ข / ๐ฅโฆ๐ถ โ โ) |
60 | | csbeq1a 3874 |
. . . . . . . 8
โข (๐ = ๐ฆ โ โฆ๐ข / ๐ฅโฆ๐ถ = โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) |
61 | | simpll 766 |
. . . . . . . . 9
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โ ๐) |
62 | | eldifi 4091 |
. . . . . . . . . . 11
โข (๐ฆ โ (๐ต โ ๐ง) โ ๐ฆ โ ๐ต) |
63 | 62 | ad2antll 728 |
. . . . . . . . . 10
โข ((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โ ๐ฆ โ ๐ต) |
64 | 63 | adantr 482 |
. . . . . . . . 9
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โ ๐ฆ โ ๐ต) |
65 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โ ๐ข โ ๐ด) |
66 | | simpll 766 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ข โ ๐ด) โ ๐) |
67 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ข โ ๐ด) โ ๐ข โ ๐ด) |
68 | | simplr 768 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ข โ ๐ด) โ ๐ฆ โ ๐ต) |
69 | | nfv 1918 |
. . . . . . . . . . . 12
โข
โฒ๐(๐ โง ๐ข โ ๐ด โง ๐ฆ โ ๐ต) |
70 | | nfcv 2908 |
. . . . . . . . . . . . 13
โข
โฒ๐โ |
71 | 31, 70 | nfel 2922 |
. . . . . . . . . . . 12
โข
โฒ๐โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ โ โ |
72 | 69, 71 | nfim 1900 |
. . . . . . . . . . 11
โข
โฒ๐((๐ โง ๐ข โ ๐ด โง ๐ฆ โ ๐ต) โ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ โ โ) |
73 | | eleq1w 2821 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฆ โ (๐ โ ๐ต โ ๐ฆ โ ๐ต)) |
74 | 73 | 3anbi3d 1443 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ ((๐ โง ๐ข โ ๐ด โง ๐ โ ๐ต) โ (๐ โง ๐ข โ ๐ด โง ๐ฆ โ ๐ต))) |
75 | 60 | eleq1d 2823 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (โฆ๐ข / ๐ฅโฆ๐ถ โ โ โ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ โ โ)) |
76 | 74, 75 | imbi12d 345 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ (((๐ โง ๐ข โ ๐ด โง ๐ โ ๐ต) โ โฆ๐ข / ๐ฅโฆ๐ถ โ โ) โ ((๐ โง ๐ข โ ๐ด โง ๐ฆ โ ๐ต) โ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ โ โ))) |
77 | 72, 76, 58 | chvarfv 2234 |
. . . . . . . . . 10
โข ((๐ โง ๐ข โ ๐ด โง ๐ฆ โ ๐ต) โ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ โ โ) |
78 | 66, 67, 68, 77 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ ๐ต) โง ๐ข โ ๐ด) โ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ โ โ) |
79 | 61, 64, 65, 78 | syl21anc 837 |
. . . . . . . 8
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ โ โ) |
80 | 30, 31, 38, 40, 43, 59, 60, 79 | fprodsplitsn 15879 |
. . . . . . 7
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง ๐ข โ ๐ด) โ โ๐ โ (๐ง โช {๐ฆ})โฆ๐ข / ๐ฅโฆ๐ถ = (โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ ยท โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ)) |
81 | 80 | mpteq2dva 5210 |
. . . . . 6
โข ((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โ (๐ข โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})โฆ๐ข / ๐ฅโฆ๐ถ) = (๐ข โ ๐ด โฆ (โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ ยท โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ))) |
82 | 81 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ)) โ (๐ข โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})โฆ๐ข / ๐ฅโฆ๐ถ) = (๐ข โ ๐ด โฆ (โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ ยท โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ))) |
83 | | nfcv 2908 |
. . . . . . . . . . 11
โข
โฒ๐ขโ๐ โ ๐ง ๐ถ |
84 | | nfcv 2908 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ๐ง |
85 | 84, 23 | nfcprod 15801 |
. . . . . . . . . . 11
โข
โฒ๐ฅโ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ |
86 | 25 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฅ = ๐ข โง ๐ โ ๐ง) โ ๐ถ = โฆ๐ข / ๐ฅโฆ๐ถ) |
87 | 86 | prodeq2dv 15813 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ข โ โ๐ โ ๐ง ๐ถ = โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ) |
88 | 83, 85, 87 | cbvmpt 5221 |
. . . . . . . . . 10
โข (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) = (๐ข โ ๐ด โฆ โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ) |
89 | 88 | eqcomi 2746 |
. . . . . . . . 9
โข (๐ข โ ๐ด โฆ โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ) = (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) |
90 | 89 | a1i 11 |
. . . . . . . 8
โข ((๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ) โ (๐ข โ ๐ด โฆ โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ) = (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ)) |
91 | | id 22 |
. . . . . . . 8
โข ((๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ) โ (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ)) |
92 | 90, 91 | eqeltrd 2838 |
. . . . . . 7
โข ((๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ) โ (๐ข โ ๐ด โฆ โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) |
93 | 92 | adantl 483 |
. . . . . 6
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ)) โ (๐ข โ ๐ด โฆ โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) |
94 | | nfv 1918 |
. . . . . . . . . 10
โข
โฒ๐(๐ โง ๐ฆ โ ๐ต) |
95 | | nfcv 2908 |
. . . . . . . . . . . 12
โข
โฒ๐๐ด |
96 | 95, 31 | nfmpt 5217 |
. . . . . . . . . . 11
โข
โฒ๐(๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) |
97 | | nfcv 2908 |
. . . . . . . . . . 11
โข
โฒ๐(๐ดโcnโโ) |
98 | 96, 97 | nfel 2922 |
. . . . . . . . . 10
โข
โฒ๐(๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ) |
99 | 94, 98 | nfim 1900 |
. . . . . . . . 9
โข
โฒ๐((๐ โง ๐ฆ โ ๐ต) โ (๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) |
100 | 73 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ ((๐ โง ๐ โ ๐ต) โ (๐ โง ๐ฆ โ ๐ต))) |
101 | 60 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ = ๐ฆ โง ๐ข โ ๐ด) โ โฆ๐ข / ๐ฅโฆ๐ถ = โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) |
102 | 101 | mpteq2dva 5210 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ (๐ข โ ๐ด โฆ โฆ๐ข / ๐ฅโฆ๐ถ) = (๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ)) |
103 | 102 | eleq1d 2823 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ ((๐ข โ ๐ด โฆ โฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ) โ (๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ))) |
104 | 100, 103 | imbi12d 345 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ (((๐ โง ๐ โ ๐ต) โ (๐ข โ ๐ด โฆ โฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) โ ((๐ โง ๐ฆ โ ๐ต) โ (๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)))) |
105 | | nfcv 2908 |
. . . . . . . . . . 11
โข
โฒ๐ข๐ถ |
106 | 105, 23, 25 | cbvmpt 5221 |
. . . . . . . . . 10
โข (๐ฅ โ ๐ด โฆ ๐ถ) = (๐ข โ ๐ด โฆ โฆ๐ข / ๐ฅโฆ๐ถ) |
107 | | fprodcncf.cn |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ (๐ฅ โ ๐ด โฆ ๐ถ) โ (๐ดโcnโโ)) |
108 | 106, 107 | eqeltrrid 2843 |
. . . . . . . . 9
โข ((๐ โง ๐ โ ๐ต) โ (๐ข โ ๐ด โฆ โฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) |
109 | 99, 104, 108 | chvarfv 2234 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ ๐ต) โ (๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) |
110 | 63, 109 | syldan 592 |
. . . . . . 7
โข ((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โ (๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) |
111 | 110 | adantr 482 |
. . . . . 6
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ)) โ (๐ข โ ๐ด โฆ โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) |
112 | 93, 111 | mulcncf 24826 |
. . . . 5
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ)) โ (๐ข โ ๐ด โฆ (โ๐ โ ๐ง โฆ๐ข / ๐ฅโฆ๐ถ ยท โฆ๐ฆ / ๐โฆโฆ๐ข / ๐ฅโฆ๐ถ)) โ (๐ดโcnโโ)) |
113 | 82, 112 | eqeltrd 2838 |
. . . 4
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ)) โ (๐ข โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})โฆ๐ข / ๐ฅโฆ๐ถ) โ (๐ดโcnโโ)) |
114 | 29, 113 | eqeltrd 2838 |
. . 3
โข (((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โง (๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ)) โ (๐ฅ โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})๐ถ) โ (๐ดโcnโโ)) |
115 | 114 | ex 414 |
. 2
โข ((๐ โง (๐ง โ ๐ต โง ๐ฆ โ (๐ต โ ๐ง))) โ ((๐ฅ โ ๐ด โฆ โ๐ โ ๐ง ๐ถ) โ (๐ดโcnโโ) โ (๐ฅ โ ๐ด โฆ โ๐ โ (๐ง โช {๐ฆ})๐ถ) โ (๐ดโcnโโ))) |
116 | 3, 6, 9, 12, 20, 115, 32 | findcard2d 9117 |
1
โข (๐ โ (๐ฅ โ ๐ด โฆ โ๐ โ ๐ต ๐ถ) โ (๐ดโcnโโ)) |