Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7346 |
. 2
โข
Q = ((N ร N) /
~Q ) |
2 | | mulpipqqs 7371 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
ยทQ [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ(๐ฅ
ยทN ๐ง), (๐ฆ ยทN ๐ค)โฉ]
~Q ) |
3 | | mulpipqqs 7371 |
. 2
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q
ยทQ [โจ๐ฃ, ๐ขโฉ] ~Q ) =
[โจ(๐ง
ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q ) |
4 | | mulpipqqs 7371 |
. 2
โข ((((๐ฅ
ยทN ๐ง) โ N โง (๐ฆ
ยทN ๐ค) โ N) โง (๐ฃ โ N โง
๐ข โ N))
โ ([โจ(๐ฅ
ยทN ๐ง), (๐ฆ ยทN ๐ค)โฉ]
~Q ยทQ [โจ๐ฃ, ๐ขโฉ] ~Q ) =
[โจ((๐ฅ
ยทN ๐ง) ยทN ๐ฃ), ((๐ฆ ยทN ๐ค)
ยทN ๐ข)โฉ] ~Q
) |
5 | | mulpipqqs 7371 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง ((๐ง
ยทN ๐ฃ) โ N โง (๐ค
ยทN ๐ข) โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q ยทQ [โจ(๐ง
ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q ) = [โจ(๐ฅ ยทN (๐ง
ยทN ๐ฃ)), (๐ฆ ยทN (๐ค
ยทN ๐ข))โฉ] ~Q
) |
6 | | mulclpi 7326 |
. . . 4
โข ((๐ฅ โ N โง
๐ง โ N)
โ (๐ฅ
ยทN ๐ง) โ N) |
7 | 6 | ad2ant2r 509 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ (๐ฅ ยทN ๐ง) โ
N) |
8 | | mulclpi 7326 |
. . . 4
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) โ N) |
9 | 8 | ad2ant2l 508 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ (๐ฆ ยทN ๐ค) โ
N) |
10 | 7, 9 | jca 306 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ((๐ฅ ยทN ๐ง) โ N โง
(๐ฆ
ยทN ๐ค) โ N)) |
11 | | mulclpi 7326 |
. . . 4
โข ((๐ง โ N โง
๐ฃ โ N)
โ (๐ง
ยทN ๐ฃ) โ N) |
12 | 11 | ad2ant2r 509 |
. . 3
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ง ยทN ๐ฃ) โ
N) |
13 | | mulclpi 7326 |
. . . 4
โข ((๐ค โ N โง
๐ข โ N)
โ (๐ค
ยทN ๐ข) โ N) |
14 | 13 | ad2ant2l 508 |
. . 3
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ค ยทN ๐ข) โ
N) |
15 | 12, 14 | jca 306 |
. 2
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ((๐ง ยทN ๐ฃ) โ N โง
(๐ค
ยทN ๐ข) โ N)) |
16 | | mulasspig 7330 |
. . . . 5
โข ((๐ฅ โ N โง
๐ง โ N
โง ๐ฃ โ
N) โ ((๐ฅ
ยทN ๐ง) ยทN ๐ฃ) = (๐ฅ ยทN (๐ง
ยทN ๐ฃ))) |
17 | 16 | 3adant1r 1231 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง ๐ง โ
N โง ๐ฃ
โ N) โ ((๐ฅ ยทN ๐ง)
ยทN ๐ฃ) = (๐ฅ ยทN (๐ง
ยทN ๐ฃ))) |
18 | 17 | 3adant2r 1233 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง ๐ฃ โ N) โ ((๐ฅ
ยทN ๐ง) ยทN ๐ฃ) = (๐ฅ ยทN (๐ง
ยทN ๐ฃ))) |
19 | 18 | 3adant3r 1235 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฅ
ยทN ๐ง) ยทN ๐ฃ) = (๐ฅ ยทN (๐ง
ยทN ๐ฃ))) |
20 | | mulasspig 7330 |
. . . . 5
โข ((๐ฆ โ N โง
๐ค โ N
โง ๐ข โ
N) โ ((๐ฆ
ยทN ๐ค) ยทN ๐ข) = (๐ฆ ยทN (๐ค
ยทN ๐ข))) |
21 | 20 | 3adant1l 1230 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง ๐ค โ
N โง ๐ข
โ N) โ ((๐ฆ ยทN ๐ค)
ยทN ๐ข) = (๐ฆ ยทN (๐ค
ยทN ๐ข))) |
22 | 21 | 3adant2l 1232 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง ๐ข โ N) โ ((๐ฆ
ยทN ๐ค) ยทN ๐ข) = (๐ฆ ยทN (๐ค
ยทN ๐ข))) |
23 | 22 | 3adant3l 1234 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฆ
ยทN ๐ค) ยทN ๐ข) = (๐ฆ ยทN (๐ค
ยทN ๐ข))) |
24 | 1, 2, 3, 4, 5, 10,
15, 19, 23 | ecoviass 6644 |
1
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ ((๐ด
ยทQ ๐ต) ยทQ ๐ถ) = (๐ด ยทQ (๐ต
ยทQ ๐ถ))) |