Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7346 |
. 2
โข
Q = ((N ร N) /
~Q ) |
2 | | addpipqqs 7368 |
. 2
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ง, ๐คโฉ] ~Q
+Q [โจ๐ฃ, ๐ขโฉ] ~Q ) =
[โจ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)), (๐ค ยทN ๐ข)โฉ]
~Q ) |
3 | | mulpipqqs 7371 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N โง (๐ค
ยทN ๐ข) โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q ยทQ [โจ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)), (๐ค ยทN ๐ข)โฉ]
~Q ) = [โจ(๐ฅ ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ))), (๐ฆ ยทN (๐ค
ยทN ๐ข))โฉ] ~Q
) |
4 | | mulclpi 7326 |
. . . . . . 7
โข ((๐ฅ โ N โง
((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N) โ (๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N) |
5 | | simpl 109 |
. . . . . . . 8
โข ((๐ฆ โ N โง
(๐ค
ยทN ๐ข) โ N) โ ๐ฆ โ
N) |
6 | | mulclpi 7326 |
. . . . . . . 8
โข ((๐ฆ โ N โง
(๐ค
ยทN ๐ข) โ N) โ (๐ฆ
ยทN (๐ค ยทN ๐ข)) โ
N) |
7 | 5, 6 | jca 306 |
. . . . . . 7
โข ((๐ฆ โ N โง
(๐ค
ยทN ๐ข) โ N) โ (๐ฆ โ N โง
(๐ฆ
ยทN (๐ค ยทN ๐ข)) โ
N)) |
8 | 4, 7 | anim12i 338 |
. . . . . 6
โข (((๐ฅ โ N โง
((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N) โง (๐ฆ โ N โง
(๐ค
ยทN ๐ข) โ N)) โ ((๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ โ N โง
(๐ฆ
ยทN (๐ค ยทN ๐ข)) โ
N))) |
9 | | an12 561 |
. . . . . . 7
โข (((๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ โ N โง
(๐ฆ
ยทN (๐ค ยทN ๐ข)) โ N))
โ (๐ฆ โ
N โง ((๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ
ยทN (๐ค ยทN ๐ข)) โ
N))) |
10 | | 3anass 982 |
. . . . . . 7
โข ((๐ฆ โ N โง
(๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ
ยทN (๐ค ยทN ๐ข)) โ N)
โ (๐ฆ โ
N โง ((๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ
ยทN (๐ค ยทN ๐ข)) โ
N))) |
11 | 9, 10 | bitr4i 187 |
. . . . . 6
โข (((๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ โ N โง
(๐ฆ
ยทN (๐ค ยทN ๐ข)) โ N))
โ (๐ฆ โ
N โง (๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ
ยทN (๐ค ยทN ๐ข)) โ
N)) |
12 | 8, 11 | sylib 122 |
. . . . 5
โข (((๐ฅ โ N โง
((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N) โง (๐ฆ โ N โง
(๐ค
ยทN ๐ข) โ N)) โ (๐ฆ โ N โง
(๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ
ยทN (๐ค ยทN ๐ข)) โ
N)) |
13 | 12 | an4s 588 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N โง (๐ค
ยทN ๐ข) โ N)) โ (๐ฆ โ N โง
(๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ
ยทN (๐ค ยทN ๐ข)) โ
N)) |
14 | | mulcanenqec 7384 |
. . . 4
โข ((๐ฆ โ N โง
(๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))) โ N โง (๐ฆ
ยทN (๐ค ยทN ๐ข)) โ N)
โ [โจ(๐ฆ
ยทN (๐ฅ ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)))), (๐ฆ ยทN (๐ฆ
ยทN (๐ค ยทN ๐ข)))โฉ]
~Q = [โจ(๐ฅ ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ))), (๐ฆ ยทN (๐ค
ยทN ๐ข))โฉ] ~Q
) |
15 | 13, 14 | syl 14 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N โง (๐ค
ยทN ๐ข) โ N)) โ
[โจ(๐ฆ
ยทN (๐ฅ ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)))), (๐ฆ ยทN (๐ฆ
ยทN (๐ค ยทN ๐ข)))โฉ]
~Q = [โจ(๐ฅ ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ))), (๐ฆ ยทN (๐ค
ยทN ๐ข))โฉ] ~Q
) |
16 | 3, 15 | eqtr4d 2213 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N โง (๐ค
ยทN ๐ข) โ N)) โ
([โจ๐ฅ, ๐ฆโฉ]
~Q ยทQ [โจ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)), (๐ค ยทN ๐ข)โฉ]
~Q ) = [โจ(๐ฆ ยทN (๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ)))), (๐ฆ ยทN (๐ฆ
ยทN (๐ค ยทN ๐ข)))โฉ]
~Q ) |
17 | | mulpipqqs 7371 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
ยทQ [โจ๐ง, ๐คโฉ] ~Q ) =
[โจ(๐ฅ
ยทN ๐ง), (๐ฆ ยทN ๐ค)โฉ]
~Q ) |
18 | | mulpipqqs 7371 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ([โจ๐ฅ, ๐ฆโฉ] ~Q
ยทQ [โจ๐ฃ, ๐ขโฉ] ~Q ) =
[โจ(๐ฅ
ยทN ๐ฃ), (๐ฆ ยทN ๐ข)โฉ]
~Q ) |
19 | | addpipqqs 7368 |
. 2
โข ((((๐ฅ
ยทN ๐ง) โ N โง (๐ฆ
ยทN ๐ค) โ N) โง ((๐ฅ
ยทN ๐ฃ) โ N โง (๐ฆ
ยทN ๐ข) โ N)) โ
([โจ(๐ฅ
ยทN ๐ง), (๐ฆ ยทN ๐ค)โฉ]
~Q +Q [โจ(๐ฅ
ยทN ๐ฃ), (๐ฆ ยทN ๐ข)โฉ]
~Q ) = [โจ(((๐ฅ ยทN ๐ง)
ยทN (๐ฆ ยทN ๐ข)) +N
((๐ฆ
ยทN ๐ค) ยทN (๐ฅ
ยทN ๐ฃ))), ((๐ฆ ยทN ๐ค)
ยทN (๐ฆ ยทN ๐ข))โฉ]
~Q ) |
20 | | mulclpi 7326 |
. . . . 5
โข ((๐ง โ N โง
๐ข โ N)
โ (๐ง
ยทN ๐ข) โ N) |
21 | | mulclpi 7326 |
. . . . 5
โข ((๐ค โ N โง
๐ฃ โ N)
โ (๐ค
ยทN ๐ฃ) โ N) |
22 | | addclpi 7325 |
. . . . 5
โข (((๐ง
ยทN ๐ข) โ N โง (๐ค
ยทN ๐ฃ) โ N) โ ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N) |
23 | 20, 21, 22 | syl2an 289 |
. . . 4
โข (((๐ง โ N โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ)) โ N) |
24 | 23 | an42s 589 |
. . 3
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ)) โ N) |
25 | | mulclpi 7326 |
. . . 4
โข ((๐ค โ N โง
๐ข โ N)
โ (๐ค
ยทN ๐ข) โ N) |
26 | 25 | ad2ant2l 508 |
. . 3
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (๐ค ยทN ๐ข) โ
N) |
27 | 24, 26 | jca 306 |
. 2
โข (((๐ง โ N โง
๐ค โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ (((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ)) โ N โง (๐ค
ยทN ๐ข) โ N)) |
28 | | mulclpi 7326 |
. . . 4
โข ((๐ฅ โ N โง
๐ง โ N)
โ (๐ฅ
ยทN ๐ง) โ N) |
29 | | mulclpi 7326 |
. . . 4
โข ((๐ฆ โ N โง
๐ค โ N)
โ (๐ฆ
ยทN ๐ค) โ N) |
30 | 28, 29 | anim12i 338 |
. . 3
โข (((๐ฅ โ N โง
๐ง โ N)
โง (๐ฆ โ
N โง ๐ค
โ N)) โ ((๐ฅ ยทN ๐ง) โ N โง
(๐ฆ
ยทN ๐ค) โ N)) |
31 | 30 | an4s 588 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N)) โ ((๐ฅ ยทN ๐ง) โ N โง
(๐ฆ
ยทN ๐ค) โ N)) |
32 | | mulclpi 7326 |
. . . 4
โข ((๐ฅ โ N โง
๐ฃ โ N)
โ (๐ฅ
ยทN ๐ฃ) โ N) |
33 | | mulclpi 7326 |
. . . 4
โข ((๐ฆ โ N โง
๐ข โ N)
โ (๐ฆ
ยทN ๐ข) โ N) |
34 | 32, 33 | anim12i 338 |
. . 3
โข (((๐ฅ โ N โง
๐ฃ โ N)
โง (๐ฆ โ
N โง ๐ข
โ N)) โ ((๐ฅ ยทN ๐ฃ) โ N โง
(๐ฆ
ยทN ๐ข) โ N)) |
35 | 34 | an4s 588 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ฃ โ
N โง ๐ข
โ N)) โ ((๐ฅ ยทN ๐ฃ) โ N โง
(๐ฆ
ยทN ๐ข) โ N)) |
36 | | an42 587 |
. . . . 5
โข (((๐ง โ N โง
๐ข โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ((๐ง โ N โง ๐ค โ N) โง
(๐ฃ โ N
โง ๐ข โ
N))) |
37 | 36 | anbi2i 457 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง ((๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)))
โ ((๐ฅ โ
N โง ๐ฆ
โ N) โง ((๐ง โ N โง ๐ค โ N) โง
(๐ฃ โ N
โง ๐ข โ
N)))) |
38 | | 3anass 982 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ฅ โ N
โง ๐ฆ โ
N) โง ((๐ง
โ N โง ๐ข โ N) โง (๐ค โ N โง
๐ฃ โ
N)))) |
39 | | 3anass 982 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
((๐ฅ โ N
โง ๐ฆ โ
N) โง ((๐ง
โ N โง ๐ค โ N) โง (๐ฃ โ N โง
๐ข โ
N)))) |
40 | 37, 38, 39 | 3bitr4i 212 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ฅ โ N
โง ๐ฆ โ
N) โง (๐ง
โ N โง ๐ค โ N) โง (๐ฃ โ N โง
๐ข โ
N))) |
41 | | mulclpi 7326 |
. . . . . 6
โข ((๐ฆ โ N โง
๐ฅ โ N)
โ (๐ฆ
ยทN ๐ฅ) โ N) |
42 | 41 | ancoms 268 |
. . . . 5
โข ((๐ฅ โ N โง
๐ฆ โ N)
โ (๐ฆ
ยทN ๐ฅ) โ N) |
43 | | distrpig 7331 |
. . . . 5
โข (((๐ฆ
ยทN ๐ฅ) โ N โง (๐ง
ยทN ๐ข) โ N โง (๐ค
ยทN ๐ฃ) โ N) โ ((๐ฆ
ยทN ๐ฅ) ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ))) = (((๐ฆ ยทN ๐ฅ)
ยทN (๐ง ยทN ๐ข)) +N
((๐ฆ
ยทN ๐ฅ) ยทN (๐ค
ยทN ๐ฃ)))) |
44 | 42, 20, 21, 43 | syl3an 1280 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ฆ
ยทN ๐ฅ) ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ))) = (((๐ฆ ยทN ๐ฅ)
ยทN (๐ง ยทN ๐ข)) +N
((๐ฆ
ยทN ๐ฅ) ยทN (๐ค
ยทN ๐ฃ)))) |
45 | | simp1r 1022 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
๐ฆ โ
N) |
46 | | simp1l 1021 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
๐ฅ โ
N) |
47 | 20 | 3ad2ant2 1019 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
(๐ง
ยทN ๐ข) โ N) |
48 | 21 | 3ad2ant3 1020 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
(๐ค
ยทN ๐ฃ) โ N) |
49 | 47, 48, 22 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N) |
50 | | mulasspig 7330 |
. . . . 5
โข ((๐ฆ โ N โง
๐ฅ โ N
โง ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)) โ N) โ ((๐ฆ
ยทN ๐ฅ) ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ))) = (๐ฆ ยทN (๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))))) |
51 | 45, 46, 49, 50 | syl3anc 1238 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ฆ
ยทN ๐ฅ) ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ))) = (๐ฆ ยทN (๐ฅ
ยทN ((๐ง ยทN ๐ข) +N
(๐ค
ยทN ๐ฃ))))) |
52 | | mulcompig 7329 |
. . . . . . . . 9
โข ((๐ฅ โ N โง
๐ฆ โ N)
โ (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ)) |
53 | 52 | oveq1d 5889 |
. . . . . . . 8
โข ((๐ฅ โ N โง
๐ฆ โ N)
โ ((๐ฅ
ยทN ๐ฆ) ยทN (๐ง
ยทN ๐ข)) = ((๐ฆ ยทN ๐ฅ)
ยทN (๐ง ยทN ๐ข))) |
54 | 53 | adantr 276 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โ ((๐ฅ ยทN ๐ฆ)
ยทN (๐ง ยทN ๐ข)) = ((๐ฆ ยทN ๐ฅ)
ยทN (๐ง ยทN ๐ข))) |
55 | | simpll 527 |
. . . . . . . 8
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โ ๐ฅ โ N) |
56 | | simplr 528 |
. . . . . . . 8
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โ ๐ฆ โ N) |
57 | | simprl 529 |
. . . . . . . 8
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โ ๐ง โ N) |
58 | | mulcompig 7329 |
. . . . . . . . 9
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
59 | 58 | adantl 277 |
. . . . . . . 8
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โง (๐ โ N โง ๐ โ N)) โ
(๐
ยทN ๐) = (๐ ยทN ๐)) |
60 | | mulasspig 7330 |
. . . . . . . . 9
โข ((๐ โ N โง
๐ โ N
โง โ โ
N) โ ((๐
ยทN ๐) ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
61 | 60 | adantl 277 |
. . . . . . . 8
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โง (๐ โ N โง ๐ โ N โง
โ โ N))
โ ((๐
ยทN ๐) ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
62 | | simprr 531 |
. . . . . . . 8
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โ ๐ข โ N) |
63 | | mulclpi 7326 |
. . . . . . . . 9
โข ((๐ โ N โง
๐ โ N)
โ (๐
ยทN ๐) โ N) |
64 | 63 | adantl 277 |
. . . . . . . 8
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โง (๐ โ N โง ๐ โ N)) โ
(๐
ยทN ๐) โ N) |
65 | 55, 56, 57, 59, 61, 62, 64 | caov4d 6058 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โ ((๐ฅ ยทN ๐ฆ)
ยทN (๐ง ยทN ๐ข)) = ((๐ฅ ยทN ๐ง)
ยทN (๐ฆ ยทN ๐ข))) |
66 | 54, 65 | eqtr3d 2212 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N)) โ ((๐ฆ ยทN ๐ฅ)
ยทN (๐ง ยทN ๐ข)) = ((๐ฅ ยทN ๐ง)
ยทN (๐ฆ ยทN ๐ข))) |
67 | 66 | 3adant3 1017 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ฆ
ยทN ๐ฅ) ยทN (๐ง
ยทN ๐ข)) = ((๐ฅ ยทN ๐ง)
ยทN (๐ฆ ยทN ๐ข))) |
68 | | simplr 528 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ๐ฆ โ N) |
69 | | simpll 527 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ๐ฅ โ N) |
70 | | simprl 529 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ๐ค โ N) |
71 | 58 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ โ N โง ๐ โ N)) โ
(๐
ยทN ๐) = (๐ ยทN ๐)) |
72 | 60 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ โ N โง ๐ โ N โง
โ โ N))
โ ((๐
ยทN ๐) ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
73 | | simprr 531 |
. . . . . . 7
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ๐ฃ โ N) |
74 | 63 | adantl 277 |
. . . . . . 7
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โง (๐ โ N โง ๐ โ N)) โ
(๐
ยทN ๐) โ N) |
75 | 68, 69, 70, 71, 72, 73, 74 | caov4d 6058 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ค โ
N โง ๐ฃ
โ N)) โ ((๐ฆ ยทN ๐ฅ)
ยทN (๐ค ยทN ๐ฃ)) = ((๐ฆ ยทN ๐ค)
ยทN (๐ฅ ยทN ๐ฃ))) |
76 | 75 | 3adant2 1016 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ฆ
ยทN ๐ฅ) ยทN (๐ค
ยทN ๐ฃ)) = ((๐ฆ ยทN ๐ค)
ยทN (๐ฅ ยทN ๐ฃ))) |
77 | 67, 76 | oveq12d 5892 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
(((๐ฆ
ยทN ๐ฅ) ยทN (๐ง
ยทN ๐ข)) +N ((๐ฆ
ยทN ๐ฅ) ยทN (๐ค
ยทN ๐ฃ))) = (((๐ฅ ยทN ๐ง)
ยทN (๐ฆ ยทN ๐ข)) +N
((๐ฆ
ยทN ๐ค) ยทN (๐ฅ
ยทN ๐ฃ)))) |
78 | 44, 51, 77 | 3eqtr3d 2218 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
(๐ฆ
ยทN (๐ฅ ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)))) = (((๐ฅ ยทN ๐ง)
ยทN (๐ฆ ยทN ๐ข)) +N
((๐ฆ
ยทN ๐ค) ยทN (๐ฅ
ยทN ๐ฃ)))) |
79 | 40, 78 | sylbir 135 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฆ
ยทN (๐ฅ ยทN ((๐ง
ยทN ๐ข) +N (๐ค
ยทN ๐ฃ)))) = (((๐ฅ ยทN ๐ง)
ยทN (๐ฆ ยทN ๐ข)) +N
((๐ฆ
ยทN ๐ค) ยทN (๐ฅ
ยทN ๐ฃ)))) |
80 | 70 | 3adant2 1016 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
๐ค โ
N) |
81 | 62 | 3adant3 1017 |
. . . . . 6
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
๐ข โ
N) |
82 | 80, 81, 25 | syl2anc 411 |
. . . . 5
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
(๐ค
ยทN ๐ข) โ N) |
83 | | mulasspig 7330 |
. . . . 5
โข ((๐ฆ โ N โง
๐ฆ โ N
โง (๐ค
ยทN ๐ข) โ N) โ ((๐ฆ
ยทN ๐ฆ) ยทN (๐ค
ยทN ๐ข)) = (๐ฆ ยทN (๐ฆ
ยทN (๐ค ยทN ๐ข)))) |
84 | 45, 45, 82, 83 | syl3anc 1238 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ฆ
ยทN ๐ฆ) ยทN (๐ค
ยทN ๐ข)) = (๐ฆ ยทN (๐ฆ
ยทN (๐ค ยทN ๐ข)))) |
85 | 58 | adantl 277 |
. . . . 5
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
ยทN ๐) = (๐ ยทN ๐)) |
86 | 60 | adantl 277 |
. . . . 5
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โง
(๐ โ N
โง ๐ โ
N โง โ
โ N)) โ ((๐ ยทN ๐)
ยทN โ) = (๐ ยทN (๐
ยทN โ))) |
87 | 63 | adantl 277 |
. . . . 5
โข ((((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โง
(๐ โ N
โง ๐ โ
N)) โ (๐
ยทN ๐) โ N) |
88 | 45, 45, 80, 85, 86, 81, 87 | caov4d 6058 |
. . . 4
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
((๐ฆ
ยทN ๐ฆ) ยทN (๐ค
ยทN ๐ข)) = ((๐ฆ ยทN ๐ค)
ยทN (๐ฆ ยทN ๐ข))) |
89 | 84, 88 | eqtr3d 2212 |
. . 3
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ข
โ N) โง (๐ค โ N โง ๐ฃ โ N)) โ
(๐ฆ
ยทN (๐ฆ ยทN (๐ค
ยทN ๐ข))) = ((๐ฆ ยทN ๐ค)
ยทN (๐ฆ ยทN ๐ข))) |
90 | 40, 89 | sylbir 135 |
. 2
โข (((๐ฅ โ N โง
๐ฆ โ N)
โง (๐ง โ
N โง ๐ค
โ N) โง (๐ฃ โ N โง ๐ข โ N)) โ
(๐ฆ
ยทN (๐ฆ ยทN (๐ค
ยทN ๐ข))) = ((๐ฆ ยทN ๐ค)
ยทN (๐ฆ ยทN ๐ข))) |
91 | 1, 2, 16, 17, 18, 19, 27, 31, 35, 79, 90 | ecovidi 6646 |
1
โข ((๐ด โ Q โง
๐ต โ Q
โง ๐ถ โ
Q) โ (๐ด
ยทQ (๐ต +Q ๐ถ)) = ((๐ด ยทQ ๐ต) +Q
(๐ด
ยทQ ๐ถ))) |