Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(mulGrpββfld) =
(mulGrpββfld) |
2 | | fzofi 13885 |
. . . 4
β’ (0..^2)
β Fin |
3 | 2 | a1i 11 |
. . 3
β’ (π β (0..^2) β
Fin) |
4 | | 2nn 12231 |
. . . . 5
β’ 2 β
β |
5 | | lbfzo0 13618 |
. . . . 5
β’ (0 β
(0..^2) β 2 β β) |
6 | 4, 5 | mpbir 230 |
. . . 4
β’ 0 β
(0..^2) |
7 | | ne0i 4295 |
. . . 4
β’ (0 β
(0..^2) β (0..^2) β β
) |
8 | 6, 7 | mp1i 13 |
. . 3
β’ (π β (0..^2) β
β
) |
9 | | amgmw2d.0 |
. . . . . 6
β’ (π β π΄ β
β+) |
10 | | amgmw2d.2 |
. . . . . 6
β’ (π β π΅ β
β+) |
11 | 9, 10 | s2cld 14766 |
. . . . 5
β’ (π β β¨βπ΄π΅ββ© β Word
β+) |
12 | | wrdf 14413 |
. . . . 5
β’
(β¨βπ΄π΅ββ© β Word
β+ β β¨βπ΄π΅ββ©:(0..^(β―ββ¨βπ΄π΅ββ©))βΆβ+) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (π β β¨βπ΄π΅ββ©:(0..^(β―ββ¨βπ΄π΅ββ©))βΆβ+) |
14 | | s2len 14784 |
. . . . . 6
β’
(β―ββ¨βπ΄π΅ββ©) = 2 |
15 | 14 | oveq2i 7369 |
. . . . 5
β’
(0..^(β―ββ¨βπ΄π΅ββ©)) = (0..^2) |
16 | 15 | feq2i 6661 |
. . . 4
β’
(β¨βπ΄π΅ββ©:(0..^(β―ββ¨βπ΄π΅ββ©))βΆβ+ β
β¨βπ΄π΅ββ©:(0..^2)βΆβ+) |
17 | 13, 16 | sylib 217 |
. . 3
β’ (π β β¨βπ΄π΅ββ©:(0..^2)βΆβ+) |
18 | | amgmw2d.1 |
. . . . . 6
β’ (π β π β
β+) |
19 | | amgmw2d.3 |
. . . . . 6
β’ (π β π β
β+) |
20 | 18, 19 | s2cld 14766 |
. . . . 5
β’ (π β β¨βππββ© β Word
β+) |
21 | | wrdf 14413 |
. . . . 5
β’
(β¨βππββ© β Word
β+ β β¨βππββ©:(0..^(β―ββ¨βππββ©))βΆβ+) |
22 | 20, 21 | syl 17 |
. . . 4
β’ (π β β¨βππββ©:(0..^(β―ββ¨βππββ©))βΆβ+) |
23 | | s2len 14784 |
. . . . . 6
β’
(β―ββ¨βππββ©) = 2 |
24 | 23 | oveq2i 7369 |
. . . . 5
β’
(0..^(β―ββ¨βππββ©)) = (0..^2) |
25 | 24 | feq2i 6661 |
. . . 4
β’
(β¨βππββ©:(0..^(β―ββ¨βππββ©))βΆβ+ β
β¨βππββ©:(0..^2)βΆβ+) |
26 | 22, 25 | sylib 217 |
. . 3
β’ (π β β¨βππββ©:(0..^2)βΆβ+) |
27 | | cnring 20835 |
. . . . . 6
β’
βfld β Ring |
28 | | ringmnd 19979 |
. . . . . 6
β’
(βfld β Ring β βfld β
Mnd) |
29 | 27, 28 | mp1i 13 |
. . . . 5
β’ (π β βfld
β Mnd) |
30 | 18 | rpcnd 12964 |
. . . . 5
β’ (π β π β β) |
31 | 19 | rpcnd 12964 |
. . . . 5
β’ (π β π β β) |
32 | | cnfldbas 20816 |
. . . . . 6
β’ β =
(Baseββfld) |
33 | | cnfldadd 20817 |
. . . . . 6
β’ + =
(+gββfld) |
34 | 32, 33 | gsumws2 18657 |
. . . . 5
β’
((βfld β Mnd β§ π β β β§ π β β) β
(βfld Ξ£g β¨βππββ©) = (π + π)) |
35 | 29, 30, 31, 34 | syl3anc 1372 |
. . . 4
β’ (π β (βfld
Ξ£g β¨βππββ©) = (π + π)) |
36 | | amgmw2d.4 |
. . . 4
β’ (π β (π + π) = 1) |
37 | 35, 36 | eqtrd 2773 |
. . 3
β’ (π β (βfld
Ξ£g β¨βππββ©) = 1) |
38 | 1, 3, 8, 17, 26, 37 | amgmwlem 47335 |
. 2
β’ (π β
((mulGrpββfld) Ξ£g
(β¨βπ΄π΅ββ©
βf βπβ¨βππββ©)) β€ (βfld
Ξ£g (β¨βπ΄π΅ββ© βf Β·
β¨βππββ©))) |
39 | 9, 10 | jca 513 |
. . . . 5
β’ (π β (π΄ β β+ β§ π΅ β
β+)) |
40 | 18, 19 | jca 513 |
. . . . 5
β’ (π β (π β β+ β§ π β
β+)) |
41 | | ofs2 14862 |
. . . . 5
β’ (((π΄ β β+
β§ π΅ β
β+) β§ (π β β+ β§ π β β+))
β (β¨βπ΄π΅ββ©
βf βπβ¨βππββ©) = β¨β(π΄βππ)(π΅βππ)ββ©) |
42 | 39, 40, 41 | syl2anc 585 |
. . . 4
β’ (π β (β¨βπ΄π΅ββ© βf
βπβ¨βππββ©) = β¨β(π΄βππ)(π΅βππ)ββ©) |
43 | 42 | oveq2d 7374 |
. . 3
β’ (π β
((mulGrpββfld) Ξ£g
(β¨βπ΄π΅ββ©
βf βπβ¨βππββ©)) =
((mulGrpββfld) Ξ£g
β¨β(π΄βππ)(π΅βππ)ββ©)) |
44 | 1 | ringmgp 19975 |
. . . . 5
β’
(βfld β Ring β
(mulGrpββfld) β Mnd) |
45 | 27, 44 | mp1i 13 |
. . . 4
β’ (π β
(mulGrpββfld) β Mnd) |
46 | 18 | rpred 12962 |
. . . . . 6
β’ (π β π β β) |
47 | 9, 46 | rpcxpcld 26103 |
. . . . 5
β’ (π β (π΄βππ) β
β+) |
48 | 47 | rpcnd 12964 |
. . . 4
β’ (π β (π΄βππ) β β) |
49 | 19 | rpred 12962 |
. . . . . 6
β’ (π β π β β) |
50 | 10, 49 | rpcxpcld 26103 |
. . . . 5
β’ (π β (π΅βππ) β
β+) |
51 | 50 | rpcnd 12964 |
. . . 4
β’ (π β (π΅βππ) β β) |
52 | 1, 32 | mgpbas 19907 |
. . . . 5
β’ β =
(Baseβ(mulGrpββfld)) |
53 | | cnfldmul 20818 |
. . . . . 6
β’ Β·
= (.rββfld) |
54 | 1, 53 | mgpplusg 19905 |
. . . . 5
β’ Β·
= (+gβ(mulGrpββfld)) |
55 | 52, 54 | gsumws2 18657 |
. . . 4
β’
(((mulGrpββfld) β Mnd β§ (π΄βππ) β β β§ (π΅βππ) β β) β
((mulGrpββfld) Ξ£g
β¨β(π΄βππ)(π΅βππ)ββ©) = ((π΄βππ) Β· (π΅βππ))) |
56 | 45, 48, 51, 55 | syl3anc 1372 |
. . 3
β’ (π β
((mulGrpββfld) Ξ£g
β¨β(π΄βππ)(π΅βππ)ββ©) = ((π΄βππ) Β· (π΅βππ))) |
57 | 43, 56 | eqtrd 2773 |
. 2
β’ (π β
((mulGrpββfld) Ξ£g
(β¨βπ΄π΅ββ©
βf βπβ¨βππββ©)) = ((π΄βππ) Β· (π΅βππ))) |
58 | | ofs2 14862 |
. . . . 5
β’ (((π΄ β β+
β§ π΅ β
β+) β§ (π β β+ β§ π β β+))
β (β¨βπ΄π΅ββ©
βf Β· β¨βππββ©) = β¨β(π΄ Β· π)(π΅ Β· π)ββ©) |
59 | 39, 40, 58 | syl2anc 585 |
. . . 4
β’ (π β (β¨βπ΄π΅ββ© βf Β·
β¨βππββ©) =
β¨β(π΄ Β·
π)(π΅ Β· π)ββ©) |
60 | 59 | oveq2d 7374 |
. . 3
β’ (π β (βfld
Ξ£g (β¨βπ΄π΅ββ© βf Β·
β¨βππββ©)) =
(βfld Ξ£g β¨β(π΄ Β· π)(π΅ Β· π)ββ©)) |
61 | 9, 18 | rpmulcld 12978 |
. . . . 5
β’ (π β (π΄ Β· π) β
β+) |
62 | 61 | rpcnd 12964 |
. . . 4
β’ (π β (π΄ Β· π) β β) |
63 | 10, 19 | rpmulcld 12978 |
. . . . 5
β’ (π β (π΅ Β· π) β
β+) |
64 | 63 | rpcnd 12964 |
. . . 4
β’ (π β (π΅ Β· π) β β) |
65 | 32, 33 | gsumws2 18657 |
. . . 4
β’
((βfld β Mnd β§ (π΄ Β· π) β β β§ (π΅ Β· π) β β) β
(βfld Ξ£g β¨β(π΄ Β· π)(π΅ Β· π)ββ©) = ((π΄ Β· π) + (π΅ Β· π))) |
66 | 29, 62, 64, 65 | syl3anc 1372 |
. . 3
β’ (π β (βfld
Ξ£g β¨β(π΄ Β· π)(π΅ Β· π)ββ©) = ((π΄ Β· π) + (π΅ Β· π))) |
67 | 60, 66 | eqtrd 2773 |
. 2
β’ (π β (βfld
Ξ£g (β¨βπ΄π΅ββ© βf Β·
β¨βππββ©)) = ((π΄ Β· π) + (π΅ Β· π))) |
68 | 38, 57, 67 | 3brtr3d 5137 |
1
β’ (π β ((π΄βππ) Β· (π΅βππ)) β€ ((π΄ Β· π) + (π΅ Β· π))) |