Step | Hyp | Ref
| Expression |
1 | | lspsolv.w |
. . . . 5
β’ (π β π β LMod) |
2 | | lspsolv.q |
. . . . . . 7
β’ π = {π§ β π β£ βπ β π΅ (π§ + (π Β· π)) β (πβπ΄)} |
3 | 2 | ssrab3 4041 |
. . . . . 6
β’ π β π |
4 | 3 | a1i 11 |
. . . . 5
β’ (π β π β π) |
5 | | lspsolv.ss |
. . . . . . . 8
β’ (π β π΄ β π) |
6 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β π β LMod) |
7 | | lspsolv.f |
. . . . . . . . . . 11
β’ πΉ = (Scalarβπ) |
8 | | lspsolv.b |
. . . . . . . . . . 11
β’ π΅ = (BaseβπΉ) |
9 | | eqid 2733 |
. . . . . . . . . . 11
β’
(0gβπΉ) = (0gβπΉ) |
10 | 7, 8, 9 | lmod0cl 20363 |
. . . . . . . . . 10
β’ (π β LMod β
(0gβπΉ)
β π΅) |
11 | 6, 10 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π§ β π΄) β (0gβπΉ) β π΅) |
12 | | lspsolv.y |
. . . . . . . . . . . . . 14
β’ (π β π β π) |
13 | | lspsolv.v |
. . . . . . . . . . . . . . 15
β’ π = (Baseβπ) |
14 | | lspsolv.t |
. . . . . . . . . . . . . . 15
β’ Β· = (
Β·π βπ) |
15 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(0gβπ) = (0gβπ) |
16 | 13, 7, 14, 9, 15 | lmod0vs 20370 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ π β π) β ((0gβπΉ) Β· π) = (0gβπ)) |
17 | 1, 12, 16 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β
((0gβπΉ)
Β·
π) =
(0gβπ)) |
18 | 17 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π΄) β ((0gβπΉ) Β· π) = (0gβπ)) |
19 | 18 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β (π§ +
((0gβπΉ)
Β·
π)) = (π§ + (0gβπ))) |
20 | 5 | sselda 3945 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π΄) β π§ β π) |
21 | | lspsolv.p |
. . . . . . . . . . . . 13
β’ + =
(+gβπ) |
22 | 13, 21, 15 | lmod0vrid 20368 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π§ β π) β (π§ + (0gβπ)) = π§) |
23 | 6, 20, 22 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β (π§ + (0gβπ)) = π§) |
24 | 19, 23 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β (π§ +
((0gβπΉ)
Β·
π)) = π§) |
25 | | lspsolv.n |
. . . . . . . . . . . . 13
β’ π = (LSpanβπ) |
26 | 13, 25 | lspssid 20461 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π΄ β π) β π΄ β (πβπ΄)) |
27 | 1, 5, 26 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β π΄ β (πβπ΄)) |
28 | 27 | sselda 3945 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β π§ β (πβπ΄)) |
29 | 24, 28 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π§ β π΄) β (π§ +
((0gβπΉ)
Β·
π)) β (πβπ΄)) |
30 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π = (0gβπΉ) β (π Β· π) = ((0gβπΉ) Β· π)) |
31 | 30 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π = (0gβπΉ) β (π§ + (π Β· π)) = (π§ +
((0gβπΉ)
Β·
π))) |
32 | 31 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = (0gβπΉ) β ((π§ + (π Β· π)) β (πβπ΄) β (π§ +
((0gβπΉ)
Β·
π)) β (πβπ΄))) |
33 | 32 | rspcev 3580 |
. . . . . . . . 9
β’
(((0gβπΉ) β π΅ β§ (π§ +
((0gβπΉ)
Β·
π)) β (πβπ΄)) β βπ β π΅ (π§ + (π Β· π)) β (πβπ΄)) |
34 | 11, 29, 33 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π§ β π΄) β βπ β π΅ (π§ + (π Β· π)) β (πβπ΄)) |
35 | 5, 34 | ssrabdv 4032 |
. . . . . . 7
β’ (π β π΄ β {π§ β π β£ βπ β π΅ (π§ + (π Β· π)) β (πβπ΄)}) |
36 | 35, 2 | sseqtrrdi 3996 |
. . . . . 6
β’ (π β π΄ β π) |
37 | 7 | lmodfgrp 20345 |
. . . . . . . . . . 11
β’ (π β LMod β πΉ β Grp) |
38 | 1, 37 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ β Grp) |
39 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(1rβπΉ) = (1rβπΉ) |
40 | 7, 8, 39 | lmod1cl 20364 |
. . . . . . . . . . 11
β’ (π β LMod β
(1rβπΉ)
β π΅) |
41 | 1, 40 | syl 17 |
. . . . . . . . . 10
β’ (π β (1rβπΉ) β π΅) |
42 | | eqid 2733 |
. . . . . . . . . . 11
β’
(invgβπΉ) = (invgβπΉ) |
43 | 8, 42 | grpinvcl 18803 |
. . . . . . . . . 10
β’ ((πΉ β Grp β§
(1rβπΉ)
β π΅) β
((invgβπΉ)β(1rβπΉ)) β π΅) |
44 | 38, 41, 43 | syl2anc 585 |
. . . . . . . . 9
β’ (π β
((invgβπΉ)β(1rβπΉ)) β π΅) |
45 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(invgβπ) = (invgβπ) |
46 | 13, 45, 7, 14, 39, 42 | lmodvneg1 20380 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π β π) β (((invgβπΉ)β(1rβπΉ)) Β· π) = ((invgβπ)βπ)) |
47 | 1, 12, 46 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β
(((invgβπΉ)β(1rβπΉ)) Β· π) = ((invgβπ)βπ)) |
48 | 47 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π β (π +
(((invgβπΉ)β(1rβπΉ)) Β· π)) = (π +
((invgβπ)βπ))) |
49 | | lmodgrp 20343 |
. . . . . . . . . . . . 13
β’ (π β LMod β π β Grp) |
50 | 1, 49 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β Grp) |
51 | 13, 21, 15, 45 | grprinv 18806 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ π β π) β (π +
((invgβπ)βπ)) = (0gβπ)) |
52 | 50, 12, 51 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π +
((invgβπ)βπ)) = (0gβπ)) |
53 | 48, 52 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β (π +
(((invgβπΉ)β(1rβπΉ)) Β· π)) = (0gβπ)) |
54 | | lspsolv.s |
. . . . . . . . . . . . 13
β’ π = (LSubSpβπ) |
55 | 13, 54, 25 | lspcl 20452 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π΄ β π) β (πβπ΄) β π) |
56 | 1, 5, 55 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πβπ΄) β π) |
57 | 15, 54 | lss0cl 20422 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (πβπ΄) β π) β (0gβπ) β (πβπ΄)) |
58 | 1, 56, 57 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (0gβπ) β (πβπ΄)) |
59 | 53, 58 | eqeltrd 2834 |
. . . . . . . . 9
β’ (π β (π +
(((invgβπΉ)β(1rβπΉ)) Β· π)) β (πβπ΄)) |
60 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π = ((invgβπΉ)β(1rβπΉ)) β (π Β· π) = (((invgβπΉ)β(1rβπΉ)) Β· π)) |
61 | 60 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π = ((invgβπΉ)β(1rβπΉ)) β (π + (π Β· π)) = (π +
(((invgβπΉ)β(1rβπΉ)) Β· π))) |
62 | 61 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = ((invgβπΉ)β(1rβπΉ)) β ((π + (π Β· π)) β (πβπ΄) β (π +
(((invgβπΉ)β(1rβπΉ)) Β· π)) β (πβπ΄))) |
63 | 62 | rspcev 3580 |
. . . . . . . . 9
β’
((((invgβπΉ)β(1rβπΉ)) β π΅ β§ (π +
(((invgβπΉ)β(1rβπΉ)) Β· π)) β (πβπ΄)) β βπ β π΅ (π + (π Β· π)) β (πβπ΄)) |
64 | 44, 59, 63 | syl2anc 585 |
. . . . . . . 8
β’ (π β βπ β π΅ (π + (π Β· π)) β (πβπ΄)) |
65 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π§ = π β (π§ + (π Β· π)) = (π + (π Β· π))) |
66 | 65 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π§ = π β ((π§ + (π Β· π)) β (πβπ΄) β (π + (π Β· π)) β (πβπ΄))) |
67 | 66 | rexbidv 3172 |
. . . . . . . . 9
β’ (π§ = π β (βπ β π΅ (π§ + (π Β· π)) β (πβπ΄) β βπ β π΅ (π + (π Β· π)) β (πβπ΄))) |
68 | 67, 2 | elrab2 3649 |
. . . . . . . 8
β’ (π β π β (π β π β§ βπ β π΅ (π + (π Β· π)) β (πβπ΄))) |
69 | 12, 64, 68 | sylanbrc 584 |
. . . . . . 7
β’ (π β π β π) |
70 | 69 | snssd 4770 |
. . . . . 6
β’ (π β {π} β π) |
71 | 36, 70 | unssd 4147 |
. . . . 5
β’ (π β (π΄ βͺ {π}) β π) |
72 | 13, 25 | lspss 20460 |
. . . . 5
β’ ((π β LMod β§ π β π β§ (π΄ βͺ {π}) β π) β (πβ(π΄ βͺ {π})) β (πβπ)) |
73 | 1, 4, 71, 72 | syl3anc 1372 |
. . . 4
β’ (π β (πβ(π΄ βͺ {π})) β (πβπ)) |
74 | 7 | a1i 11 |
. . . . . 6
β’ (π β πΉ = (Scalarβπ)) |
75 | 8 | a1i 11 |
. . . . . 6
β’ (π β π΅ = (BaseβπΉ)) |
76 | 13 | a1i 11 |
. . . . . 6
β’ (π β π = (Baseβπ)) |
77 | 21 | a1i 11 |
. . . . . 6
β’ (π β + =
(+gβπ)) |
78 | 14 | a1i 11 |
. . . . . 6
β’ (π β Β· = (
Β·π βπ)) |
79 | 54 | a1i 11 |
. . . . . 6
β’ (π β π = (LSubSpβπ)) |
80 | 69 | ne0d 4296 |
. . . . . 6
β’ (π β π β β
) |
81 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ (π§ = π₯ β (π§ + (π Β· π)) = (π₯ + (π Β· π))) |
82 | 81 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π§ = π₯ β ((π§ + (π Β· π)) β (πβπ΄) β (π₯ + (π Β· π)) β (πβπ΄))) |
83 | 82 | rexbidv 3172 |
. . . . . . . . . . . . 13
β’ (π§ = π₯ β (βπ β π΅ (π§ + (π Β· π)) β (πβπ΄) β βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄))) |
84 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π Β· π) = (π Β· π)) |
85 | 84 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π₯ + (π Β· π)) = (π₯ + (π Β· π))) |
86 | 85 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π₯ + (π Β· π)) β (πβπ΄) β (π₯ + (π Β· π)) β (πβπ΄))) |
87 | 86 | cbvrexvw 3225 |
. . . . . . . . . . . . 13
β’
(βπ β
π΅ (π₯ + (π Β· π)) β (πβπ΄) β βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄)) |
88 | 83, 87 | bitrdi 287 |
. . . . . . . . . . . 12
β’ (π§ = π₯ β (βπ β π΅ (π§ + (π Β· π)) β (πβπ΄) β βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄))) |
89 | 88, 2 | elrab2 3649 |
. . . . . . . . . . 11
β’ (π₯ β π β (π₯ β π β§ βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄))) |
90 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ (π§ = π¦ β (π§ + (π Β· π)) = (π¦ + (π Β· π))) |
91 | 90 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π§ = π¦ β ((π§ + (π Β· π)) β (πβπ΄) β (π¦ + (π Β· π)) β (πβπ΄))) |
92 | 91 | rexbidv 3172 |
. . . . . . . . . . . . 13
β’ (π§ = π¦ β (βπ β π΅ (π§ + (π Β· π)) β (πβπ΄) β βπ β π΅ (π¦ + (π Β· π)) β (πβπ΄))) |
93 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π Β· π) = (π‘ Β· π)) |
94 | 93 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π = π‘ β (π¦ + (π Β· π)) = (π¦ + (π‘ Β· π))) |
95 | 94 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = π‘ β ((π¦ + (π Β· π)) β (πβπ΄) β (π¦ + (π‘ Β· π)) β (πβπ΄))) |
96 | 95 | cbvrexvw 3225 |
. . . . . . . . . . . . 13
β’
(βπ β
π΅ (π¦ + (π Β· π)) β (πβπ΄) β βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄)) |
97 | 92, 96 | bitrdi 287 |
. . . . . . . . . . . 12
β’ (π§ = π¦ β (βπ β π΅ (π§ + (π Β· π)) β (πβπ΄) β βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄))) |
98 | 97, 2 | elrab2 3649 |
. . . . . . . . . . 11
β’ (π¦ β π β (π¦ β π β§ βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄))) |
99 | 89, 98 | anbi12i 628 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π) β ((π₯ β π β§ βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄)) β§ (π¦ β π β§ βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄)))) |
100 | | an4 655 |
. . . . . . . . . 10
β’ (((π₯ β π β§ βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄)) β§ (π¦ β π β§ βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π₯ β π β§ π¦ β π) β§ (βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄) β§ βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄)))) |
101 | 99, 100 | bitri 275 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β π) β ((π₯ β π β§ π¦ β π) β§ (βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄) β§ βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄)))) |
102 | | reeanv 3216 |
. . . . . . . . . . 11
β’
(βπ β
π΅ βπ‘ β π΅ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄)) β (βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄) β§ βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄))) |
103 | | simp1ll 1237 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β π) |
104 | 103, 1 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β π β LMod) |
105 | | simp1lr 1238 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β π β π΅) |
106 | | simp1rl 1239 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β π₯ β π) |
107 | 13, 7, 14, 8 | lmodvscl 20354 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ π β π΅ β§ π₯ β π) β (π Β· π₯) β π) |
108 | 104, 105,
106, 107 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (π Β· π₯) β π) |
109 | | simp1rr 1240 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β π¦ β π) |
110 | 13, 21 | lmodvacl 20351 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ (π Β· π₯) β π β§ π¦ β π) β ((π Β· π₯) + π¦) β π) |
111 | 104, 108,
109, 110 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π Β· π₯) + π¦) β π) |
112 | | simp2l 1200 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β π β π΅) |
113 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(.rβπΉ) = (.rβπΉ) |
114 | 7, 8, 113 | lmodmcl 20349 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ π β π΅ β§ π β π΅) β (π(.rβπΉ)π ) β π΅) |
115 | 104, 105,
112, 114 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (π(.rβπΉ)π ) β π΅) |
116 | | simp2r 1201 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β π‘ β π΅) |
117 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’
(+gβπΉ) = (+gβπΉ) |
118 | 7, 8, 117 | lmodacl 20348 |
. . . . . . . . . . . . . . . 16
β’ ((π β LMod β§ (π(.rβπΉ)π ) β π΅ β§ π‘ β π΅) β ((π(.rβπΉ)π )(+gβπΉ)π‘) β π΅) |
119 | 104, 115,
116, 118 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π(.rβπΉ)π )(+gβπΉ)π‘) β π΅) |
120 | 103, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β π β π) |
121 | 13, 7, 14, 8 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β LMod β§ π β π΅ β§ π β π) β (π Β· π) β π) |
122 | 104, 112,
120, 121 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (π Β· π) β π) |
123 | 13, 7, 14, 8 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β LMod β§ π β π΅ β§ (π Β· π) β π) β (π Β· (π Β· π)) β π) |
124 | 104, 105,
122, 123 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (π Β· (π Β· π)) β π) |
125 | 13, 7, 14, 8 | lmodvscl 20354 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β LMod β§ π‘ β π΅ β§ π β π) β (π‘ Β· π) β π) |
126 | 104, 116,
120, 125 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (π‘ Β· π) β π) |
127 | 13, 21 | lmod4 20387 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ ((π Β· π₯) β π β§ π¦ β π) β§ ((π Β· (π Β· π)) β π β§ (π‘ Β· π) β π)) β (((π Β· π₯) + π¦) + ((π Β· (π Β· π)) + (π‘ Β· π))) = (((π Β· π₯) + (π Β· (π Β· π))) + (π¦ + (π‘ Β· π)))) |
128 | 104, 108,
109, 124, 126, 127 | syl122anc 1380 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (((π Β· π₯) + π¦) + ((π Β· (π Β· π)) + (π‘ Β· π))) = (((π Β· π₯) + (π Β· (π Β· π))) + (π¦ + (π‘ Β· π)))) |
129 | 13, 21, 7, 14, 8, 117 | lmodvsdir 20361 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β LMod β§ ((π(.rβπΉ)π ) β π΅ β§ π‘ β π΅ β§ π β π)) β (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π) = (((π(.rβπΉ)π ) Β· π) + (π‘ Β· π))) |
130 | 104, 115,
116, 120, 129 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π) = (((π(.rβπΉ)π ) Β· π) + (π‘ Β· π))) |
131 | 13, 7, 14, 8, 113 | lmodvsass 20362 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β LMod β§ (π β π΅ β§ π β π΅ β§ π β π)) β ((π(.rβπΉ)π ) Β· π) = (π Β· (π Β· π))) |
132 | 104, 105,
112, 120, 131 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π(.rβπΉ)π ) Β· π) = (π Β· (π Β· π))) |
133 | 132 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (((π(.rβπΉ)π ) Β· π) + (π‘ Β· π)) = ((π Β· (π Β· π)) + (π‘ Β· π))) |
134 | 130, 133 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π) = ((π Β· (π Β· π)) + (π‘ Β· π))) |
135 | 134 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (((π Β· π₯) + π¦) + (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π)) = (((π Β· π₯) + π¦) + ((π Β· (π Β· π)) + (π‘ Β· π)))) |
136 | 13, 21, 7, 14, 8 | lmodvsdi 20360 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β LMod β§ (π β π΅ β§ π₯ β π β§ (π Β· π) β π)) β (π Β· (π₯ + (π Β· π))) = ((π Β· π₯) + (π Β· (π Β· π)))) |
137 | 104, 105,
106, 122, 136 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (π Β· (π₯ + (π Β· π))) = ((π Β· π₯) + (π Β· (π Β· π)))) |
138 | 137 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π Β· (π₯ + (π Β· π))) + (π¦ + (π‘ Β· π))) = (((π Β· π₯) + (π Β· (π Β· π))) + (π¦ + (π‘ Β· π)))) |
139 | 128, 135,
138 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (((π Β· π₯) + π¦) + (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π)) = ((π Β· (π₯ + (π Β· π))) + (π¦ + (π‘ Β· π)))) |
140 | 103, 56 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (πβπ΄) β π) |
141 | | simp3l 1202 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (π₯ + (π Β· π)) β (πβπ΄)) |
142 | | simp3r 1203 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (π¦ + (π‘ Β· π)) β (πβπ΄)) |
143 | 7, 8, 21, 14, 54 | lsscl 20418 |
. . . . . . . . . . . . . . . . 17
β’ (((πβπ΄) β π β§ (π β π΅ β§ (π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π Β· (π₯ + (π Β· π))) + (π¦ + (π‘ Β· π))) β (πβπ΄)) |
144 | 140, 105,
141, 142, 143 | syl13anc 1373 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π Β· (π₯ + (π Β· π))) + (π¦ + (π‘ Β· π))) β (πβπ΄)) |
145 | 139, 144 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β (((π Β· π₯) + π¦) + (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π)) β (πβπ΄)) |
146 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . 18
β’ (π = ((π(.rβπΉ)π )(+gβπΉ)π‘) β (π Β· π) = (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π)) |
147 | 146 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ (π = ((π(.rβπΉ)π )(+gβπΉ)π‘) β (((π Β· π₯) + π¦) + (π Β· π)) = (((π Β· π₯) + π¦) + (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π))) |
148 | 147 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π = ((π(.rβπΉ)π )(+gβπΉ)π‘) β ((((π Β· π₯) + π¦) + (π Β· π)) β (πβπ΄) β (((π Β· π₯) + π¦) + (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π)) β (πβπ΄))) |
149 | 148 | rspcev 3580 |
. . . . . . . . . . . . . . 15
β’ ((((π(.rβπΉ)π )(+gβπΉ)π‘) β π΅ β§ (((π Β· π₯) + π¦) + (((π(.rβπΉ)π )(+gβπΉ)π‘) Β· π)) β (πβπ΄)) β βπ β π΅ (((π Β· π₯) + π¦) + (π Β· π)) β (πβπ΄)) |
150 | 119, 145,
149 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β βπ β π΅ (((π Β· π₯) + π¦) + (π Β· π)) β (πβπ΄)) |
151 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = ((π Β· π₯) + π¦) β (π§ + (π Β· π)) = (((π Β· π₯) + π¦) + (π Β· π))) |
152 | 151 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π§ = ((π Β· π₯) + π¦) β ((π§ + (π Β· π)) β (πβπ΄) β (((π Β· π₯) + π¦) + (π Β· π)) β (πβπ΄))) |
153 | 152 | rexbidv 3172 |
. . . . . . . . . . . . . . 15
β’ (π§ = ((π Β· π₯) + π¦) β (βπ β π΅ (π§ + (π Β· π)) β (πβπ΄) β βπ β π΅ (((π Β· π₯) + π¦) + (π Β· π)) β (πβπ΄))) |
154 | 153, 2 | elrab2 3649 |
. . . . . . . . . . . . . 14
β’ (((π Β· π₯) + π¦) β π β (((π Β· π₯) + π¦) β π β§ βπ β π΅ (((π Β· π₯) + π¦) + (π Β· π)) β (πβπ΄))) |
155 | 111, 150,
154 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β§ (π β π΅ β§ π‘ β π΅) β§ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π Β· π₯) + π¦) β π) |
156 | 155 | 3exp 1120 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β ((π β π΅ β§ π‘ β π΅) β (((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄)) β ((π Β· π₯) + π¦) β π))) |
157 | 156 | rexlimdvv 3201 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β (βπ β π΅ βπ‘ β π΅ ((π₯ + (π Β· π)) β (πβπ΄) β§ (π¦ + (π‘ Β· π)) β (πβπ΄)) β ((π Β· π₯) + π¦) β π)) |
158 | 102, 157 | biimtrrid 242 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ (π₯ β π β§ π¦ β π)) β ((βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄) β§ βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄)) β ((π Β· π₯) + π¦) β π)) |
159 | 158 | expimpd 455 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (((π₯ β π β§ π¦ β π) β§ (βπ β π΅ (π₯ + (π Β· π)) β (πβπ΄) β§ βπ‘ β π΅ (π¦ + (π‘ Β· π)) β (πβπ΄))) β ((π Β· π₯) + π¦) β π)) |
160 | 101, 159 | biimtrid 241 |
. . . . . . . 8
β’ ((π β§ π β π΅) β ((π₯ β π β§ π¦ β π) β ((π Β· π₯) + π¦) β π)) |
161 | 160 | exp4b 432 |
. . . . . . 7
β’ (π β (π β π΅ β (π₯ β π β (π¦ β π β ((π Β· π₯) + π¦) β π)))) |
162 | 161 | 3imp2 1350 |
. . . . . 6
β’ ((π β§ (π β π΅ β§ π₯ β π β§ π¦ β π)) β ((π Β· π₯) + π¦) β π) |
163 | 74, 75, 76, 77, 78, 79, 4, 80, 162 | islssd 20411 |
. . . . 5
β’ (π β π β π) |
164 | 54, 25 | lspid 20458 |
. . . . 5
β’ ((π β LMod β§ π β π) β (πβπ) = π) |
165 | 1, 163, 164 | syl2anc 585 |
. . . 4
β’ (π β (πβπ) = π) |
166 | 73, 165 | sseqtrd 3985 |
. . 3
β’ (π β (πβ(π΄ βͺ {π})) β π) |
167 | | lspsolv.x |
. . 3
β’ (π β π β (πβ(π΄ βͺ {π}))) |
168 | 166, 167 | sseldd 3946 |
. 2
β’ (π β π β π) |
169 | | oveq1 7365 |
. . . . . 6
β’ (π§ = π β (π§ + (π Β· π)) = (π + (π Β· π))) |
170 | 169 | eleq1d 2819 |
. . . . 5
β’ (π§ = π β ((π§ + (π Β· π)) β (πβπ΄) β (π + (π Β· π)) β (πβπ΄))) |
171 | 170 | rexbidv 3172 |
. . . 4
β’ (π§ = π β (βπ β π΅ (π§ + (π Β· π)) β (πβπ΄) β βπ β π΅ (π + (π Β· π)) β (πβπ΄))) |
172 | 171, 2 | elrab2 3649 |
. . 3
β’ (π β π β (π β π β§ βπ β π΅ (π + (π Β· π)) β (πβπ΄))) |
173 | 172 | simprbi 498 |
. 2
β’ (π β π β βπ β π΅ (π + (π Β· π)) β (πβπ΄)) |
174 | 168, 173 | syl 17 |
1
β’ (π β βπ β π΅ (π + (π Β· π)) β (πβπ΄)) |