Step | Hyp | Ref
| Expression |
1 | | prop 7473 |
. . . . . . . . 9
โข (๐ต โ P โ
โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ
P) |
2 | | elprnql 7479 |
. . . . . . . . 9
โข
((โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ P โง ๐ง โ (1st
โ๐ต)) โ ๐ง โ
Q) |
3 | 1, 2 | sylan 283 |
. . . . . . . 8
โข ((๐ต โ P โง
๐ง โ (1st
โ๐ต)) โ ๐ง โ
Q) |
4 | | prop 7473 |
. . . . . . . . . . . . 13
โข (๐ด โ P โ
โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ
P) |
5 | | elprnql 7479 |
. . . . . . . . . . . . 13
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ฆ โ (1st
โ๐ด)) โ ๐ฆ โ
Q) |
6 | 4, 5 | sylan 283 |
. . . . . . . . . . . 12
โข ((๐ด โ P โง
๐ฆ โ (1st
โ๐ด)) โ ๐ฆ โ
Q) |
7 | | mulcomnqg 7381 |
. . . . . . . . . . . . 13
โข ((๐ง โ Q โง
๐ฆ โ Q)
โ (๐ง
ยทQ ๐ฆ) = (๐ฆ ยทQ ๐ง)) |
8 | 7 | eqeq2d 2189 |
. . . . . . . . . . . 12
โข ((๐ง โ Q โง
๐ฆ โ Q)
โ (๐ฅ = (๐ง
ยทQ ๐ฆ) โ ๐ฅ = (๐ฆ ยทQ ๐ง))) |
9 | 6, 8 | sylan2 286 |
. . . . . . . . . . 11
โข ((๐ง โ Q โง
(๐ด โ P
โง ๐ฆ โ
(1st โ๐ด)))
โ (๐ฅ = (๐ง
ยทQ ๐ฆ) โ ๐ฅ = (๐ฆ ยทQ ๐ง))) |
10 | 9 | anassrs 400 |
. . . . . . . . . 10
โข (((๐ง โ Q โง
๐ด โ P)
โง ๐ฆ โ
(1st โ๐ด))
โ (๐ฅ = (๐ง
ยทQ ๐ฆ) โ ๐ฅ = (๐ฆ ยทQ ๐ง))) |
11 | 10 | rexbidva 2474 |
. . . . . . . . 9
โข ((๐ง โ Q โง
๐ด โ P)
โ (โ๐ฆ โ
(1st โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (1st
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
12 | 11 | ancoms 268 |
. . . . . . . 8
โข ((๐ด โ P โง
๐ง โ Q)
โ (โ๐ฆ โ
(1st โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (1st
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
13 | 3, 12 | sylan2 286 |
. . . . . . 7
โข ((๐ด โ P โง
(๐ต โ P
โง ๐ง โ
(1st โ๐ต)))
โ (โ๐ฆ โ
(1st โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (1st
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
14 | 13 | anassrs 400 |
. . . . . 6
โข (((๐ด โ P โง
๐ต โ P)
โง ๐ง โ
(1st โ๐ต))
โ (โ๐ฆ โ
(1st โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (1st
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
15 | 14 | rexbidva 2474 |
. . . . 5
โข ((๐ด โ P โง
๐ต โ P)
โ (โ๐ง โ
(1st โ๐ต)โ๐ฆ โ (1st โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ง โ (1st
โ๐ต)โ๐ฆ โ (1st
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
16 | | rexcom 2641 |
. . . . 5
โข
(โ๐ง โ
(1st โ๐ต)โ๐ฆ โ (1st โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง) โ โ๐ฆ โ (1st
โ๐ด)โ๐ง โ (1st
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง)) |
17 | 15, 16 | bitrdi 196 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P)
โ (โ๐ง โ
(1st โ๐ต)โ๐ฆ โ (1st โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (1st
โ๐ด)โ๐ง โ (1st
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง))) |
18 | 17 | rabbidv 2726 |
. . 3
โข ((๐ด โ P โง
๐ต โ P)
โ {๐ฅ โ
Q โฃ โ๐ง โ (1st โ๐ต)โ๐ฆ โ (1st โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ)} = {๐ฅ โ Q โฃ โ๐ฆ โ (1st
โ๐ด)โ๐ง โ (1st
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง)}) |
19 | | elprnqu 7480 |
. . . . . . . . 9
โข
((โจ(1st โ๐ต), (2nd โ๐ต)โฉ โ P โง ๐ง โ (2nd
โ๐ต)) โ ๐ง โ
Q) |
20 | 1, 19 | sylan 283 |
. . . . . . . 8
โข ((๐ต โ P โง
๐ง โ (2nd
โ๐ต)) โ ๐ง โ
Q) |
21 | | elprnqu 7480 |
. . . . . . . . . . . . 13
โข
((โจ(1st โ๐ด), (2nd โ๐ด)โฉ โ P โง ๐ฆ โ (2nd
โ๐ด)) โ ๐ฆ โ
Q) |
22 | 4, 21 | sylan 283 |
. . . . . . . . . . . 12
โข ((๐ด โ P โง
๐ฆ โ (2nd
โ๐ด)) โ ๐ฆ โ
Q) |
23 | 22, 8 | sylan2 286 |
. . . . . . . . . . 11
โข ((๐ง โ Q โง
(๐ด โ P
โง ๐ฆ โ
(2nd โ๐ด)))
โ (๐ฅ = (๐ง
ยทQ ๐ฆ) โ ๐ฅ = (๐ฆ ยทQ ๐ง))) |
24 | 23 | anassrs 400 |
. . . . . . . . . 10
โข (((๐ง โ Q โง
๐ด โ P)
โง ๐ฆ โ
(2nd โ๐ด))
โ (๐ฅ = (๐ง
ยทQ ๐ฆ) โ ๐ฅ = (๐ฆ ยทQ ๐ง))) |
25 | 24 | rexbidva 2474 |
. . . . . . . . 9
โข ((๐ง โ Q โง
๐ด โ P)
โ (โ๐ฆ โ
(2nd โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (2nd
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
26 | 25 | ancoms 268 |
. . . . . . . 8
โข ((๐ด โ P โง
๐ง โ Q)
โ (โ๐ฆ โ
(2nd โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (2nd
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
27 | 20, 26 | sylan2 286 |
. . . . . . 7
โข ((๐ด โ P โง
(๐ต โ P
โง ๐ง โ
(2nd โ๐ต)))
โ (โ๐ฆ โ
(2nd โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (2nd
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
28 | 27 | anassrs 400 |
. . . . . 6
โข (((๐ด โ P โง
๐ต โ P)
โง ๐ง โ
(2nd โ๐ต))
โ (โ๐ฆ โ
(2nd โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (2nd
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
29 | 28 | rexbidva 2474 |
. . . . 5
โข ((๐ด โ P โง
๐ต โ P)
โ (โ๐ง โ
(2nd โ๐ต)โ๐ฆ โ (2nd โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ง โ (2nd
โ๐ต)โ๐ฆ โ (2nd
โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง))) |
30 | | rexcom 2641 |
. . . . 5
โข
(โ๐ง โ
(2nd โ๐ต)โ๐ฆ โ (2nd โ๐ด)๐ฅ = (๐ฆ ยทQ ๐ง) โ โ๐ฆ โ (2nd
โ๐ด)โ๐ง โ (2nd
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง)) |
31 | 29, 30 | bitrdi 196 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P)
โ (โ๐ง โ
(2nd โ๐ต)โ๐ฆ โ (2nd โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ) โ โ๐ฆ โ (2nd
โ๐ด)โ๐ง โ (2nd
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง))) |
32 | 31 | rabbidv 2726 |
. . 3
โข ((๐ด โ P โง
๐ต โ P)
โ {๐ฅ โ
Q โฃ โ๐ง โ (2nd โ๐ต)โ๐ฆ โ (2nd โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ)} = {๐ฅ โ Q โฃ โ๐ฆ โ (2nd
โ๐ด)โ๐ง โ (2nd
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง)}) |
33 | 18, 32 | opeq12d 3786 |
. 2
โข ((๐ด โ P โง
๐ต โ P)
โ โจ{๐ฅ โ
Q โฃ โ๐ง โ (1st โ๐ต)โ๐ฆ โ (1st โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ)}, {๐ฅ โ Q โฃ โ๐ง โ (2nd
โ๐ต)โ๐ฆ โ (2nd
โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ)}โฉ = โจ{๐ฅ โ Q โฃ
โ๐ฆ โ
(1st โ๐ด)โ๐ง โ (1st โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง)}, {๐ฅ โ Q โฃ โ๐ฆ โ (2nd
โ๐ด)โ๐ง โ (2nd
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง)}โฉ) |
34 | | mpvlu 7537 |
. . 3
โข ((๐ต โ P โง
๐ด โ P)
โ (๐ต
ยทP ๐ด) = โจ{๐ฅ โ Q โฃ โ๐ง โ (1st
โ๐ต)โ๐ฆ โ (1st
โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ)}, {๐ฅ โ Q โฃ โ๐ง โ (2nd
โ๐ต)โ๐ฆ โ (2nd
โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ)}โฉ) |
35 | 34 | ancoms 268 |
. 2
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ต
ยทP ๐ด) = โจ{๐ฅ โ Q โฃ โ๐ง โ (1st
โ๐ต)โ๐ฆ โ (1st
โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ)}, {๐ฅ โ Q โฃ โ๐ง โ (2nd
โ๐ต)โ๐ฆ โ (2nd
โ๐ด)๐ฅ = (๐ง ยทQ ๐ฆ)}โฉ) |
36 | | mpvlu 7537 |
. 2
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ด
ยทP ๐ต) = โจ{๐ฅ โ Q โฃ โ๐ฆ โ (1st
โ๐ด)โ๐ง โ (1st
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง)}, {๐ฅ โ Q โฃ โ๐ฆ โ (2nd
โ๐ด)โ๐ง โ (2nd
โ๐ต)๐ฅ = (๐ฆ ยทQ ๐ง)}โฉ) |
37 | 33, 35, 36 | 3eqtr4rd 2221 |
1
โข ((๐ด โ P โง
๐ต โ P)
โ (๐ด
ยทP ๐ต) = (๐ต ยทP ๐ด)) |