Step | Hyp | Ref
| Expression |
1 | | cnre 7952 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |
2 | 1 | adantr 276 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |
3 | | cnre 7952 |
. . . . . . 7
โข (๐ต โ โ โ
โ๐ง โ โ
โ๐ค โ โ
๐ต = (๐ง + (i ยท ๐ค))) |
4 | 3 | adantl 277 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
โ๐ง โ โ
โ๐ค โ โ
๐ต = (๐ง + (i ยท ๐ค))) |
5 | 4 | ad2antrr 488 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ โ๐ง โ โ โ๐ค โ โ ๐ต = (๐ง + (i ยท ๐ค))) |
6 | | simpr 110 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ โ โ โง ๐ฆ โ
โ)) |
7 | 6 | ad3antrrr 492 |
. . . . . . . . 9
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (๐ฅ โ โ โง ๐ฆ โ โ)) |
8 | | simplr 528 |
. . . . . . . . 9
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (๐ง โ โ โง ๐ค โ โ)) |
9 | | cru 8558 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ง โ โ โง ๐ค โ โ)) โ ((๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
10 | 7, 8, 9 | syl2anc 411 |
. . . . . . . 8
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ ((๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค)) โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
11 | | simpllr 534 |
. . . . . . . . 9
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) |
12 | | simpr 110 |
. . . . . . . . 9
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ ๐ต = (๐ง + (i ยท ๐ค))) |
13 | 11, 12 | eqeq12d 2192 |
. . . . . . . 8
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (๐ด = ๐ต โ (๐ฅ + (i ยท ๐ฆ)) = (๐ง + (i ยท ๐ค)))) |
14 | | apreim 8559 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ง โ โ โง ๐ค โ โ)) โ ((๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)) โ (๐ฅ # ๐ง โจ ๐ฆ # ๐ค))) |
15 | 14 | notbid 667 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ง โ โ โง ๐ค โ โ)) โ (ยฌ
(๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)) โ ยฌ (๐ฅ # ๐ง โจ ๐ฆ # ๐ค))) |
16 | | ioran 752 |
. . . . . . . . . . 11
โข (ยฌ
(๐ฅ # ๐ง โจ ๐ฆ # ๐ค) โ (ยฌ ๐ฅ # ๐ง โง ยฌ ๐ฆ # ๐ค)) |
17 | 15, 16 | bitrdi 196 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ง โ โ โง ๐ค โ โ)) โ (ยฌ
(๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)) โ (ยฌ ๐ฅ # ๐ง โง ยฌ ๐ฆ # ๐ค))) |
18 | 7, 8, 17 | syl2anc 411 |
. . . . . . . . 9
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (ยฌ (๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)) โ (ยฌ ๐ฅ # ๐ง โง ยฌ ๐ฆ # ๐ค))) |
19 | 11, 12 | breq12d 4016 |
. . . . . . . . . 10
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (๐ด # ๐ต โ (๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)))) |
20 | 19 | notbid 667 |
. . . . . . . . 9
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (ยฌ ๐ด # ๐ต โ ยฌ (๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)))) |
21 | 7 | simpld 112 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ ๐ฅ โ โ) |
22 | 8 | simpld 112 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ ๐ง โ โ) |
23 | | reapti 8535 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ง โ โ) โ (๐ฅ = ๐ง โ ยฌ ๐ฅ #โ ๐ง)) |
24 | | apreap 8543 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ง โ โ) โ (๐ฅ # ๐ง โ ๐ฅ #โ ๐ง)) |
25 | 24 | notbid 667 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ง โ โ) โ (ยฌ
๐ฅ # ๐ง โ ยฌ ๐ฅ #โ ๐ง)) |
26 | 23, 25 | bitr4d 191 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ง โ โ) โ (๐ฅ = ๐ง โ ยฌ ๐ฅ # ๐ง)) |
27 | 21, 22, 26 | syl2anc 411 |
. . . . . . . . . 10
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (๐ฅ = ๐ง โ ยฌ ๐ฅ # ๐ง)) |
28 | 7 | simprd 114 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ ๐ฆ โ โ) |
29 | 8 | simprd 114 |
. . . . . . . . . . 11
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ ๐ค โ โ) |
30 | | reapti 8535 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง ๐ค โ โ) โ (๐ฆ = ๐ค โ ยฌ ๐ฆ #โ ๐ค)) |
31 | | apreap 8543 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ โง ๐ค โ โ) โ (๐ฆ # ๐ค โ ๐ฆ #โ ๐ค)) |
32 | 31 | notbid 667 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง ๐ค โ โ) โ (ยฌ
๐ฆ # ๐ค โ ยฌ ๐ฆ #โ ๐ค)) |
33 | 30, 32 | bitr4d 191 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ค โ โ) โ (๐ฆ = ๐ค โ ยฌ ๐ฆ # ๐ค)) |
34 | 28, 29, 33 | syl2anc 411 |
. . . . . . . . . 10
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (๐ฆ = ๐ค โ ยฌ ๐ฆ # ๐ค)) |
35 | 27, 34 | anbi12d 473 |
. . . . . . . . 9
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ ((๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ (ยฌ ๐ฅ # ๐ง โง ยฌ ๐ฆ # ๐ค))) |
36 | 18, 20, 35 | 3bitr4d 220 |
. . . . . . . 8
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (ยฌ ๐ด # ๐ต โ (๐ฅ = ๐ง โง ๐ฆ = ๐ค))) |
37 | 10, 13, 36 | 3bitr4d 220 |
. . . . . . 7
โข
((((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (๐ด = ๐ต โ ยฌ ๐ด # ๐ต)) |
38 | 37 | ex 115 |
. . . . . 6
โข
(((((๐ด โ
โ โง ๐ต โ
โ) โง (๐ฅ โ
โ โง ๐ฆ โ
โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โง (๐ง โ โ โง ๐ค โ โ)) โ (๐ต = (๐ง + (i ยท ๐ค)) โ (๐ด = ๐ต โ ยฌ ๐ด # ๐ต))) |
39 | 38 | rexlimdvva 2602 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (โ๐ง โ โ โ๐ค โ โ ๐ต = (๐ง + (i ยท ๐ค)) โ (๐ด = ๐ต โ ยฌ ๐ด # ๐ต))) |
40 | 5, 39 | mpd 13 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด = ๐ต โ ยฌ ๐ด # ๐ต)) |
41 | 40 | ex 115 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ด = ๐ต โ ยฌ ๐ด # ๐ต))) |
42 | 41 | rexlimdvva 2602 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ด = ๐ต โ ยฌ ๐ด # ๐ต))) |
43 | 2, 42 | mpd 13 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด = ๐ต โ ยฌ ๐ด # ๐ต)) |