Step | Hyp | Ref
| Expression |
1 | | nqpi 7379 |
. . . 4
โข (๐ด โ Q โ
โ๐งโ๐ค((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q
)) |
2 | | nqpi 7379 |
. . . 4
โข (๐ต โ Q โ
โ๐ฃโ๐ข((๐ฃ โ N โง ๐ข โ N) โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q
)) |
3 | 1, 2 | anim12i 338 |
. . 3
โข ((๐ด โ Q โง
๐ต โ Q)
โ (โ๐งโ๐ค((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โง
โ๐ฃโ๐ข((๐ฃ โ N โง ๐ข โ N) โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q
))) |
4 | | ee4anv 1934 |
. . 3
โข
(โ๐งโ๐คโ๐ฃโ๐ข(((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โง
((๐ฃ โ N
โง ๐ข โ
N) โง ๐ต =
[โจ๐ฃ, ๐ขโฉ]
~Q )) โ (โ๐งโ๐ค((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โง
โ๐ฃโ๐ข((๐ฃ โ N โง ๐ข โ N) โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q
))) |
5 | 3, 4 | sylibr 134 |
. 2
โข ((๐ด โ Q โง
๐ต โ Q)
โ โ๐งโ๐คโ๐ฃโ๐ข(((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โง
((๐ฃ โ N
โง ๐ข โ
N) โง ๐ต =
[โจ๐ฃ, ๐ขโฉ]
~Q ))) |
6 | | oveq12 5886 |
. . . . . . 7
โข ((๐ด = [โจ๐ง, ๐คโฉ] ~Q โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q ) โ
(๐ด
ยทQ ๐ต) = ([โจ๐ง, ๐คโฉ] ~Q
ยทQ [โจ๐ฃ, ๐ขโฉ] ~Q
)) |
7 | | mulpiord 7318 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ฃ โ N)
โ (๐ง
ยทN ๐ฃ) = (๐ง ยทo ๐ฃ)) |
8 | 7 | ad2ant2r 509 |
. . . . . . . . . 10
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ง ยทN ๐ฃ) = (๐ง ยทo ๐ฃ)) |
9 | | mulpiord 7318 |
. . . . . . . . . . 11
โข ((๐ค โ N โง
๐ข โ N)
โ (๐ค
ยทN ๐ข) = (๐ค ยทo ๐ข)) |
10 | 9 | ad2ant2l 508 |
. . . . . . . . . 10
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ค ยทN ๐ข) = (๐ค ยทo ๐ข)) |
11 | 8, 10 | opeq12d 3788 |
. . . . . . . . 9
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ โจ(๐ง ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ = โจ(๐ง ยทo ๐ฃ), (๐ค ยทo ๐ข)โฉ) |
12 | 11 | eceq1d 6573 |
. . . . . . . 8
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ [โจ(๐ง ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q0 = [โจ(๐ง ยทo ๐ฃ), (๐ค ยทo ๐ข)โฉ] ~Q0
) |
13 | | mulpipqqs 7374 |
. . . . . . . . 9
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q
ยทQ [โจ๐ฃ, ๐ขโฉ] ~Q ) =
[โจ(๐ง
ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q ) |
14 | | mulclpi 7329 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ฃ โ N)
โ (๐ง
ยทN ๐ฃ) โ N) |
15 | 14 | ad2ant2r 509 |
. . . . . . . . . 10
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ง ยทN ๐ฃ) โ
N) |
16 | | mulclpi 7329 |
. . . . . . . . . . 11
โข ((๐ค โ N โง
๐ข โ N)
โ (๐ค
ยทN ๐ข) โ N) |
17 | 16 | ad2ant2l 508 |
. . . . . . . . . 10
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ค ยทN ๐ข) โ
N) |
18 | | nqnq0pi 7439 |
. . . . . . . . . 10
โข (((๐ง
ยทN ๐ฃ) โ N โง (๐ค
ยทN ๐ข) โ N) โ
[โจ(๐ง
ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q0 = [โจ(๐ง ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q ) |
19 | 15, 17, 18 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ [โจ(๐ง ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q0 = [โจ(๐ง ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q ) |
20 | 13, 19 | eqtr4d 2213 |
. . . . . . . 8
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q
ยทQ [โจ๐ฃ, ๐ขโฉ] ~Q ) =
[โจ(๐ง
ยทN ๐ฃ), (๐ค ยทN ๐ข)โฉ]
~Q0 ) |
21 | | pinn 7310 |
. . . . . . . . . 10
โข (๐ง โ N โ
๐ง โ
ฯ) |
22 | 21 | anim1i 340 |
. . . . . . . . 9
โข ((๐ง โ N โง
๐ค โ N)
โ (๐ง โ ฯ
โง ๐ค โ
N)) |
23 | | pinn 7310 |
. . . . . . . . . 10
โข (๐ฃ โ N โ
๐ฃ โ
ฯ) |
24 | 23 | anim1i 340 |
. . . . . . . . 9
โข ((๐ฃ โ N โง
๐ข โ N)
โ (๐ฃ โ ฯ
โง ๐ข โ
N)) |
25 | | mulnnnq0 7451 |
. . . . . . . . 9
โข (((๐ง โ ฯ โง ๐ค โ N) โง
(๐ฃ โ ฯ โง
๐ข โ N))
โ ([โจ๐ง, ๐คโฉ]
~Q0 ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ) =
[โจ(๐ง
ยทo ๐ฃ),
(๐ค ยทo
๐ข)โฉ]
~Q0 ) |
26 | 22, 24, 25 | syl2an 289 |
. . . . . . . 8
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0 ) =
[โจ(๐ง
ยทo ๐ฃ),
(๐ค ยทo
๐ข)โฉ]
~Q0 ) |
27 | 12, 20, 26 | 3eqtr4d 2220 |
. . . . . . 7
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q
ยทQ [โจ๐ฃ, ๐ขโฉ] ~Q ) =
([โจ๐ง, ๐คโฉ]
~Q0 ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)) |
28 | 6, 27 | sylan9eqr 2232 |
. . . . . 6
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โง (๐ด = [โจ๐ง, ๐คโฉ] ~Q โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q )) โ
(๐ด
ยทQ ๐ต) = ([โจ๐ง, ๐คโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)) |
29 | | nqnq0pi 7439 |
. . . . . . . . . . 11
โข ((๐ง โ N โง
๐ค โ N)
โ [โจ๐ง, ๐คโฉ]
~Q0 = [โจ๐ง, ๐คโฉ] ~Q
) |
30 | 29 | adantr 276 |
. . . . . . . . . 10
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ [โจ๐ง, ๐คโฉ] ~Q0 =
[โจ๐ง, ๐คโฉ]
~Q ) |
31 | 30 | eqeq2d 2189 |
. . . . . . . . 9
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โ
๐ด = [โจ๐ง, ๐คโฉ] ~Q
)) |
32 | | nqnq0pi 7439 |
. . . . . . . . . . 11
โข ((๐ฃ โ N โง
๐ข โ N)
โ [โจ๐ฃ, ๐ขโฉ]
~Q0 = [โจ๐ฃ, ๐ขโฉ] ~Q
) |
33 | 32 | adantl 277 |
. . . . . . . . . 10
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ [โจ๐ฃ, ๐ขโฉ] ~Q0 =
[โจ๐ฃ, ๐ขโฉ]
~Q ) |
34 | 33 | eqeq2d 2189 |
. . . . . . . . 9
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q0 โ
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q
)) |
35 | 31, 34 | anbi12d 473 |
. . . . . . . 8
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ((๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q0 ) โ
(๐ด = [โจ๐ง, ๐คโฉ] ~Q โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q
))) |
36 | 35 | pm5.32i 454 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โง (๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q0 ))
โ (((๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โง
(๐ด = [โจ๐ง, ๐คโฉ] ~Q โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q
))) |
37 | | oveq12 5886 |
. . . . . . . 8
โข ((๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q0 ) โ
(๐ด
ยทQ0 ๐ต) = ([โจ๐ง, ๐คโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)) |
38 | 37 | adantl 277 |
. . . . . . 7
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โง (๐ด = [โจ๐ง, ๐คโฉ] ~Q0 โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q0 ))
โ (๐ด
ยทQ0 ๐ต) = ([โจ๐ง, ๐คโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)) |
39 | 36, 38 | sylbir 135 |
. . . . . 6
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โง (๐ด = [โจ๐ง, ๐คโฉ] ~Q โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q )) โ
(๐ด
ยทQ0 ๐ต) = ([โจ๐ง, ๐คโฉ] ~Q0
ยทQ0 [โจ๐ฃ, ๐ขโฉ] ~Q0
)) |
40 | 28, 39 | eqtr4d 2213 |
. . . . 5
โข ((((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โง (๐ด = [โจ๐ง, ๐คโฉ] ~Q โง
๐ต = [โจ๐ฃ, ๐ขโฉ] ~Q )) โ
(๐ด
ยทQ ๐ต) = (๐ด ยทQ0 ๐ต)) |
41 | 40 | an4s 588 |
. . . 4
โข ((((๐ง โ N โง
๐ค โ N)
โง ๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โง
((๐ฃ โ N
โง ๐ข โ
N) โง ๐ต =
[โจ๐ฃ, ๐ขโฉ]
~Q )) โ (๐ด ยทQ ๐ต) = (๐ด ยทQ0 ๐ต)) |
42 | 41 | exlimivv 1896 |
. . 3
โข
(โ๐ฃโ๐ข(((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โง
((๐ฃ โ N
โง ๐ข โ
N) โง ๐ต =
[โจ๐ฃ, ๐ขโฉ]
~Q )) โ (๐ด ยทQ ๐ต) = (๐ด ยทQ0 ๐ต)) |
43 | 42 | exlimivv 1896 |
. 2
โข
(โ๐งโ๐คโ๐ฃโ๐ข(((๐ง โ N โง ๐ค โ N) โง
๐ด = [โจ๐ง, ๐คโฉ] ~Q ) โง
((๐ฃ โ N
โง ๐ข โ
N) โง ๐ต =
[โจ๐ฃ, ๐ขโฉ]
~Q )) โ (๐ด ยทQ ๐ต) = (๐ด ยทQ0 ๐ต)) |
44 | 5, 43 | syl 14 |
1
โข ((๐ด โ Q โง
๐ต โ Q)
โ (๐ด
ยทQ ๐ต) = (๐ด ยทQ0 ๐ต)) |