Step | Hyp | Ref
| Expression |
1 | | fveq2 6892 |
. . . . . 6
β’ (π = π β (Baseβπ) = (Baseβπ)) |
2 | | islmod.v |
. . . . . 6
β’ π = (Baseβπ) |
3 | 1, 2 | eqtr4di 2791 |
. . . . 5
β’ (π = π β (Baseβπ) = π) |
4 | | fveq2 6892 |
. . . . . . 7
β’ (π = π β (+gβπ) = (+gβπ)) |
5 | | islmod.a |
. . . . . . 7
β’ + =
(+gβπ) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . 6
β’ (π = π β (+gβπ) = + ) |
7 | | fveq2 6892 |
. . . . . . . 8
β’ (π = π β (Scalarβπ) = (Scalarβπ)) |
8 | | islmod.f |
. . . . . . . 8
β’ πΉ = (Scalarβπ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . 7
β’ (π = π β (Scalarβπ) = πΉ) |
10 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = π β (
Β·π βπ) = ( Β·π
βπ)) |
11 | | islmod.s |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = π β (
Β·π βπ) = Β· ) |
13 | 12 | sbceq1d 3783 |
. . . . . . 7
β’ (π = π β ([(
Β·π βπ) / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [ Β· / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))))) |
14 | 9, 13 | sbceqbid 3785 |
. . . . . 6
β’ (π = π β ([(Scalarβπ) / π][(
Β·π βπ) / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [πΉ / π][ Β· / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))))) |
15 | 6, 14 | sbceqbid 3785 |
. . . . 5
β’ (π = π β ([(+gβπ) / π][(Scalarβπ) / π][(
Β·π βπ) / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [ + / π][πΉ / π][ Β· / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))))) |
16 | 3, 15 | sbceqbid 3785 |
. . . 4
β’ (π = π β ([(Baseβπ) / π£][(+gβπ) / π][(Scalarβπ) / π][(
Β·π βπ) / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [π / π£][ + / π][πΉ / π][ Β· / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))))) |
17 | 2 | fvexi 6906 |
. . . . . 6
β’ π β V |
18 | 5 | fvexi 6906 |
. . . . . 6
β’ + β
V |
19 | 8 | fvexi 6906 |
. . . . . 6
β’ πΉ β V |
20 | | simp3 1139 |
. . . . . . . . . 10
β’ ((π£ = π β§ π = + β§ π = πΉ) β π = πΉ) |
21 | 20 | fveq2d 6896 |
. . . . . . . . 9
β’ ((π£ = π β§ π = + β§ π = πΉ) β (Baseβπ) = (BaseβπΉ)) |
22 | | islmod.k |
. . . . . . . . 9
β’ πΎ = (BaseβπΉ) |
23 | 21, 22 | eqtr4di 2791 |
. . . . . . . 8
β’ ((π£ = π β§ π = + β§ π = πΉ) β (Baseβπ) = πΎ) |
24 | 20 | fveq2d 6896 |
. . . . . . . . . 10
β’ ((π£ = π β§ π = + β§ π = πΉ) β (+gβπ) = (+gβπΉ)) |
25 | | islmod.p |
. . . . . . . . . 10
⒠⨣ =
(+gβπΉ) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π£ = π β§ π = + β§ π = πΉ) β (+gβπ) = ⨣ ) |
27 | 20 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ ((π£ = π β§ π = + β§ π = πΉ) β (.rβπ) = (.rβπΉ)) |
28 | | islmod.t |
. . . . . . . . . . . 12
β’ Γ =
(.rβπΉ) |
29 | 27, 28 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ ((π£ = π β§ π = + β§ π = πΉ) β (.rβπ) = Γ ) |
30 | 29 | sbceq1d 3783 |
. . . . . . . . . 10
β’ ((π£ = π β§ π = + β§ π = πΉ) β ([(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [ Γ / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))))) |
31 | 28 | fvexi 6906 |
. . . . . . . . . . . 12
β’ Γ β
V |
32 | | oveq 7415 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = Γ β (ππ‘π) = (π Γ π)) |
33 | 32 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = Γ β ((ππ‘π)π π€) = ((π Γ π)π π€)) |
34 | 33 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = Γ β (((ππ‘π)π π€) = (ππ (ππ π€)) β ((π Γ π)π π€) = (ππ (ππ π€)))) |
35 | 34 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = Γ β ((((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€) β (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) |
36 | 35 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π‘ = Γ β ((((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)) β (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)))) |
37 | 36 | 2ralbidv 3219 |
. . . . . . . . . . . . . 14
β’ (π‘ = Γ β
(βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)) β βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)))) |
38 | 37 | 2ralbidv 3219 |
. . . . . . . . . . . . 13
β’ (π‘ = Γ β
(βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)) β βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)))) |
39 | 38 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π‘ = Γ β ((π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β (π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))))) |
40 | 31, 39 | sbcie 3821 |
. . . . . . . . . . 11
β’ ([
Γ /
π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β (π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)))) |
41 | 20 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ ((π£ = π β§ π = + β§ π = πΉ) β (π β Ring β πΉ β Ring)) |
42 | | simp1 1137 |
. . . . . . . . . . . . . 14
β’ ((π£ = π β§ π = + β§ π = πΉ) β π£ = π) |
43 | 42 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
β’ ((π£ = π β§ π = + β§ π = πΉ) β ((ππ π€) β π£ β (ππ π€) β π)) |
44 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π£ = π β§ π = + β§ π = πΉ) β π = + ) |
45 | 44 | oveqd 7426 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π£ = π β§ π = + β§ π = πΉ) β (π€ππ₯) = (π€ + π₯)) |
46 | 45 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . 18
β’ ((π£ = π β§ π = + β§ π = πΉ) β (ππ (π€ππ₯)) = (ππ (π€ + π₯))) |
47 | 44 | oveqd 7426 |
. . . . . . . . . . . . . . . . . 18
β’ ((π£ = π β§ π = + β§ π = πΉ) β ((ππ π€)π(ππ π₯)) = ((ππ π€) + (ππ π₯))) |
48 | 46, 47 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . 17
β’ ((π£ = π β§ π = + β§ π = πΉ) β ((ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)))) |
49 | 44 | oveqd 7426 |
. . . . . . . . . . . . . . . . . 18
β’ ((π£ = π β§ π = + β§ π = πΉ) β ((ππ π€)π(ππ π€)) = ((ππ π€) + (ππ π€))) |
50 | 49 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ ((π£ = π β§ π = + β§ π = πΉ) β (((πππ)π π€) = ((ππ π€)π(ππ π€)) β ((πππ)π π€) = ((ππ π€) + (ππ π€)))) |
51 | 43, 48, 50 | 3anbi123d 1437 |
. . . . . . . . . . . . . . . 16
β’ ((π£ = π β§ π = + β§ π = πΉ) β (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β ((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))))) |
52 | 20 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π£ = π β§ π = + β§ π = πΉ) β (1rβπ) = (1rβπΉ)) |
53 | | islmod.u |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 =
(1rβπΉ) |
54 | 52, 53 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π£ = π β§ π = + β§ π = πΉ) β (1rβπ) = 1 ) |
55 | 54 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . 18
β’ ((π£ = π β§ π = + β§ π = πΉ) β ((1rβπ)π π€) = ( 1 π π€)) |
56 | 55 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ ((π£ = π β§ π = + β§ π = πΉ) β (((1rβπ)π π€) = π€ β ( 1 π π€) = π€)) |
57 | 56 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
β’ ((π£ = π β§ π = + β§ π = πΉ) β ((((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€) β (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))) |
58 | 51, 57 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ ((π£ = π β§ π = + β§ π = πΉ) β ((((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)) β (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)))) |
59 | 42, 58 | raleqbidv 3343 |
. . . . . . . . . . . . . 14
β’ ((π£ = π β§ π = + β§ π = πΉ) β (βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)) β βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)))) |
60 | 42, 59 | raleqbidv 3343 |
. . . . . . . . . . . . 13
β’ ((π£ = π β§ π = + β§ π = πΉ) β (βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)) β βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)))) |
61 | 60 | 2ralbidv 3219 |
. . . . . . . . . . . 12
β’ ((π£ = π β§ π = + β§ π = πΉ) β (βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)) β βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)))) |
62 | 41, 61 | anbi12d 632 |
. . . . . . . . . . 11
β’ ((π£ = π β§ π = + β§ π = πΉ) β ((π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β (πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))))) |
63 | 40, 62 | bitrid 283 |
. . . . . . . . . 10
β’ ((π£ = π β§ π = + β§ π = πΉ) β ([ Γ / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β (πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))))) |
64 | 30, 63 | bitrd 279 |
. . . . . . . . 9
β’ ((π£ = π β§ π = + β§ π = πΉ) β ([(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β (πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))))) |
65 | 26, 64 | sbceqbid 3785 |
. . . . . . . 8
β’ ((π£ = π β§ π = + β§ π = πΉ) β ([(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [ ⨣ / π](πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))))) |
66 | 23, 65 | sbceqbid 3785 |
. . . . . . 7
β’ ((π£ = π β§ π = + β§ π = πΉ) β ([(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [πΎ / π][ ⨣ / π](πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))))) |
67 | 66 | sbcbidv 3837 |
. . . . . 6
β’ ((π£ = π β§ π = + β§ π = πΉ) β ([ Β· / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [ Β· / π ][πΎ / π][ ⨣ / π](πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))))) |
68 | 17, 18, 19, 67 | sbc3ie 3864 |
. . . . 5
β’
([π / π£][ + / π][πΉ / π][ Β· / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β [ Β· / π ][πΎ / π][ ⨣ / π](πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)))) |
69 | 11 | fvexi 6906 |
. . . . . 6
β’ Β· β
V |
70 | 22 | fvexi 6906 |
. . . . . 6
β’ πΎ β V |
71 | 25 | fvexi 6906 |
. . . . . 6
⒠⨣ β
V |
72 | | simp2 1138 |
. . . . . . . 8
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β π = πΎ) |
73 | | simp1 1137 |
. . . . . . . . . . . . . 14
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β π = Β· ) |
74 | 73 | oveqd 7426 |
. . . . . . . . . . . . 13
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (ππ π€) = (π Β· π€)) |
75 | 74 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((ππ π€) β π β (π Β· π€) β π)) |
76 | 73 | oveqd 7426 |
. . . . . . . . . . . . 13
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (ππ (π€ + π₯)) = (π Β· (π€ + π₯))) |
77 | 73 | oveqd 7426 |
. . . . . . . . . . . . . 14
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (ππ π₯) = (π Β· π₯)) |
78 | 74, 77 | oveq12d 7427 |
. . . . . . . . . . . . 13
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((ππ π€) + (ππ π₯)) = ((π Β· π€) + (π Β· π₯))) |
79 | 76, 78 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)))) |
80 | | simp3 1139 |
. . . . . . . . . . . . . . . 16
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β π = ⨣ ) |
81 | 80 | oveqd 7426 |
. . . . . . . . . . . . . . 15
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (πππ) = (π ⨣ π)) |
82 | 81 | oveq1d 7424 |
. . . . . . . . . . . . . 14
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((πππ)π π€) = ((π ⨣ π)π π€)) |
83 | 73 | oveqd 7426 |
. . . . . . . . . . . . . 14
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((π ⨣ π)π π€) = ((π ⨣ π) Β· π€)) |
84 | 82, 83 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((πππ)π π€) = ((π ⨣ π) Β· π€)) |
85 | 73 | oveqd 7426 |
. . . . . . . . . . . . . 14
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (ππ π€) = (π Β· π€)) |
86 | 85, 74 | oveq12d 7427 |
. . . . . . . . . . . . 13
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((ππ π€) + (ππ π€)) = ((π Β· π€) + (π Β· π€))) |
87 | 84, 86 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (((πππ)π π€) = ((ππ π€) + (ππ π€)) β ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€)))) |
88 | 75, 79, 87 | 3anbi123d 1437 |
. . . . . . . . . . 11
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β ((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))))) |
89 | 73 | oveqd 7426 |
. . . . . . . . . . . . 13
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((π Γ π)π π€) = ((π Γ π) Β· π€)) |
90 | 74 | oveq2d 7425 |
. . . . . . . . . . . . . 14
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (ππ (ππ π€)) = (ππ (π Β· π€))) |
91 | 73 | oveqd 7426 |
. . . . . . . . . . . . . 14
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (ππ (π Β· π€)) = (π Β· (π Β· π€))) |
92 | 90, 91 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (ππ (ππ π€)) = (π Β· (π Β· π€))) |
93 | 89, 92 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (((π Γ π)π π€) = (ππ (ππ π€)) β ((π Γ π) Β· π€) = (π Β· (π Β· π€)))) |
94 | 73 | oveqd 7426 |
. . . . . . . . . . . . 13
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ( 1 π π€) = ( 1 Β· π€)) |
95 | 94 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β (( 1 π π€) = π€ β ( 1 Β· π€) = π€)) |
96 | 93, 95 | anbi12d 632 |
. . . . . . . . . . 11
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€) β (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))) |
97 | 88, 96 | anbi12d 632 |
. . . . . . . . . 10
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)) β (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)))) |
98 | 97 | 2ralbidv 3219 |
. . . . . . . . 9
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β
(βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)) β βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)))) |
99 | 72, 98 | raleqbidv 3343 |
. . . . . . . 8
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β
(βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)) β βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)))) |
100 | 72, 99 | raleqbidv 3343 |
. . . . . . 7
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β
(βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€)) β βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)))) |
101 | 100 | anbi2d 630 |
. . . . . 6
β’ ((π = Β· β§ π = πΎ β§ π = ⨣ ) β ((πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))) β (πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))))) |
102 | 69, 70, 71, 101 | sbc3ie 3864 |
. . . . 5
β’ ([
Β·
/ π ][πΎ / π][ ⨣ / π](πΉ β Ring β§ βπ β π βπ β π βπ₯ β π βπ€ β π (((ππ π€) β π β§ (ππ (π€ + π₯)) = ((ππ π€) + (ππ π₯)) β§ ((πππ)π π€) = ((ππ π€) + (ππ π€))) β§ (((π Γ π)π π€) = (ππ (ππ π€)) β§ ( 1 π π€) = π€))) β (πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)))) |
103 | 68, 102 | bitri 275 |
. . . 4
β’
([π / π£][ + / π][πΉ / π][ Β· / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β (πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)))) |
104 | 16, 103 | bitrdi 287 |
. . 3
β’ (π = π β ([(Baseβπ) / π£][(+gβπ) / π][(Scalarβπ) / π][(
Β·π βπ) / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€))) β (πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))))) |
105 | | df-lmod 20473 |
. . 3
β’ LMod =
{π β Grp β£
[(Baseβπ) /
π£][(+gβπ) / π][(Scalarβπ) / π][(
Β·π βπ) / π ][(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘](π β Ring β§ βπ β π βπ β π βπ₯ β π£ βπ€ β π£ (((ππ π€) β π£ β§ (ππ (π€ππ₯)) = ((ππ π€)π(ππ π₯)) β§ ((πππ)π π€) = ((ππ π€)π(ππ π€))) β§ (((ππ‘π)π π€) = (ππ (ππ π€)) β§ ((1rβπ)π π€) = π€)))} |
106 | 104, 105 | elrab2 3687 |
. 2
β’ (π β LMod β (π β Grp β§ (πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))))) |
107 | | 3anass 1096 |
. 2
β’ ((π β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))) β (π β Grp β§ (πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€))))) |
108 | 106, 107 | bitr4i 278 |
1
β’ (π β LMod β (π β Grp β§ πΉ β Ring β§ βπ β πΎ βπ β πΎ βπ₯ β π βπ€ β π (((π Β· π€) β π β§ (π Β· (π€ + π₯)) = ((π Β· π€) + (π Β· π₯)) β§ ((π ⨣ π) Β· π€) = ((π Β· π€) + (π Β· π€))) β§ (((π Γ π) Β· π€) = (π Β· (π Β· π€)) β§ ( 1 Β· π€) = π€)))) |