Step | Hyp | Ref
| Expression |
1 | | ralunb 4152 |
. . . . . . 7
โข
(โ๐ฆ โ
(๐ โช ๐)(๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ) โ (โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ) โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ))) |
2 | 1 | a1i 11 |
. . . . . 6
โข (((๐ โ ๐ต โง ๐ โ ๐ต) โง ๐ฅ โ ๐ต) โ (โ๐ฆ โ (๐ โช ๐)(๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ) โ (โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ) โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)))) |
3 | 2 | pm5.32da 580 |
. . . . 5
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ฅ โ ๐ต โง โ๐ฆ โ (๐ โช ๐)(๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)) โ (๐ฅ โ ๐ต โง (โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ) โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ))))) |
4 | | anandi 675 |
. . . . 5
โข ((๐ฅ โ ๐ต โง (โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ) โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ))) โ ((๐ฅ โ ๐ต โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)) โง (๐ฅ โ ๐ต โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)))) |
5 | 3, 4 | bitrdi 287 |
. . . 4
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ฅ โ ๐ต โง โ๐ฆ โ (๐ โช ๐)(๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)) โ ((๐ฅ โ ๐ต โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)) โง (๐ฅ โ ๐ต โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ))))) |
6 | | unss 4145 |
. . . . 5
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โช ๐) โ ๐ต) |
7 | | cntzun.b |
. . . . . 6
โข ๐ต = (Baseโ๐) |
8 | | eqid 2733 |
. . . . . 6
โข
(+gโ๐) = (+gโ๐) |
9 | | cntzun.z |
. . . . . 6
โข ๐ = (Cntzโ๐) |
10 | 7, 8, 9 | elcntz 19107 |
. . . . 5
โข ((๐ โช ๐) โ ๐ต โ (๐ฅ โ (๐โ(๐ โช ๐)) โ (๐ฅ โ ๐ต โง โ๐ฆ โ (๐ โช ๐)(๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)))) |
11 | 6, 10 | sylbi 216 |
. . . 4
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ฅ โ (๐โ(๐ โช ๐)) โ (๐ฅ โ ๐ต โง โ๐ฆ โ (๐ โช ๐)(๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)))) |
12 | 7, 8, 9 | elcntz 19107 |
. . . . 5
โข (๐ โ ๐ต โ (๐ฅ โ (๐โ๐) โ (๐ฅ โ ๐ต โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)))) |
13 | 7, 8, 9 | elcntz 19107 |
. . . . 5
โข (๐ โ ๐ต โ (๐ฅ โ (๐โ๐) โ (๐ฅ โ ๐ต โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)))) |
14 | 12, 13 | bi2anan9 638 |
. . . 4
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ฅ โ (๐โ๐) โง ๐ฅ โ (๐โ๐)) โ ((๐ฅ โ ๐ต โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)) โง (๐ฅ โ ๐ต โง โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ))))) |
15 | 5, 11, 14 | 3bitr4d 311 |
. . 3
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ฅ โ (๐โ(๐ โช ๐)) โ (๐ฅ โ (๐โ๐) โง ๐ฅ โ (๐โ๐)))) |
16 | | elin 3927 |
. . 3
โข (๐ฅ โ ((๐โ๐) โฉ (๐โ๐)) โ (๐ฅ โ (๐โ๐) โง ๐ฅ โ (๐โ๐))) |
17 | 15, 16 | bitr4di 289 |
. 2
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ฅ โ (๐โ(๐ โช ๐)) โ ๐ฅ โ ((๐โ๐) โฉ (๐โ๐)))) |
18 | 17 | eqrdv 2731 |
1
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐โ(๐ โช ๐)) = ((๐โ๐) โฉ (๐โ๐))) |