Step | Hyp | Ref
| Expression |
1 | | 0cn 11207 |
. 2
β’ 0 β
β |
2 | | cnlmod.w |
. . . . . 6
β’ π = ({β¨(Baseβndx),
ββ©, β¨(+gβndx), + β©} βͺ
{β¨(Scalarβndx), βfldβ©, β¨(
Β·π βndx), Β·
β©}) |
3 | 2 | cnlmodlem1 25014 |
. . . . 5
β’
(Baseβπ) =
β |
4 | 3 | eqcomi 2735 |
. . . 4
β’ β =
(Baseβπ) |
5 | 4 | a1i 11 |
. . 3
β’ (0 β
β β β = (Baseβπ)) |
6 | 2 | cnlmodlem2 25015 |
. . . . 5
β’
(+gβπ) = + |
7 | 6 | eqcomi 2735 |
. . . 4
β’ + =
(+gβπ) |
8 | 7 | a1i 11 |
. . 3
β’ (0 β
β β + = (+gβπ)) |
9 | | addcl 11191 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
10 | 9 | 3adant1 1127 |
. . 3
β’ ((0
β β β§ π₯
β β β§ π¦
β β) β (π₯ +
π¦) β
β) |
11 | | addass 11196 |
. . . 4
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
12 | 11 | adantl 481 |
. . 3
β’ ((0
β β β§ (π₯
β β β§ π¦
β β β§ π§
β β)) β ((π₯
+ π¦) + π§) = (π₯ + (π¦ + π§))) |
13 | | id 22 |
. . 3
β’ (0 β
β β 0 β β) |
14 | | addlid 11398 |
. . . 4
β’ (π₯ β β β (0 +
π₯) = π₯) |
15 | 14 | adantl 481 |
. . 3
β’ ((0
β β β§ π₯
β β) β (0 + π₯) = π₯) |
16 | | negcl 11461 |
. . . 4
β’ (π₯ β β β -π₯ β
β) |
17 | 16 | adantl 481 |
. . 3
β’ ((0
β β β§ π₯
β β) β -π₯
β β) |
18 | | id 22 |
. . . . . 6
β’ (π₯ β β β π₯ β
β) |
19 | 16, 18 | addcomd 11417 |
. . . . 5
β’ (π₯ β β β (-π₯ + π₯) = (π₯ + -π₯)) |
20 | 19 | adantl 481 |
. . . 4
β’ ((0
β β β§ π₯
β β) β (-π₯
+ π₯) = (π₯ + -π₯)) |
21 | | negid 11508 |
. . . . 5
β’ (π₯ β β β (π₯ + -π₯) = 0) |
22 | 21 | adantl 481 |
. . . 4
β’ ((0
β β β§ π₯
β β) β (π₯ +
-π₯) = 0) |
23 | 20, 22 | eqtrd 2766 |
. . 3
β’ ((0
β β β§ π₯
β β) β (-π₯
+ π₯) = 0) |
24 | 5, 8, 10, 12, 13, 15, 17, 23 | isgrpd 18886 |
. 2
β’ (0 β
β β π β
Grp) |
25 | 4 | a1i 11 |
. . 3
β’ (π β Grp β β =
(Baseβπ)) |
26 | 7 | a1i 11 |
. . 3
β’ (π β Grp β + =
(+gβπ)) |
27 | 2 | cnlmodlem3 25016 |
. . . . 5
β’
(Scalarβπ) =
βfld |
28 | 27 | eqcomi 2735 |
. . . 4
β’
βfld = (Scalarβπ) |
29 | 28 | a1i 11 |
. . 3
β’ (π β Grp β
βfld = (Scalarβπ)) |
30 | 2 | cnlmod4 25017 |
. . . . 5
β’ (
Β·π βπ) = Β· |
31 | 30 | eqcomi 2735 |
. . . 4
β’ Β·
= ( Β·π βπ) |
32 | 31 | a1i 11 |
. . 3
β’ (π β Grp β Β· = (
Β·π βπ)) |
33 | | cnfldbas 21240 |
. . . 4
β’ β =
(Baseββfld) |
34 | 33 | a1i 11 |
. . 3
β’ (π β Grp β β =
(Baseββfld)) |
35 | | cnfldadd 21242 |
. . . 4
β’ + =
(+gββfld) |
36 | 35 | a1i 11 |
. . 3
β’ (π β Grp β + =
(+gββfld)) |
37 | | cnfldmul 21244 |
. . . 4
β’ Β·
= (.rββfld) |
38 | 37 | a1i 11 |
. . 3
β’ (π β Grp β Β· =
(.rββfld)) |
39 | | cnfld1 21278 |
. . . 4
β’ 1 =
(1rββfld) |
40 | 39 | a1i 11 |
. . 3
β’ (π β Grp β 1 =
(1rββfld)) |
41 | | cnring 21275 |
. . . 4
β’
βfld β Ring |
42 | 41 | a1i 11 |
. . 3
β’ (π β Grp β
βfld β Ring) |
43 | | id 22 |
. . 3
β’ (π β Grp β π β Grp) |
44 | | mulcl 11193 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
45 | 44 | 3adant1 1127 |
. . 3
β’ ((π β Grp β§ π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
46 | | adddi 11198 |
. . . 4
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) |
47 | 46 | adantl 481 |
. . 3
β’ ((π β Grp β§ (π₯ β β β§ π¦ β β β§ π§ β β)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) |
48 | | adddir 11206 |
. . . 4
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
49 | 48 | adantl 481 |
. . 3
β’ ((π β Grp β§ (π₯ β β β§ π¦ β β β§ π§ β β)) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
50 | | mulass 11197 |
. . . 4
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) |
51 | 50 | adantl 481 |
. . 3
β’ ((π β Grp β§ (π₯ β β β§ π¦ β β β§ π§ β β)) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) |
52 | | mullid 11214 |
. . . 4
β’ (π₯ β β β (1
Β· π₯) = π₯) |
53 | 52 | adantl 481 |
. . 3
β’ ((π β Grp β§ π₯ β β) β (1
Β· π₯) = π₯) |
54 | 25, 26, 29, 32, 34, 36, 38, 40, 42, 43, 45, 47, 49, 51, 53 | islmodd 20710 |
. 2
β’ (π β Grp β π β LMod) |
55 | 1, 24, 54 | mp2b 10 |
1
β’ π β LMod |