Step | Hyp | Ref
| Expression |
1 | | xp1st 7958 |
. . . . 5
โข (๐ด โ (N ร
N) โ (1st โ๐ด) โ N) |
2 | 1 | 3ad2ant1 1134 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (1st โ๐ด) โ N) |
3 | | xp1st 7958 |
. . . . 5
โข (๐ถ โ (N ร
N) โ (1st โ๐ถ) โ N) |
4 | 3 | 3ad2ant3 1136 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (1st โ๐ถ) โ N) |
5 | | mulclpi 10836 |
. . . 4
โข
(((1st โ๐ด) โ N โง
(1st โ๐ถ)
โ N) โ ((1st โ๐ด) ยทN
(1st โ๐ถ))
โ N) |
6 | 2, 4, 5 | syl2anc 585 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((1st โ๐ด) ยทN
(1st โ๐ถ))
โ N) |
7 | | xp2nd 7959 |
. . . . 5
โข (๐ด โ (N ร
N) โ (2nd โ๐ด) โ N) |
8 | 7 | 3ad2ant1 1134 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (2nd โ๐ด) โ N) |
9 | | xp2nd 7959 |
. . . . 5
โข (๐ถ โ (N ร
N) โ (2nd โ๐ถ) โ N) |
10 | 9 | 3ad2ant3 1136 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (2nd โ๐ถ) โ N) |
11 | | mulclpi 10836 |
. . . 4
โข
(((2nd โ๐ด) โ N โง
(2nd โ๐ถ)
โ N) โ ((2nd โ๐ด) ยทN
(2nd โ๐ถ))
โ N) |
12 | 8, 10, 11 | syl2anc 585 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((2nd โ๐ด) ยทN
(2nd โ๐ถ))
โ N) |
13 | | xp1st 7958 |
. . . . 5
โข (๐ต โ (N ร
N) โ (1st โ๐ต) โ N) |
14 | 13 | 3ad2ant2 1135 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (1st โ๐ต) โ N) |
15 | | mulclpi 10836 |
. . . 4
โข
(((1st โ๐ต) โ N โง
(1st โ๐ถ)
โ N) โ ((1st โ๐ต) ยทN
(1st โ๐ถ))
โ N) |
16 | 14, 4, 15 | syl2anc 585 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((1st โ๐ต) ยทN
(1st โ๐ถ))
โ N) |
17 | | xp2nd 7959 |
. . . . 5
โข (๐ต โ (N ร
N) โ (2nd โ๐ต) โ N) |
18 | 17 | 3ad2ant2 1135 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (2nd โ๐ต) โ N) |
19 | | mulclpi 10836 |
. . . 4
โข
(((2nd โ๐ต) โ N โง
(2nd โ๐ถ)
โ N) โ ((2nd โ๐ต) ยทN
(2nd โ๐ถ))
โ N) |
20 | 18, 10, 19 | syl2anc 585 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((2nd โ๐ต) ยทN
(2nd โ๐ถ))
โ N) |
21 | | enqbreq 10862 |
. . 3
โข
(((((1st โ๐ด) ยทN
(1st โ๐ถ))
โ N โง ((2nd โ๐ด) ยทN
(2nd โ๐ถ))
โ N) โง (((1st โ๐ต) ยทN
(1st โ๐ถ))
โ N โง ((2nd โ๐ต) ยทN
(2nd โ๐ถ))
โ N)) โ (โจ((1st โ๐ด)
ยทN (1st โ๐ถ)), ((2nd โ๐ด)
ยทN (2nd โ๐ถ))โฉ ~Q
โจ((1st โ๐ต) ยทN
(1st โ๐ถ)),
((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ โ (((1st
โ๐ด)
ยทN (1st โ๐ถ)) ยทN
((2nd โ๐ต)
ยทN (2nd โ๐ถ))) = (((2nd โ๐ด)
ยทN (2nd โ๐ถ)) ยทN
((1st โ๐ต)
ยทN (1st โ๐ถ))))) |
22 | 6, 12, 16, 20, 21 | syl22anc 838 |
. 2
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (โจ((1st โ๐ด) ยทN
(1st โ๐ถ)),
((2nd โ๐ด)
ยทN (2nd โ๐ถ))โฉ ~Q
โจ((1st โ๐ต) ยทN
(1st โ๐ถ)),
((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ โ (((1st
โ๐ด)
ยทN (1st โ๐ถ)) ยทN
((2nd โ๐ต)
ยทN (2nd โ๐ถ))) = (((2nd โ๐ด)
ยทN (2nd โ๐ถ)) ยทN
((1st โ๐ต)
ยทN (1st โ๐ถ))))) |
23 | | mulpipq2 10882 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ถ
โ (N ร N)) โ (๐ด ยทpQ ๐ถ) = โจ((1st
โ๐ด)
ยทN (1st โ๐ถ)), ((2nd โ๐ด)
ยทN (2nd โ๐ถ))โฉ) |
24 | 23 | 3adant2 1132 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (๐ด
ยทpQ ๐ถ) = โจ((1st โ๐ด)
ยทN (1st โ๐ถ)), ((2nd โ๐ด)
ยทN (2nd โ๐ถ))โฉ) |
25 | | mulpipq2 10882 |
. . . 4
โข ((๐ต โ (N ร
N) โง ๐ถ
โ (N ร N)) โ (๐ต ยทpQ ๐ถ) = โจ((1st
โ๐ต)
ยทN (1st โ๐ถ)), ((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ) |
26 | 25 | 3adant1 1131 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (๐ต
ยทpQ ๐ถ) = โจ((1st โ๐ต)
ยทN (1st โ๐ถ)), ((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ) |
27 | 24, 26 | breq12d 5123 |
. 2
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((๐ด ยทpQ ๐ถ) ~Q
(๐ต
ยทpQ ๐ถ) โ โจ((1st โ๐ด)
ยทN (1st โ๐ถ)), ((2nd โ๐ด)
ยทN (2nd โ๐ถ))โฉ ~Q
โจ((1st โ๐ต) ยทN
(1st โ๐ถ)),
((2nd โ๐ต)
ยทN (2nd โ๐ถ))โฉ)) |
28 | | enqbreq2 10863 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N)) โ (๐ด ~Q ๐ต โ ((1st
โ๐ด)
ยทN (2nd โ๐ต)) = ((1st โ๐ต)
ยทN (2nd โ๐ด)))) |
29 | 28 | 3adant3 1133 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (๐ด
~Q ๐ต โ ((1st โ๐ด)
ยทN (2nd โ๐ต)) = ((1st โ๐ต)
ยทN (2nd โ๐ด)))) |
30 | | mulclpi 10836 |
. . . . 5
โข
(((1st โ๐ถ) โ N โง
(2nd โ๐ถ)
โ N) โ ((1st โ๐ถ) ยทN
(2nd โ๐ถ))
โ N) |
31 | 4, 10, 30 | syl2anc 585 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((1st โ๐ถ) ยทN
(2nd โ๐ถ))
โ N) |
32 | | mulclpi 10836 |
. . . . 5
โข
(((1st โ๐ด) โ N โง
(2nd โ๐ต)
โ N) โ ((1st โ๐ด) ยทN
(2nd โ๐ต))
โ N) |
33 | 2, 18, 32 | syl2anc 585 |
. . . 4
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((1st โ๐ด) ยทN
(2nd โ๐ต))
โ N) |
34 | | mulcanpi 10843 |
. . . 4
โข
((((1st โ๐ถ) ยทN
(2nd โ๐ถ))
โ N โง ((1st โ๐ด) ยทN
(2nd โ๐ต))
โ N) โ ((((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ ((1st โ๐ด) ยทN
(2nd โ๐ต))
= ((1st โ๐ต) ยทN
(2nd โ๐ด)))) |
35 | 31, 33, 34 | syl2anc 585 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ ((1st โ๐ด) ยทN
(2nd โ๐ต))
= ((1st โ๐ต) ยทN
(2nd โ๐ด)))) |
36 | | mulcompi 10839 |
. . . . . 6
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((1st โ๐ด) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ถ))) |
37 | | fvex 6860 |
. . . . . . 7
โข
(1st โ๐ด) โ V |
38 | | fvex 6860 |
. . . . . . 7
โข
(2nd โ๐ต) โ V |
39 | | fvex 6860 |
. . . . . . 7
โข
(1st โ๐ถ) โ V |
40 | | mulcompi 10839 |
. . . . . . 7
โข (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ) |
41 | | mulasspi 10840 |
. . . . . . 7
โข ((๐ฅ
ยทN ๐ฆ) ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง)) |
42 | | fvex 6860 |
. . . . . . 7
โข
(2nd โ๐ถ) โ V |
43 | 37, 38, 39, 40, 41, 42 | caov4 7590 |
. . . . . 6
โข
(((1st โ๐ด) ยทN
(2nd โ๐ต))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ถ)))
= (((1st โ๐ด) ยทN
(1st โ๐ถ))
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ))) |
44 | 36, 43 | eqtri 2765 |
. . . . 5
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((1st โ๐ด) ยทN
(1st โ๐ถ))
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ))) |
45 | | mulcompi 10839 |
. . . . . 6
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
= (((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ถ))) |
46 | | fvex 6860 |
. . . . . . 7
โข
(1st โ๐ต) โ V |
47 | | fvex 6860 |
. . . . . . 7
โข
(2nd โ๐ด) โ V |
48 | 46, 47, 39, 40, 41, 42 | caov4 7590 |
. . . . . 6
โข
(((1st โ๐ต) ยทN
(2nd โ๐ด))
ยทN ((1st โ๐ถ) ยทN
(2nd โ๐ถ)))
= (((1st โ๐ต) ยทN
(1st โ๐ถ))
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ถ))) |
49 | | mulcompi 10839 |
. . . . . 6
โข
(((1st โ๐ต) ยทN
(1st โ๐ถ))
ยทN ((2nd โ๐ด) ยทN
(2nd โ๐ถ)))
= (((2nd โ๐ด) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(1st โ๐ถ))) |
50 | 45, 48, 49 | 3eqtri 2769 |
. . . . 5
โข
(((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
= (((2nd โ๐ด) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(1st โ๐ถ))) |
51 | 44, 50 | eqeq12i 2755 |
. . . 4
โข
((((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ (((1st โ๐ด) ยทN
(1st โ๐ถ))
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
= (((2nd โ๐ด) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(1st โ๐ถ)))) |
52 | 51 | a1i 11 |
. . 3
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ ((((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ด) ยทN
(2nd โ๐ต)))
= (((1st โ๐ถ) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(2nd โ๐ด)))
โ (((1st โ๐ด) ยทN
(1st โ๐ถ))
ยทN ((2nd โ๐ต) ยทN
(2nd โ๐ถ)))
= (((2nd โ๐ด) ยทN
(2nd โ๐ถ))
ยทN ((1st โ๐ต) ยทN
(1st โ๐ถ))))) |
53 | 29, 35, 52 | 3bitr2d 307 |
. 2
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (๐ด
~Q ๐ต โ (((1st โ๐ด)
ยทN (1st โ๐ถ)) ยทN
((2nd โ๐ต)
ยทN (2nd โ๐ถ))) = (((2nd โ๐ด)
ยทN (2nd โ๐ถ)) ยทN
((1st โ๐ต)
ยทN (1st โ๐ถ))))) |
54 | 22, 27, 53 | 3bitr4rd 312 |
1
โข ((๐ด โ (N ร
N) โง ๐ต
โ (N ร N) โง ๐ถ โ (N ร
N)) โ (๐ด
~Q ๐ต โ (๐ด ยทpQ ๐ถ) ~Q
(๐ต
ยทpQ ๐ถ))) |