| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simp1 1136 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β π β LMod) |
| 2 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Scalarβπ) =
(Scalarβπ) |
| 3 | | eqid 2732 |
. . . . . . . . . . 11
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
| 4 | | eqid 2732 |
. . . . . . . . . . 11
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
| 5 | 2, 3, 4 | lmod1cl 20498 |
. . . . . . . . . 10
β’ (π β LMod β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
| 6 | 1, 5 | syl 17 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π β§ π β π) β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
| 7 | | eqid 2732 |
. . . . . . . . . 10
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
| 8 | 2, 3, 7 | lmodacl 20482 |
. . . . . . . . 9
β’ ((π β LMod β§
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ)) β§
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
| 9 | 1, 6, 6, 8 | syl3anc 1371 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β
((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
| 10 | | simp2 1137 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β π β π) |
| 11 | | simp3 1138 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β π β π) |
| 12 | | lmodcom.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
| 13 | | lmodcom.a |
. . . . . . . . 9
β’ + =
(+gβπ) |
| 14 | | eqid 2732 |
. . . . . . . . 9
β’ (
Β·π βπ) = ( Β·π
βπ) |
| 15 | 12, 13, 2, 14, 3 | lmodvsdi 20494 |
. . . . . . . 8
β’ ((π β 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 | 1, 9, 10, 11, 15 | syl13anc 1372 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)(π + π)) =
((((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) +
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π))) |
| 17 | 12, 13 | lmodvacl 20485 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
| 18 | 12, 13, 2, 14, 3, 7 | lmodvsdir 20495 |
. . . . . . . 8
β’ ((π β LMod β§
((1rβ(Scalarβπ)) β (Baseβ(Scalarβπ)) β§
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ)) β§ (π + π) β π)) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)(π + π)) =
(((1rβ(Scalarβπ))( Β·π
βπ)(π + π)) +
((1rβ(Scalarβπ))( Β·π
βπ)(π + π)))) |
| 19 | 1, 6, 6, 17, 18 | syl13anc 1372 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)(π + π)) =
(((1rβ(Scalarβπ))( Β·π
βπ)(π + π)) +
((1rβ(Scalarβπ))( Β·π
βπ)(π + π)))) |
| 20 | 16, 19 | eqtr3d 2774 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β
((((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) +
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π)) =
(((1rβ(Scalarβπ))( Β·π
βπ)(π + π)) +
((1rβ(Scalarβπ))( Β·π
βπ)(π + π)))) |
| 21 | 12, 13, 2, 14, 3, 7 | lmodvsdir 20495 |
. . . . . . . . 9
β’ ((π β LMod β§
((1rβ(Scalarβπ)) β (Baseβ(Scalarβπ)) β§
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ)) β§ π β π)) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) =
(((1rβ(Scalarβπ))( Β·π
βπ)π) +
((1rβ(Scalarβπ))( Β·π
βπ)π))) |
| 22 | 1, 6, 6, 10, 21 | syl13anc 1372 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) =
(((1rβ(Scalarβπ))( Β·π
βπ)π) +
((1rβ(Scalarβπ))( Β·π
βπ)π))) |
| 23 | 12, 2, 14, 4 | lmodvs1 20499 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β
((1rβ(Scalarβπ))( Β·π
βπ)π) = π) |
| 24 | 1, 10, 23 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π β§ π β π) β
((1rβ(Scalarβπ))( Β·π
βπ)π) = π) |
| 25 | 24, 24 | oveq12d 7426 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))( Β·π
βπ)π) +
((1rβ(Scalarβπ))( Β·π
βπ)π)) = (π + π)) |
| 26 | 22, 25 | eqtrd 2772 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) = (π + π)) |
| 27 | 12, 13, 2, 14, 3, 7 | lmodvsdir 20495 |
. . . . . . . . 9
β’ ((π β LMod β§
((1rβ(Scalarβπ)) β (Baseβ(Scalarβπ)) β§
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ)) β§ π β π)) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) =
(((1rβ(Scalarβπ))( Β·π
βπ)π) +
((1rβ(Scalarβπ))( Β·π
βπ)π))) |
| 28 | 1, 6, 6, 11, 27 | syl13anc 1372 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) =
(((1rβ(Scalarβπ))( Β·π
βπ)π) +
((1rβ(Scalarβπ))( Β·π
βπ)π))) |
| 29 | 12, 2, 14, 4 | lmodvs1 20499 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π) β
((1rβ(Scalarβπ))( Β·π
βπ)π) = π) |
| 30 | 1, 11, 29 | syl2anc 584 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π β§ π β π) β
((1rβ(Scalarβπ))( Β·π
βπ)π) = π) |
| 31 | 30, 30 | oveq12d 7426 |
. . . . . . . 8
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))( Β·π
βπ)π) +
((1rβ(Scalarβπ))( Β·π
βπ)π)) = (π + π)) |
| 32 | 28, 31 | eqtrd 2772 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) = (π + π)) |
| 33 | 26, 32 | oveq12d 7426 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β
((((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π) +
(((1rβ(Scalarβπ))(+gβ(Scalarβπ))(1rβ(Scalarβπ)))(
Β·π βπ)π)) = ((π + π) + (π + π))) |
| 34 | 12, 2, 14, 4 | lmodvs1 20499 |
. . . . . . . 8
β’ ((π β LMod β§ (π + π) β π) β
((1rβ(Scalarβπ))( Β·π
βπ)(π + π)) = (π + π)) |
| 35 | 1, 17, 34 | syl2anc 584 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β
((1rβ(Scalarβπ))( Β·π
βπ)(π + π)) = (π + π)) |
| 36 | 35, 35 | oveq12d 7426 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β
(((1rβ(Scalarβπ))( Β·π
βπ)(π + π)) +
((1rβ(Scalarβπ))( Β·π
βπ)(π + π))) = ((π + π) + (π + π))) |
| 37 | 20, 33, 36 | 3eqtr3d 2780 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β ((π + π) + (π + π)) = ((π + π) + (π + π))) |
| 38 | 12, 13 | lmodvacl 20485 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
| 39 | 1, 10, 10, 38 | syl3anc 1371 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
| 40 | 12, 13 | lmodass 20486 |
. . . . . 6
β’ ((π β LMod β§ ((π + π) β π β§ π β π β§ π β π)) β (((π + π) + π) + π) = ((π + π) + (π + π))) |
| 41 | 1, 39, 11, 11, 40 | syl13anc 1372 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β (((π + π) + π) + π) = ((π + π) + (π + π))) |
| 42 | 12, 13 | lmodass 20486 |
. . . . . 6
β’ ((π β LMod β§ ((π + π) β π β§ π β π β§ π β π)) β (((π + π) + π) + π) = ((π + π) + (π + π))) |
| 43 | 1, 17, 10, 11, 42 | syl13anc 1372 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β (((π + π) + π) + π) = ((π + π) + (π + π))) |
| 44 | 37, 41, 43 | 3eqtr4d 2782 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β (((π + π) + π) + π) = (((π + π) + π) + π)) |
| 45 | | lmodgrp 20477 |
. . . . . 6
β’ (π β LMod β π β Grp) |
| 46 | 1, 45 | syl 17 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β π β Grp) |
| 47 | 12, 13 | lmodvacl 20485 |
. . . . . 6
β’ ((π β LMod β§ (π + π) β π β§ π β π) β ((π + π) + π) β π) |
| 48 | 1, 39, 11, 47 | syl3anc 1371 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β ((π + π) + π) β π) |
| 49 | 12, 13 | lmodvacl 20485 |
. . . . . 6
β’ ((π β LMod β§ (π + π) β π β§ π β π) β ((π + π) + π) β π) |
| 50 | 1, 17, 10, 49 | syl3anc 1371 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β ((π + π) + π) β π) |
| 51 | 12, 13 | grprcan 18857 |
. . . . 5
β’ ((π β Grp β§ (((π + π) + π) β π β§ ((π + π) + π) β π β§ π β π)) β ((((π + π) + π) + π) = (((π + π) + π) + π) β ((π + π) + π) = ((π + π) + π))) |
| 52 | 46, 48, 50, 11, 51 | syl13anc 1372 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β ((((π + π) + π) + π) = (((π + π) + π) + π) β ((π + π) + π) = ((π + π) + π))) |
| 53 | 44, 52 | mpbid 231 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β ((π + π) + π) = ((π + π) + π)) |
| 54 | 12, 13 | lmodass 20486 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β π β§ π β π)) β ((π + π) + π) = (π + (π + π))) |
| 55 | 1, 10, 10, 11, 54 | syl13anc 1372 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β ((π + π) + π) = (π + (π + π))) |
| 56 | 12, 13 | lmodass 20486 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β π β§ π β π)) β ((π + π) + π) = (π + (π + π))) |
| 57 | 1, 10, 11, 10, 56 | syl13anc 1372 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β ((π + π) + π) = (π + (π + π))) |
| 58 | 53, 55, 57 | 3eqtr3d 2780 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β (π + (π + π)) = (π + (π + π))) |
| 59 | 12, 13 | lmodvacl 20485 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
| 60 | 59 | 3com23 1126 |
. . 3
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) β π) |
| 61 | 12, 13 | lmodlcan 20487 |
. . 3
β’ ((π β LMod β§ ((π + π) β π β§ (π + π) β π β§ π β π)) β ((π + (π + π)) = (π + (π + π)) β (π + π) = (π + π))) |
| 62 | 1, 17, 60, 10, 61 | syl13anc 1372 |
. 2
β’ ((π β LMod β§ π β π β§ π β π) β ((π + (π + π)) = (π + (π + π)) β (π + π) = (π + π))) |
| 63 | 58, 62 | mpbid 231 |
1
β’ ((π β LMod β§ π β π β§ π β π) β (π + π) = (π + π)) |
