Step | Hyp | Ref
| Expression |
1 | | signsw.p |
. . . . . 6
⒠⨣ =
(π β {-1, 0, 1}, π β {-1, 0, 1} β¦
if(π = 0, π, π)) |
2 | 1 | signspval 33632 |
. . . . 5
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1}) β
(π’ ⨣ π£) = if(π£ = 0, π’, π£)) |
3 | | ifcl 4573 |
. . . . 5
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1}) β
if(π£ = 0, π’, π£) β {-1, 0, 1}) |
4 | 2, 3 | eqeltrd 2833 |
. . . 4
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1}) β
(π’ ⨣ π£) β {-1, 0, 1}) |
5 | 1 | signspval 33632 |
. . . . . . . . . . . . 13
β’ (((π’ ⨣ π£) β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β ((π’ ⨣ π£) ⨣ π€) = if(π€ = 0, (π’ ⨣ π£), π€)) |
6 | 4, 5 | stoic3 1778 |
. . . . . . . . . . . 12
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β
((π’ ⨣ π£) ⨣ π€) = if(π€ = 0, (π’ ⨣ π£), π€)) |
7 | | iftrue 4534 |
. . . . . . . . . . . 12
β’ (π€ = 0 β if(π€ = 0, (π’ ⨣ π£), π€) = (π’ ⨣ π£)) |
8 | 6, 7 | sylan9eq 2792 |
. . . . . . . . . . 11
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β ((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ π£)) |
9 | 8 | adantr 481 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β ((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ π£)) |
10 | 2 | 3adant3 1132 |
. . . . . . . . . . 11
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β
(π’ ⨣ π£) = if(π£ = 0, π’, π£)) |
11 | 10 | ad2antrr 724 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β (π’ ⨣ π£) = if(π£ = 0, π’, π£)) |
12 | | iftrue 4534 |
. . . . . . . . . . 11
β’ (π£ = 0 β if(π£ = 0, π’, π£) = π’) |
13 | 12 | adantl 482 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β if(π£ = 0, π’, π£) = π’) |
14 | 9, 11, 13 | 3eqtrd 2776 |
. . . . . . . . 9
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β ((π’ ⨣ π£) ⨣ π€) = π’) |
15 | | simp1 1136 |
. . . . . . . . . . . 12
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β π’ β {-1, 0,
1}) |
16 | 1 | signspval 33632 |
. . . . . . . . . . . . . 14
β’ ((π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β
(π£ ⨣ π€) = if(π€ = 0, π£, π€)) |
17 | 16 | 3adant1 1130 |
. . . . . . . . . . . . 13
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β
(π£ ⨣ π€) = if(π€ = 0, π£, π€)) |
18 | | simpl2 1192 |
. . . . . . . . . . . . . 14
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β π£ β {-1, 0, 1}) |
19 | | simpl3 1193 |
. . . . . . . . . . . . . 14
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β π€ β {-1, 0,
1}) |
20 | 18, 19 | ifclda 4563 |
. . . . . . . . . . . . 13
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β
if(π€ = 0, π£, π€) β {-1, 0, 1}) |
21 | 17, 20 | eqeltrd 2833 |
. . . . . . . . . . . 12
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β
(π£ ⨣ π€) β {-1, 0, 1}) |
22 | 1 | signspval 33632 |
. . . . . . . . . . . 12
β’ ((π’ β {-1, 0, 1} β§ (π£ ⨣ π€) β {-1, 0, 1}) β (π’ ⨣ (π£ ⨣ π€)) = if((π£ ⨣ π€) = 0, π’, (π£ ⨣ π€))) |
23 | 15, 21, 22 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β
(π’ ⨣ (π£ ⨣ π€)) = if((π£ ⨣ π€) = 0, π’, (π£ ⨣ π€))) |
24 | 23 | ad2antrr 724 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β (π’ ⨣ (π£ ⨣ π€)) = if((π£ ⨣ π€) = 0, π’, (π£ ⨣ π€))) |
25 | | iftrue 4534 |
. . . . . . . . . . . . 13
β’ (π€ = 0 β if(π€ = 0, π£, π€) = π£) |
26 | 17, 25 | sylan9eq 2792 |
. . . . . . . . . . . 12
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β (π£ ⨣ π€) = π£) |
27 | | id 22 |
. . . . . . . . . . . 12
β’ (π£ = 0 β π£ = 0) |
28 | 26, 27 | sylan9eq 2792 |
. . . . . . . . . . 11
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β (π£ ⨣ π€) = 0) |
29 | 28 | iftrued 4536 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β if((π£ ⨣ π€) = 0, π’, (π£ ⨣ π€)) = π’) |
30 | 24, 29 | eqtrd 2772 |
. . . . . . . . 9
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β (π’ ⨣ (π£ ⨣ π€)) = π’) |
31 | 14, 30 | eqtr4d 2775 |
. . . . . . . 8
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ π£ = 0) β ((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) |
32 | 6 | ad2antrr 724 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β ((π’ ⨣ π£) ⨣ π€) = if(π€ = 0, (π’ ⨣ π£), π€)) |
33 | 7 | ad2antlr 725 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β if(π€ = 0, (π’ ⨣ π£), π€) = (π’ ⨣ π£)) |
34 | 10 | ad2antrr 724 |
. . . . . . . . . . 11
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β (π’ ⨣ π£) = if(π£ = 0, π’, π£)) |
35 | | iffalse 4537 |
. . . . . . . . . . . 12
β’ (Β¬
π£ = 0 β if(π£ = 0, π’, π£) = π£) |
36 | 35 | adantl 482 |
. . . . . . . . . . 11
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β if(π£ = 0, π’, π£) = π£) |
37 | 34, 36 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β (π’ ⨣ π£) = π£) |
38 | 32, 33, 37 | 3eqtrd 2776 |
. . . . . . . . 9
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β ((π’ ⨣ π£) ⨣ π€) = π£) |
39 | 23 | ad2antrr 724 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β (π’ ⨣ (π£ ⨣ π€)) = if((π£ ⨣ π€) = 0, π’, (π£ ⨣ π€))) |
40 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β Β¬ π£ = 0) |
41 | 17 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β (π£ ⨣ π€) = if(π€ = 0, π£, π€)) |
42 | 25 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β if(π€ = 0, π£, π€) = π£) |
43 | 41, 42 | eqtrd 2772 |
. . . . . . . . . . . . 13
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β (π£ ⨣ π€) = π£) |
44 | 43 | eqeq1d 2734 |
. . . . . . . . . . . 12
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β ((π£ ⨣ π€) = 0 β π£ = 0)) |
45 | 40, 44 | mtbird 324 |
. . . . . . . . . . 11
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β Β¬ (π£ ⨣ π€) = 0) |
46 | 45 | iffalsed 4539 |
. . . . . . . . . 10
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β if((π£ ⨣ π€) = 0, π’, (π£ ⨣ π€)) = (π£ ⨣ π€)) |
47 | 39, 46, 43 | 3eqtrd 2776 |
. . . . . . . . 9
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β (π’ ⨣ (π£ ⨣ π€)) = π£) |
48 | 38, 47 | eqtr4d 2775 |
. . . . . . . 8
β’ ((((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β§ Β¬ π£ = 0) β ((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) |
49 | 31, 48 | pm2.61dan 811 |
. . . . . . 7
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ π€ = 0) β ((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) |
50 | | iffalse 4537 |
. . . . . . . . 9
β’ (Β¬
π€ = 0 β if(π€ = 0, (π’ ⨣ π£), π€) = π€) |
51 | 6, 50 | sylan9eq 2792 |
. . . . . . . 8
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β ((π’ ⨣ π£) ⨣ π€) = π€) |
52 | 23 | adantr 481 |
. . . . . . . . 9
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β (π’ ⨣ (π£ ⨣ π€)) = if((π£ ⨣ π€) = 0, π’, (π£ ⨣ π€))) |
53 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β Β¬ π€ = 0) |
54 | | iffalse 4537 |
. . . . . . . . . . . . 13
β’ (Β¬
π€ = 0 β if(π€ = 0, π£, π€) = π€) |
55 | 17, 54 | sylan9eq 2792 |
. . . . . . . . . . . 12
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β (π£ ⨣ π€) = π€) |
56 | 55 | eqeq1d 2734 |
. . . . . . . . . . 11
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β ((π£ ⨣ π€) = 0 β π€ = 0)) |
57 | 53, 56 | mtbird 324 |
. . . . . . . . . 10
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β Β¬ (π£ ⨣ π€) = 0) |
58 | 57 | iffalsed 4539 |
. . . . . . . . 9
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β if((π£ ⨣ π€) = 0, π’, (π£ ⨣ π€)) = (π£ ⨣ π€)) |
59 | 52, 58, 55 | 3eqtrd 2776 |
. . . . . . . 8
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β (π’ ⨣ (π£ ⨣ π€)) = π€) |
60 | 51, 59 | eqtr4d 2775 |
. . . . . . 7
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β§ Β¬
π€ = 0) β ((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) |
61 | 49, 60 | pm2.61dan 811 |
. . . . . 6
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1} β§ π€ β {-1, 0, 1}) β
((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) |
62 | 61 | 3expa 1118 |
. . . . 5
β’ (((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1}) β§ π€ β {-1, 0, 1}) β
((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) |
63 | 62 | ralrimiva 3146 |
. . . 4
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1}) β
βπ€ β {-1, 0, 1}
((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) |
64 | 4, 63 | jca 512 |
. . 3
β’ ((π’ β {-1, 0, 1} β§ π£ β {-1, 0, 1}) β
((π’ ⨣ π£) β {-1, 0, 1} β§ βπ€ β {-1, 0, 1} ((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€)))) |
65 | 64 | rgen2 3197 |
. 2
β’
βπ’ β
{-1, 0, 1}βπ£ β
{-1, 0, 1} ((π’ ⨣ π£) β {-1, 0, 1} β§
βπ€ β {-1, 0, 1}
((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) |
66 | | c0ex 11210 |
. . . 4
β’ 0 β
V |
67 | 66 | tpid2 4774 |
. . 3
β’ 0 β
{-1, 0, 1} |
68 | 1 | signsw0glem 33633 |
. . 3
β’
βπ’ β
{-1, 0, 1} ((0 ⨣ π’) = π’ β§ (π’ ⨣ 0) = π’) |
69 | | oveq1 7418 |
. . . . . 6
β’ (π = 0 β (π ⨣ π’) = (0 ⨣ π’)) |
70 | 69 | eqeq1d 2734 |
. . . . 5
β’ (π = 0 β ((π ⨣ π’) = π’ β (0 ⨣ π’) = π’)) |
71 | 70 | ovanraleqv 7435 |
. . . 4
β’ (π = 0 β (βπ’ β {-1, 0, 1} ((π ⨣ π’) = π’ β§ (π’ ⨣ π) = π’) β βπ’ β {-1, 0, 1} ((0 ⨣ π’) = π’ β§ (π’ ⨣ 0) = π’))) |
72 | 71 | rspcev 3612 |
. . 3
β’ ((0
β {-1, 0, 1} β§ βπ’ β {-1, 0, 1} ((0 ⨣ π’) = π’ β§ (π’ ⨣ 0) = π’)) β βπ β {-1, 0, 1}βπ’ β {-1, 0, 1} ((π ⨣ π’) = π’ β§ (π’ ⨣ π) = π’)) |
73 | 67, 68, 72 | mp2an 690 |
. 2
β’
βπ β {-1,
0, 1}βπ’ β {-1,
0, 1} ((π ⨣ π’) = π’ β§ (π’ ⨣ π) = π’) |
74 | | signsw.w |
. . . 4
β’ π = {β¨(Baseβndx), {-1,
0, 1}β©, β¨(+gβndx), ⨣
β©} |
75 | 1, 74 | signswbase 33634 |
. . 3
β’ {-1, 0,
1} = (Baseβπ) |
76 | 1, 74 | signswplusg 33635 |
. . 3
⒠⨣ =
(+gβπ) |
77 | 75, 76 | ismnd 18630 |
. 2
β’ (π β Mnd β
(βπ’ β {-1, 0,
1}βπ£ β {-1, 0,
1} ((π’ ⨣ π£) β {-1, 0, 1} β§ βπ€ β {-1, 0, 1} ((π’ ⨣ π£) ⨣ π€) = (π’ ⨣ (π£ ⨣ π€))) β§ βπ β {-1, 0, 1}βπ’ β {-1, 0, 1} ((π ⨣ π’) = π’ β§ (π’ ⨣ π) = π’))) |
78 | 65, 73, 77 | mpbir2an 709 |
1
β’ π β Mnd |