Step | Hyp | Ref
| Expression |
1 | | simpr3 1197 |
. 2
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ ๐น โ ๐บ) |
2 | | simpl3 1194 |
. 2
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) |
3 | | neeq2 3004 |
. . . . 5
โข (๐ง = ๐บ โ (๐น โ ๐ง โ ๐น โ ๐บ)) |
4 | | oveq1 7368 |
. . . . . . 7
โข (๐ง = ๐บ โ (๐ง๐ธ๐ค) = (๐บ๐ธ๐ค)) |
5 | 4 | eqeq2d 2744 |
. . . . . 6
โข (๐ง = ๐บ โ ((๐น๐ธ๐ค) = (๐ง๐ธ๐ค) โ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค))) |
6 | 5 | ralbidv 3171 |
. . . . 5
โข (๐ง = ๐บ โ (โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค) โ โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค))) |
7 | 3, 6 | anbi12d 632 |
. . . 4
โข (๐ง = ๐บ โ ((๐น โ ๐ง โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐น โ ๐บ โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)))) |
8 | 7 | imbi1d 342 |
. . 3
โข (๐ง = ๐บ โ (((๐น โ ๐ง โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 ) โ ((๐น โ ๐บ โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 ))) |
9 | | simpl2 1193 |
. . . 4
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ ๐ธ โ ๐ต) |
10 | | simpr1 1195 |
. . . 4
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ ๐น โ ๐) |
11 | | simpl1 1192 |
. . . . 5
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ ๐) |
12 | | mdetuni.al |
. . . . 5
โข (๐ โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) |
13 | 11, 12 | syl 17 |
. . . 4
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) |
14 | | oveq 7367 |
. . . . . . . . . 10
โข (๐ฅ = ๐ธ โ (๐ฆ๐ฅ๐ค) = (๐ฆ๐ธ๐ค)) |
15 | | oveq 7367 |
. . . . . . . . . 10
โข (๐ฅ = ๐ธ โ (๐ง๐ฅ๐ค) = (๐ง๐ธ๐ค)) |
16 | 14, 15 | eqeq12d 2749 |
. . . . . . . . 9
โข (๐ฅ = ๐ธ โ ((๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค) โ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค))) |
17 | 16 | ralbidv 3171 |
. . . . . . . 8
โข (๐ฅ = ๐ธ โ (โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค) โ โ๐ค โ ๐ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค))) |
18 | 17 | anbi2d 630 |
. . . . . . 7
โข (๐ฅ = ๐ธ โ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค)))) |
19 | | fveqeq2 6855 |
. . . . . . 7
โข (๐ฅ = ๐ธ โ ((๐ทโ๐ฅ) = 0 โ (๐ทโ๐ธ) = 0 )) |
20 | 18, 19 | imbi12d 345 |
. . . . . 6
โข (๐ฅ = ๐ธ โ (((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 ) โ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 ))) |
21 | 20 | ralbidv 3171 |
. . . . 5
โข (๐ฅ = ๐ธ โ (โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 ) โ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 ))) |
22 | | neeq1 3003 |
. . . . . . . 8
โข (๐ฆ = ๐น โ (๐ฆ โ ๐ง โ ๐น โ ๐ง)) |
23 | | oveq1 7368 |
. . . . . . . . . 10
โข (๐ฆ = ๐น โ (๐ฆ๐ธ๐ค) = (๐น๐ธ๐ค)) |
24 | 23 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐ฆ = ๐น โ ((๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค) โ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค))) |
25 | 24 | ralbidv 3171 |
. . . . . . . 8
โข (๐ฆ = ๐น โ (โ๐ค โ ๐ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค) โ โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค))) |
26 | 22, 25 | anbi12d 632 |
. . . . . . 7
โข (๐ฆ = ๐น โ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐น โ ๐ง โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค)))) |
27 | 26 | imbi1d 342 |
. . . . . 6
โข (๐ฆ = ๐น โ (((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 ) โ ((๐น โ ๐ง โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 ))) |
28 | 27 | ralbidv 3171 |
. . . . 5
โข (๐ฆ = ๐น โ (โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 ) โ โ๐ง โ ๐ ((๐น โ ๐ง โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 ))) |
29 | 21, 28 | rspc2va 3593 |
. . . 4
โข (((๐ธ โ ๐ต โง ๐น โ ๐) โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฆ โ ๐ง โง โ๐ค โ ๐ (๐ฆ๐ฅ๐ค) = (๐ง๐ฅ๐ค)) โ (๐ทโ๐ฅ) = 0 )) โ โ๐ง โ ๐ ((๐น โ ๐ง โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 )) |
30 | 9, 10, 13, 29 | syl21anc 837 |
. . 3
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ โ๐ง โ ๐ ((๐น โ ๐ง โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐ง๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 )) |
31 | | simpr2 1196 |
. . 3
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ ๐บ โ ๐) |
32 | 8, 30, 31 | rspcdva 3584 |
. 2
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ ((๐น โ ๐บ โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โ (๐ทโ๐ธ) = 0 )) |
33 | 1, 2, 32 | mp2and 698 |
1
โข (((๐ โง ๐ธ โ ๐ต โง โ๐ค โ ๐ (๐น๐ธ๐ค) = (๐บ๐ธ๐ค)) โง (๐น โ ๐ โง ๐บ โ ๐ โง ๐น โ ๐บ)) โ (๐ทโ๐ธ) = 0 ) |