| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lmodcom.v |
β’ π = ( Base β π ) |
| 2 |
|
lmodcom.a |
β’ + = ( +g β π ) |
| 3 |
|
simp1 |
β’ ( ( π β LMod β§ π β π β§ π β π ) β π β LMod ) |
| 4 |
|
eqid |
β’ ( Scalar β π ) = ( Scalar β π ) |
| 5 |
|
eqid |
β’ ( Base β ( Scalar β π ) ) = ( Base β ( Scalar β π ) ) |
| 6 |
|
eqid |
β’ ( 1r β ( Scalar β π ) ) = ( 1r β ( Scalar β π ) ) |
| 7 |
4 5 6
|
lmod1cl |
β’ ( π β LMod β ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) ) |
| 8 |
3 7
|
syl |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) ) |
| 9 |
|
eqid |
β’ ( +g β ( Scalar β π ) ) = ( +g β ( Scalar β π ) ) |
| 10 |
4 5 9
|
lmodacl |
β’ ( ( π β LMod β§ ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) β§ ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) ) β ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) β ( Base β ( Scalar β π ) ) ) |
| 11 |
3 8 8 10
|
syl3anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) β ( Base β ( Scalar β π ) ) ) |
| 12 |
|
simp2 |
β’ ( ( π β LMod β§ π β π β§ π β π ) β π β π ) |
| 13 |
|
simp3 |
β’ ( ( π β LMod β§ π β π β§ π β π ) β π β π ) |
| 14 |
|
eqid |
β’ ( Β·π β π ) = ( Β·π β π ) |
| 15 |
1 2 4 14 5
|
lmodvsdi |
β’ ( ( π β LMod β§ ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) β ( Base β ( Scalar β π ) ) β§ π β π β§ π β π ) ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) ( π + π ) ) = ( ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) + ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) ) ) |
| 16 |
3 11 12 13 15
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) ( π + π ) ) = ( ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) + ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) ) ) |
| 17 |
1 2
|
lmodvacl |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( π + π ) β π ) |
| 18 |
1 2 4 14 5 9
|
lmodvsdir |
β’ ( ( π β LMod β§ ( ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) β§ ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) β§ ( π + π ) β π ) ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) ( π + π ) ) = ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) ) ) |
| 19 |
3 8 8 17 18
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) ( π + π ) ) = ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) ) ) |
| 20 |
16 19
|
eqtr3d |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) + ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) ) = ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) ) ) |
| 21 |
1 2 4 14 5 9
|
lmodvsdir |
β’ ( ( π β LMod β§ ( ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) β§ ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) β§ π β π ) ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) = ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) ) ) |
| 22 |
3 8 8 12 21
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) = ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) ) ) |
| 23 |
1 4 14 6
|
lmodvs1 |
β’ ( ( π β LMod β§ π β π ) β ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) = π ) |
| 24 |
3 12 23
|
syl2anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) = π ) |
| 25 |
24 24
|
oveq12d |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) ) = ( π + π ) ) |
| 26 |
22 25
|
eqtrd |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) = ( π + π ) ) |
| 27 |
1 2 4 14 5 9
|
lmodvsdir |
β’ ( ( π β LMod β§ ( ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) β§ ( 1r β ( Scalar β π ) ) β ( Base β ( Scalar β π ) ) β§ π β π ) ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) = ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) ) ) |
| 28 |
3 8 8 13 27
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) = ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) ) ) |
| 29 |
1 4 14 6
|
lmodvs1 |
β’ ( ( π β LMod β§ π β π ) β ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) = π ) |
| 30 |
3 13 29
|
syl2anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) = π ) |
| 31 |
30 30
|
oveq12d |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) π ) ) = ( π + π ) ) |
| 32 |
28 31
|
eqtrd |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) = ( π + π ) ) |
| 33 |
26 32
|
oveq12d |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) + ( ( ( 1r β ( Scalar β π ) ) ( +g β ( Scalar β π ) ) ( 1r β ( Scalar β π ) ) ) ( Β·π β π ) π ) ) = ( ( π + π ) + ( π + π ) ) ) |
| 34 |
1 4 14 6
|
lmodvs1 |
β’ ( ( π β LMod β§ ( π + π ) β π ) β ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) = ( π + π ) ) |
| 35 |
3 17 34
|
syl2anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) = ( π + π ) ) |
| 36 |
35 35
|
oveq12d |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) + ( ( 1r β ( Scalar β π ) ) ( Β·π β π ) ( π + π ) ) ) = ( ( π + π ) + ( π + π ) ) ) |
| 37 |
20 33 36
|
3eqtr3d |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( π + π ) + ( π + π ) ) = ( ( π + π ) + ( π + π ) ) ) |
| 38 |
1 2
|
lmodvacl |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( π + π ) β π ) |
| 39 |
3 12 12 38
|
syl3anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( π + π ) β π ) |
| 40 |
1 2
|
lmodass |
β’ ( ( π β LMod β§ ( ( π + π ) β π β§ π β π β§ π β π ) ) β ( ( ( π + π ) + π ) + π ) = ( ( π + π ) + ( π + π ) ) ) |
| 41 |
3 39 13 13 40
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( π + π ) + π ) + π ) = ( ( π + π ) + ( π + π ) ) ) |
| 42 |
1 2
|
lmodass |
β’ ( ( π β LMod β§ ( ( π + π ) β π β§ π β π β§ π β π ) ) β ( ( ( π + π ) + π ) + π ) = ( ( π + π ) + ( π + π ) ) ) |
| 43 |
3 17 12 13 42
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( π + π ) + π ) + π ) = ( ( π + π ) + ( π + π ) ) ) |
| 44 |
37 41 43
|
3eqtr4d |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( π + π ) + π ) + π ) = ( ( ( π + π ) + π ) + π ) ) |
| 45 |
|
lmodgrp |
β’ ( π β LMod β π β Grp ) |
| 46 |
3 45
|
syl |
β’ ( ( π β LMod β§ π β π β§ π β π ) β π β Grp ) |
| 47 |
1 2
|
lmodvacl |
β’ ( ( π β LMod β§ ( π + π ) β π β§ π β π ) β ( ( π + π ) + π ) β π ) |
| 48 |
3 39 13 47
|
syl3anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( π + π ) + π ) β π ) |
| 49 |
1 2
|
lmodvacl |
β’ ( ( π β LMod β§ ( π + π ) β π β§ π β π ) β ( ( π + π ) + π ) β π ) |
| 50 |
3 17 12 49
|
syl3anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( π + π ) + π ) β π ) |
| 51 |
1 2
|
grprcan |
β’ ( ( π β Grp β§ ( ( ( π + π ) + π ) β π β§ ( ( π + π ) + π ) β π β§ π β π ) ) β ( ( ( ( π + π ) + π ) + π ) = ( ( ( π + π ) + π ) + π ) β ( ( π + π ) + π ) = ( ( π + π ) + π ) ) ) |
| 52 |
46 48 50 13 51
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( ( ( π + π ) + π ) + π ) = ( ( ( π + π ) + π ) + π ) β ( ( π + π ) + π ) = ( ( π + π ) + π ) ) ) |
| 53 |
44 52
|
mpbid |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( π + π ) + π ) = ( ( π + π ) + π ) ) |
| 54 |
1 2
|
lmodass |
β’ ( ( π β LMod β§ ( π β π β§ π β π β§ π β π ) ) β ( ( π + π ) + π ) = ( π + ( π + π ) ) ) |
| 55 |
3 12 12 13 54
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( π + π ) + π ) = ( π + ( π + π ) ) ) |
| 56 |
1 2
|
lmodass |
β’ ( ( π β LMod β§ ( π β π β§ π β π β§ π β π ) ) β ( ( π + π ) + π ) = ( π + ( π + π ) ) ) |
| 57 |
3 12 13 12 56
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( π + π ) + π ) = ( π + ( π + π ) ) ) |
| 58 |
53 55 57
|
3eqtr3d |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( π + ( π + π ) ) = ( π + ( π + π ) ) ) |
| 59 |
1 2
|
lmodvacl |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( π + π ) β π ) |
| 60 |
59
|
3com23 |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( π + π ) β π ) |
| 61 |
1 2
|
lmodlcan |
β’ ( ( π β LMod β§ ( ( π + π ) β π β§ ( π + π ) β π β§ π β π ) ) β ( ( π + ( π + π ) ) = ( π + ( π + π ) ) β ( π + π ) = ( π + π ) ) ) |
| 62 |
3 17 60 12 61
|
syl13anc |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( ( π + ( π + π ) ) = ( π + ( π + π ) ) β ( π + π ) = ( π + π ) ) ) |
| 63 |
58 62
|
mpbid |
β’ ( ( π β LMod β§ π β π β§ π β π ) β ( π + π ) = ( π + π ) ) |