Step | Hyp | Ref
| Expression |
1 | | islmodd.l |
. 2
β’ (π β π β Grp) |
2 | | islmodd.f |
. . 3
β’ (π β πΉ = (Scalarβπ)) |
3 | | islmodd.r |
. . 3
β’ (π β πΉ β Ring) |
4 | 2, 3 | eqeltrrd 2839 |
. 2
β’ (π β (Scalarβπ) β Ring) |
5 | | islmodd.w |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΅ β§ π¦ β π) β (π₯ Β· π¦) β π) |
6 | 5 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π)) β (π₯ Β· π¦) β π) |
7 | 6 | ralrimivva 3198 |
. . . . . . . . 9
β’ (π β βπ₯ β π΅ βπ¦ β π (π₯ Β· π¦) β π) |
8 | | oveq1 7369 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ Β· π¦) = (π Β· π¦)) |
9 | 8 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π₯ Β· π¦) β π β (π Β· π¦) β π)) |
10 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π¦ = π€ β (π Β· π¦) = (π Β· π€)) |
11 | 10 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π¦ = π€ β ((π Β· π¦) β π β (π Β· π€) β π)) |
12 | 9, 11 | rspc2v 3593 |
. . . . . . . . . 10
β’ ((π β π΅ β§ π€ β π) β (βπ₯ β π΅ βπ¦ β π (π₯ Β· π¦) β π β (π Β· π€) β π)) |
13 | 12 | ad2ant2l 745 |
. . . . . . . . 9
β’ (((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π)) β (βπ₯ β π΅ βπ¦ β π (π₯ Β· π¦) β π β (π Β· π€) β π)) |
14 | 7, 13 | mpan9 508 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β (π Β· π€) β π) |
15 | | islmodd.c |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β§ π¦ β π β§ π§ β π)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) |
16 | 15 | ralrimivvva 3201 |
. . . . . . . . 9
β’ (π β βπ₯ β π΅ βπ¦ β π βπ§ β π (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) |
17 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (π₯ Β· (π¦ + π§)) = (π Β· (π¦ + π§))) |
18 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β (π₯ Β· π§) = (π Β· π§)) |
19 | 8, 18 | oveq12d 7380 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β ((π₯ Β· π¦) + (π₯ Β· π§)) = ((π Β· π¦) + (π Β· π§))) |
20 | 17, 19 | eqeq12d 2753 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β (π Β· (π¦ + π§)) = ((π Β· π¦) + (π Β· π§)))) |
21 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π€ β (π¦ + π§) = (π€ + π§)) |
22 | 21 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π¦ = π€ β (π Β· (π¦ + π§)) = (π Β· (π€ + π§))) |
23 | 10 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (π¦ = π€ β ((π Β· π¦) + (π Β· π§)) = ((π Β· π€) + (π Β· π§))) |
24 | 22, 23 | eqeq12d 2753 |
. . . . . . . . . . . . 13
β’ (π¦ = π€ β ((π Β· (π¦ + π§)) = ((π Β· π¦) + (π Β· π§)) β (π Β· (π€ + π§)) = ((π Β· π€) + (π Β· π§)))) |
25 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π§ = π’ β (π€ + π§) = (π€ + π’)) |
26 | 25 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π§ = π’ β (π Β· (π€ + π§)) = (π Β· (π€ + π’))) |
27 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
β’ (π§ = π’ β (π Β· π§) = (π Β· π’)) |
28 | 27 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π§ = π’ β ((π Β· π€) + (π Β· π§)) = ((π Β· π€) + (π Β· π’))) |
29 | 26, 28 | eqeq12d 2753 |
. . . . . . . . . . . . 13
β’ (π§ = π’ β ((π Β· (π€ + π§)) = ((π Β· π€) + (π Β· π§)) β (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)))) |
30 | 20, 24, 29 | rspc3v 3596 |
. . . . . . . . . . . 12
β’ ((π β π΅ β§ π€ β π β§ π’ β π) β (βπ₯ β π΅ βπ¦ β π βπ§ β π (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)))) |
31 | 30 | 3com23 1127 |
. . . . . . . . . . 11
β’ ((π β π΅ β§ π’ β π β§ π€ β π) β (βπ₯ β π΅ βπ¦ β π βπ§ β π (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)))) |
32 | 31 | 3expb 1121 |
. . . . . . . . . 10
β’ ((π β π΅ β§ (π’ β π β§ π€ β π)) β (βπ₯ β π΅ βπ¦ β π βπ§ β π (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)))) |
33 | 32 | adantll 713 |
. . . . . . . . 9
β’ (((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π)) β (βπ₯ β π΅ βπ¦ β π βπ§ β π (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)))) |
34 | 16, 33 | mpan9 508 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’))) |
35 | | simpll 766 |
. . . . . . . . . 10
β’ (((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π)) β π₯ β π΅) |
36 | | islmodd.d |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π)) β ((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
37 | 36 | 3exp2 1355 |
. . . . . . . . . . . 12
β’ (π β (π₯ β π΅ β (π¦ β π΅ β (π§ β π β ((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§)))))) |
38 | 37 | imp43 429 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π)) β ((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
39 | 38 | ralrimivva 3198 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π ((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
40 | 35, 39 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β βπ¦ β π΅ βπ§ β π ((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
41 | | simprlr 779 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β π β π΅) |
42 | | simprrr 781 |
. . . . . . . . . 10
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β π€ β π) |
43 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π¦ = π β (π₯ ⨣ π¦) = (π₯ ⨣ π)) |
44 | 43 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π¦ = π β ((π₯ ⨣ π¦) Β· π§) = ((π₯ ⨣ π) Β· π§)) |
45 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π¦ = π β (π¦ Β· π§) = (π Β· π§)) |
46 | 45 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π¦ = π β ((π₯ Β· π§) + (π¦ Β· π§)) = ((π₯ Β· π§) + (π Β· π§))) |
47 | 44, 46 | eqeq12d 2753 |
. . . . . . . . . . 11
β’ (π¦ = π β (((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§)) β ((π₯ ⨣ π) Β· π§) = ((π₯ Β· π§) + (π Β· π§)))) |
48 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π§ = π€ β ((π₯ ⨣ π) Β· π§) = ((π₯ ⨣ π) Β· π€)) |
49 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π§ = π€ β (π₯ Β· π§) = (π₯ Β· π€)) |
50 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π§ = π€ β (π Β· π§) = (π Β· π€)) |
51 | 49, 50 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π§ = π€ β ((π₯ Β· π§) + (π Β· π§)) = ((π₯ Β· π€) + (π Β· π€))) |
52 | 48, 51 | eqeq12d 2753 |
. . . . . . . . . . 11
β’ (π§ = π€ β (((π₯ ⨣ π) Β· π§) = ((π₯ Β· π§) + (π Β· π§)) β ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€)))) |
53 | 47, 52 | rspc2v 3593 |
. . . . . . . . . 10
β’ ((π β π΅ β§ π€ β π) β (βπ¦ β π΅ βπ§ β π ((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§)) β ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€)))) |
54 | 41, 42, 53 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β (βπ¦ β π΅ βπ§ β π ((π₯ ⨣ π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§)) β ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€)))) |
55 | 40, 54 | mpd 15 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) |
56 | 14, 34, 55 | 3jca 1129 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β ((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€)))) |
57 | | islmodd.e |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π)) β ((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) |
58 | 57 | 3exp2 1355 |
. . . . . . . . . . 11
β’ (π β (π₯ β π΅ β (π¦ β π΅ β (π§ β π β ((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§)))))) |
59 | 58 | imp43 429 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π΅) β§ (π¦ β π΅ β§ π§ β π)) β ((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) |
60 | 59 | ralrimivva 3198 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ βπ§ β π ((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) |
61 | 35, 60 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β βπ¦ β π΅ βπ§ β π ((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) |
62 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π¦ = π β (π₯ Γ π¦) = (π₯ Γ π)) |
63 | 62 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π¦ = π β ((π₯ Γ π¦) Β· π§) = ((π₯ Γ π) Β· π§)) |
64 | 45 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π¦ = π β (π₯ Β· (π¦ Β· π§)) = (π₯ Β· (π Β· π§))) |
65 | 63, 64 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (π¦ = π β (((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§)) β ((π₯ Γ π) Β· π§) = (π₯ Β· (π Β· π§)))) |
66 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π§ = π€ β ((π₯ Γ π) Β· π§) = ((π₯ Γ π) Β· π€)) |
67 | 50 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π§ = π€ β (π₯ Β· (π Β· π§)) = (π₯ Β· (π Β· π€))) |
68 | 66, 67 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (π§ = π€ β (((π₯ Γ π) Β· π§) = (π₯ Β· (π Β· π§)) β ((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)))) |
69 | 65, 68 | rspc2v 3593 |
. . . . . . . . 9
β’ ((π β π΅ β§ π€ β π) β (βπ¦ β π΅ βπ§ β π ((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§)) β ((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)))) |
70 | 41, 42, 69 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β (βπ¦ β π΅ βπ§ β π ((π₯ Γ π¦) Β· π§) = (π₯ Β· (π¦ Β· π§)) β ((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)))) |
71 | 61, 70 | mpd 15 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β ((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€))) |
72 | | islmodd.g |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β ( 1 Β· π₯) = π₯) |
73 | 72 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ₯ β π ( 1 Β· π₯) = π₯) |
74 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π₯ = π€ β ( 1 Β· π₯) = ( 1 Β· π€)) |
75 | | id 22 |
. . . . . . . . . . 11
β’ (π₯ = π€ β π₯ = π€) |
76 | 74, 75 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (π₯ = π€ β (( 1 Β· π₯) = π₯ β ( 1 Β· π€) = π€)) |
77 | 76 | rspcv 3580 |
. . . . . . . . 9
β’ (π€ β π β (βπ₯ β π ( 1 Β· π₯) = π₯ β ( 1 Β· π€) = π€)) |
78 | 77 | ad2antll 728 |
. . . . . . . 8
β’ (((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π)) β (βπ₯ β π ( 1 Β· π₯) = π₯ β ( 1 Β· π€) = π€)) |
79 | 73, 78 | mpan9 508 |
. . . . . . 7
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β ( 1 Β· π€) = π€) |
80 | 56, 71, 79 | jca32 517 |
. . . . . 6
β’ ((π β§ ((π₯ β π΅ β§ π β π΅) β§ (π’ β π β§ π€ β π))) β (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))) |
81 | 80 | anassrs 469 |
. . . . 5
β’ (((π β§ (π₯ β π΅ β§ π β π΅)) β§ (π’ β π β§ π€ β π)) β (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))) |
82 | 81 | ralrimivva 3198 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π β π΅)) β βπ’ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))) |
83 | 82 | ralrimivva 3198 |
. . 3
β’ (π β βπ₯ β π΅ βπ β π΅ βπ’ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))) |
84 | | islmodd.b |
. . . . 5
β’ (π β π΅ = (BaseβπΉ)) |
85 | 2 | fveq2d 6851 |
. . . . 5
β’ (π β (BaseβπΉ) =
(Baseβ(Scalarβπ))) |
86 | 84, 85 | eqtrd 2777 |
. . . 4
β’ (π β π΅ = (Baseβ(Scalarβπ))) |
87 | | islmodd.v |
. . . . . 6
β’ (π β π = (Baseβπ)) |
88 | | islmodd.s |
. . . . . . . . . . 11
β’ (π β Β· = (
Β·π βπ)) |
89 | 88 | oveqd 7379 |
. . . . . . . . . 10
β’ (π β (π Β· π€) = (π( Β·π
βπ)π€)) |
90 | 89, 87 | eleq12d 2832 |
. . . . . . . . 9
β’ (π β ((π Β· π€) β π β (π( Β·π
βπ)π€) β (Baseβπ))) |
91 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (π β π = π) |
92 | | islmodd.a |
. . . . . . . . . . . 12
β’ (π β + =
(+gβπ)) |
93 | 92 | oveqd 7379 |
. . . . . . . . . . 11
β’ (π β (π€ + π’) = (π€(+gβπ)π’)) |
94 | 88, 91, 93 | oveq123d 7383 |
. . . . . . . . . 10
β’ (π β (π Β· (π€ + π’)) = (π( Β·π
βπ)(π€(+gβπ)π’))) |
95 | 88 | oveqd 7379 |
. . . . . . . . . . 11
β’ (π β (π Β· π’) = (π( Β·π
βπ)π’)) |
96 | 92, 89, 95 | oveq123d 7383 |
. . . . . . . . . 10
β’ (π β ((π Β· π€) + (π Β· π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’))) |
97 | 94, 96 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π β ((π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)))) |
98 | | islmodd.p |
. . . . . . . . . . . . 13
β’ (π β ⨣ =
(+gβπΉ)) |
99 | 2 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π β (+gβπΉ) =
(+gβ(Scalarβπ))) |
100 | 98, 99 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β ⨣ =
(+gβ(Scalarβπ))) |
101 | 100 | oveqd 7379 |
. . . . . . . . . . 11
β’ (π β (π₯ ⨣ π) = (π₯(+gβ(Scalarβπ))π)) |
102 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (π β π€ = π€) |
103 | 88, 101, 102 | oveq123d 7383 |
. . . . . . . . . 10
β’ (π β ((π₯ ⨣ π) Β· π€) = ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€)) |
104 | 88 | oveqd 7379 |
. . . . . . . . . . 11
β’ (π β (π₯ Β· π€) = (π₯( Β·π
βπ)π€)) |
105 | 92, 104, 89 | oveq123d 7383 |
. . . . . . . . . 10
β’ (π β ((π₯ Β· π€) + (π Β· π€)) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))) |
106 | 103, 105 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π β (((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€)) β ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€)))) |
107 | 90, 97, 106 | 3anbi123d 1437 |
. . . . . . . 8
β’ (π β (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β ((π( Β·π
βπ)π€) β (Baseβπ) β§ (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)) β§ ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))))) |
108 | | islmodd.t |
. . . . . . . . . . . . 13
β’ (π β Γ =
(.rβπΉ)) |
109 | 2 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π β (.rβπΉ) =
(.rβ(Scalarβπ))) |
110 | 108, 109 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β Γ =
(.rβ(Scalarβπ))) |
111 | 110 | oveqd 7379 |
. . . . . . . . . . 11
β’ (π β (π₯ Γ π) = (π₯(.rβ(Scalarβπ))π)) |
112 | 88, 111, 102 | oveq123d 7383 |
. . . . . . . . . 10
β’ (π β ((π₯ Γ π) Β· π€) = ((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€)) |
113 | | eqidd 2738 |
. . . . . . . . . . 11
β’ (π β π₯ = π₯) |
114 | 88, 113, 89 | oveq123d 7383 |
. . . . . . . . . 10
β’ (π β (π₯ Β· (π Β· π€)) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€))) |
115 | 112, 114 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π β (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β ((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)))) |
116 | | islmodd.u |
. . . . . . . . . . . 12
β’ (π β 1 =
(1rβπΉ)) |
117 | 2 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π β (1rβπΉ) =
(1rβ(Scalarβπ))) |
118 | 116, 117 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β 1 =
(1rβ(Scalarβπ))) |
119 | 88, 118, 102 | oveq123d 7383 |
. . . . . . . . . 10
β’ (π β ( 1 Β· π€) = ((1rβ(Scalarβπ))(
Β·π βπ)π€)) |
120 | 119 | eqeq1d 2739 |
. . . . . . . . 9
β’ (π β (( 1 Β· π€) = π€ β
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€)) |
121 | 115, 120 | anbi12d 632 |
. . . . . . . 8
β’ (π β ((((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€) β (((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€))) |
122 | 107, 121 | anbi12d 632 |
. . . . . . 7
β’ (π β ((((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)) β (((π( Β·π
βπ)π€) β (Baseβπ) β§ (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)) β§ ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))) β§ (((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€)))) |
123 | 87, 122 | raleqbidv 3322 |
. . . . . 6
β’ (π β (βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)) β βπ€ β (Baseβπ)(((π( Β·π
βπ)π€) β (Baseβπ) β§ (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)) β§ ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))) β§ (((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€)))) |
124 | 87, 123 | raleqbidv 3322 |
. . . . 5
β’ (π β (βπ’ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)) β βπ’ β (Baseβπ)βπ€ β (Baseβπ)(((π( Β·π
βπ)π€) β (Baseβπ) β§ (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)) β§ ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))) β§ (((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€)))) |
125 | 86, 124 | raleqbidv 3322 |
. . . 4
β’ (π β (βπ β π΅ βπ’ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)) β βπ β (Baseβ(Scalarβπ))βπ’ β (Baseβπ)βπ€ β (Baseβπ)(((π( Β·π
βπ)π€) β (Baseβπ) β§ (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)) β§ ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))) β§ (((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€)))) |
126 | 86, 125 | raleqbidv 3322 |
. . 3
β’ (π β (βπ₯ β π΅ βπ β π΅ βπ’ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π’)) = ((π Β· π€) + (π Β· π’)) β§ ((π₯ ⨣ π) Β· π€) = ((π₯ Β· π€) + (π Β· π€))) β§ (((π₯ Γ π) Β· π€) = (π₯ Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)) β βπ₯ β (Baseβ(Scalarβπ))βπ β (Baseβ(Scalarβπ))βπ’ β (Baseβπ)βπ€ β (Baseβπ)(((π( Β·π
βπ)π€) β (Baseβπ) β§ (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)) β§ ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))) β§ (((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€)))) |
127 | 83, 126 | mpbid 231 |
. 2
β’ (π β βπ₯ β (Baseβ(Scalarβπ))βπ β (Baseβ(Scalarβπ))βπ’ β (Baseβπ)βπ€ β (Baseβπ)(((π( Β·π
βπ)π€) β (Baseβπ) β§ (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)) β§ ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))) β§ (((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€))) |
128 | | eqid 2737 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
129 | | eqid 2737 |
. . 3
β’
(+gβπ) = (+gβπ) |
130 | | eqid 2737 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
131 | | eqid 2737 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
132 | | eqid 2737 |
. . 3
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
133 | | eqid 2737 |
. . 3
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
134 | | eqid 2737 |
. . 3
β’
(.rβ(Scalarβπ)) =
(.rβ(Scalarβπ)) |
135 | | eqid 2737 |
. . 3
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
136 | 128, 129,
130, 131, 132, 133, 134, 135 | islmod 20342 |
. 2
β’ (π β LMod β (π β Grp β§
(Scalarβπ) β
Ring β§ βπ₯ β
(Baseβ(Scalarβπ))βπ β (Baseβ(Scalarβπ))βπ’ β (Baseβπ)βπ€ β (Baseβπ)(((π( Β·π
βπ)π€) β (Baseβπ) β§ (π( Β·π
βπ)(π€(+gβπ)π’)) = ((π( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π’)) β§ ((π₯(+gβ(Scalarβπ))π)( Β·π
βπ)π€) = ((π₯( Β·π
βπ)π€)(+gβπ)(π( Β·π
βπ)π€))) β§ (((π₯(.rβ(Scalarβπ))π)( Β·π
βπ)π€) = (π₯( Β·π
βπ)(π(
Β·π βπ)π€)) β§
((1rβ(Scalarβπ))( Β·π
βπ)π€) = π€)))) |
137 | 1, 4, 127, 136 | syl3anbrc 1344 |
1
β’ (π β π β LMod) |