Step | Hyp | Ref
| Expression |
1 | | 0cn 11206 |
. 2
β’ 0 β
β |
2 | | cnlmod.w |
. . . . . 6
β’ π = ({β¨(Baseβndx),
ββ©, β¨(+gβndx), + β©} βͺ
{β¨(Scalarβndx), βfldβ©, β¨(
Β·π βndx), Β·
β©}) |
3 | 2 | cnlmodlem1 24652 |
. . . . 5
β’
(Baseβπ) =
β |
4 | 3 | eqcomi 2742 |
. . . 4
β’ β =
(Baseβπ) |
5 | 4 | a1i 11 |
. . 3
β’ (0 β
β β β = (Baseβπ)) |
6 | 2 | cnlmodlem2 24653 |
. . . . 5
β’
(+gβπ) = + |
7 | 6 | eqcomi 2742 |
. . . 4
β’ + =
(+gβπ) |
8 | 7 | a1i 11 |
. . 3
β’ (0 β
β β + = (+gβπ)) |
9 | | addcl 11192 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
10 | 9 | 3adant1 1131 |
. . 3
β’ ((0
β β β§ π₯
β β β§ π¦
β β) β (π₯ +
π¦) β
β) |
11 | | addass 11197 |
. . . 4
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
12 | 11 | adantl 483 |
. . 3
β’ ((0
β β β§ (π₯
β β β§ π¦
β β β§ π§
β β)) β ((π₯
+ π¦) + π§) = (π₯ + (π¦ + π§))) |
13 | | id 22 |
. . 3
β’ (0 β
β β 0 β β) |
14 | | addlid 11397 |
. . . 4
β’ (π₯ β β β (0 +
π₯) = π₯) |
15 | 14 | adantl 483 |
. . 3
β’ ((0
β β β§ π₯
β β) β (0 + π₯) = π₯) |
16 | | negcl 11460 |
. . . 4
β’ (π₯ β β β -π₯ β
β) |
17 | 16 | adantl 483 |
. . 3
β’ ((0
β β β§ π₯
β β) β -π₯
β β) |
18 | | id 22 |
. . . . . 6
β’ (π₯ β β β π₯ β
β) |
19 | 16, 18 | addcomd 11416 |
. . . . 5
β’ (π₯ β β β (-π₯ + π₯) = (π₯ + -π₯)) |
20 | 19 | adantl 483 |
. . . 4
β’ ((0
β β β§ π₯
β β) β (-π₯
+ π₯) = (π₯ + -π₯)) |
21 | | negid 11507 |
. . . . 5
β’ (π₯ β β β (π₯ + -π₯) = 0) |
22 | 21 | adantl 483 |
. . . 4
β’ ((0
β β β§ π₯
β β) β (π₯ +
-π₯) = 0) |
23 | 20, 22 | eqtrd 2773 |
. . 3
β’ ((0
β β β§ π₯
β β) β (-π₯
+ π₯) = 0) |
24 | 5, 8, 10, 12, 13, 15, 17, 23 | isgrpd 18844 |
. 2
β’ (0 β
β β π β
Grp) |
25 | 4 | a1i 11 |
. . 3
β’ (π β Grp β β =
(Baseβπ)) |
26 | 7 | a1i 11 |
. . 3
β’ (π β Grp β + =
(+gβπ)) |
27 | 2 | cnlmodlem3 24654 |
. . . . 5
β’
(Scalarβπ) =
βfld |
28 | 27 | eqcomi 2742 |
. . . 4
β’
βfld = (Scalarβπ) |
29 | 28 | a1i 11 |
. . 3
β’ (π β Grp β
βfld = (Scalarβπ)) |
30 | 2 | cnlmod4 24655 |
. . . . 5
β’ (
Β·π βπ) = Β· |
31 | 30 | eqcomi 2742 |
. . . 4
β’ Β·
= ( Β·π βπ) |
32 | 31 | a1i 11 |
. . 3
β’ (π β Grp β Β· = (
Β·π βπ)) |
33 | | cnfldbas 20948 |
. . . 4
β’ β =
(Baseββfld) |
34 | 33 | a1i 11 |
. . 3
β’ (π β Grp β β =
(Baseββfld)) |
35 | | cnfldadd 20949 |
. . . 4
β’ + =
(+gββfld) |
36 | 35 | a1i 11 |
. . 3
β’ (π β Grp β + =
(+gββfld)) |
37 | | cnfldmul 20950 |
. . . 4
β’ Β·
= (.rββfld) |
38 | 37 | a1i 11 |
. . 3
β’ (π β Grp β Β· =
(.rββfld)) |
39 | | cnfld1 20970 |
. . . 4
β’ 1 =
(1rββfld) |
40 | 39 | a1i 11 |
. . 3
β’ (π β Grp β 1 =
(1rββfld)) |
41 | | cnring 20967 |
. . . 4
β’
βfld β Ring |
42 | 41 | a1i 11 |
. . 3
β’ (π β Grp β
βfld β Ring) |
43 | | id 22 |
. . 3
β’ (π β Grp β π β Grp) |
44 | | mulcl 11194 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
45 | 44 | 3adant1 1131 |
. . 3
β’ ((π β Grp β§ π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
46 | | adddi 11199 |
. . . 4
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) |
47 | 46 | adantl 483 |
. . 3
β’ ((π β Grp β§ (π₯ β β β§ π¦ β β β§ π§ β β)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) |
48 | | adddir 11205 |
. . . 4
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
49 | 48 | adantl 483 |
. . 3
β’ ((π β Grp β§ (π₯ β β β§ π¦ β β β§ π§ β β)) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
50 | | mulass 11198 |
. . . 4
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) |
51 | 50 | adantl 483 |
. . 3
β’ ((π β Grp β§ (π₯ β β β§ π¦ β β β§ π§ β β)) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) |
52 | | mullid 11213 |
. . . 4
β’ (π₯ β β β (1
Β· π₯) = π₯) |
53 | 52 | adantl 483 |
. . 3
β’ ((π β Grp β§ π₯ β β) β (1
Β· π₯) = π₯) |
54 | 25, 26, 29, 32, 34, 36, 38, 40, 42, 43, 45, 47, 49, 51, 53 | islmodd 20477 |
. 2
β’ (π β Grp β π β LMod) |
55 | 1, 24, 54 | mp2b 10 |
1
β’ π β LMod |