Step | Hyp | Ref
| Expression |
1 | | difexg 5284 |
. . . . . . . . . . 11
β’ (π β π« π΅ β (π β {π}) β V) |
2 | 1 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β (π β {π}) β V) |
3 | 2 | adantl 482 |
. . . . . . . . 9
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β (π β {π}) β V) |
4 | 3 | adantr 481 |
. . . . . . . 8
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ πΉ finSupp 0 ) β (π β {π}) β V) |
5 | | lincresunit.g |
. . . . . . . . 9
β’ πΊ = (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) |
6 | | mptexg 7171 |
. . . . . . . . 9
β’ ((π β {π}) β V β (π β (π β {π}) β¦ ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ ))) β V) |
7 | 5, 6 | eqeltrid 2841 |
. . . . . . . 8
β’ ((π β {π}) β V β πΊ β V) |
8 | 4, 7 | syl 17 |
. . . . . . 7
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ πΉ finSupp 0 ) β πΊ β V) |
9 | 5 | funmpt2 6540 |
. . . . . . . 8
β’ Fun πΊ |
10 | 9 | a1i 11 |
. . . . . . 7
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ πΉ finSupp 0 ) β Fun πΊ) |
11 | | lincresunit.0 |
. . . . . . . . 9
β’ 0 =
(0gβπ
) |
12 | 11 | fvexi 6856 |
. . . . . . . 8
β’ 0 β
V |
13 | 12 | a1i 11 |
. . . . . . 7
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ πΉ finSupp 0 ) β 0 β
V) |
14 | | simpr 485 |
. . . . . . . 8
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ πΉ finSupp 0 ) β πΉ finSupp 0 ) |
15 | 14 | fsuppimpd 9312 |
. . . . . . 7
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ πΉ finSupp 0 ) β (πΉ supp 0 ) β
Fin) |
16 | | simplr 767 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π β (π β {π})) β (π β π« π΅ β§ π β LMod β§ π β π)) |
17 | | simpll 765 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π β (π β {π})) β (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) |
18 | | eldifi 4086 |
. . . . . . . . . . . . . 14
β’ (π β (π β {π}) β π β π) |
19 | 18 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π β (π β {π})) β π β π) |
20 | | lincresunit.b |
. . . . . . . . . . . . . 14
β’ π΅ = (Baseβπ) |
21 | | lincresunit.r |
. . . . . . . . . . . . . 14
β’ π
= (Scalarβπ) |
22 | | lincresunit.e |
. . . . . . . . . . . . . 14
β’ πΈ = (Baseβπ
) |
23 | | lincresunit.u |
. . . . . . . . . . . . . 14
β’ π = (Unitβπ
) |
24 | | lincresunit.z |
. . . . . . . . . . . . . 14
β’ π = (0gβπ) |
25 | | lincresunit.n |
. . . . . . . . . . . . . 14
β’ π = (invgβπ
) |
26 | | lincresunit.i |
. . . . . . . . . . . . . 14
β’ πΌ = (invrβπ
) |
27 | | lincresunit.t |
. . . . . . . . . . . . . 14
β’ Β· =
(.rβπ
) |
28 | 20, 21, 22, 23, 11, 24, 25, 26, 27, 5 | lincresunitlem2 46547 |
. . . . . . . . . . . . 13
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) β§ π β π) β ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ )) β πΈ) |
29 | 16, 17, 19, 28 | syl21anc 836 |
. . . . . . . . . . . 12
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π β (π β {π})) β ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ )) β πΈ) |
30 | 29 | ralrimiva 3143 |
. . . . . . . . . . 11
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β βπ β (π β {π})((πΌβ(πβ(πΉβπ))) Β· (πΉβπ )) β πΈ) |
31 | 5 | fnmpt 6641 |
. . . . . . . . . . 11
β’
(βπ β
(π β {π})((πΌβ(πβ(πΉβπ))) Β· (πΉβπ )) β πΈ β πΊ Fn (π β {π})) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β πΊ Fn (π β {π})) |
33 | | elmapfn 8803 |
. . . . . . . . . . . 12
β’ (πΉ β (πΈ βm π) β πΉ Fn π) |
34 | 33 | adantr 481 |
. . . . . . . . . . 11
β’ ((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β πΉ Fn π) |
35 | 34 | adantr 481 |
. . . . . . . . . 10
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β πΉ Fn π) |
36 | 32, 35 | jca 512 |
. . . . . . . . 9
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β (πΊ Fn (π β {π}) β§ πΉ Fn π)) |
37 | | difssd 4092 |
. . . . . . . . . 10
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β (π β {π}) β π) |
38 | | simpr1 1194 |
. . . . . . . . . 10
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β π β π« π΅) |
39 | 12 | a1i 11 |
. . . . . . . . . 10
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β 0 β V) |
40 | 37, 38, 39 | 3jca 1128 |
. . . . . . . . 9
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β ((π β {π}) β π β§ π β π« π΅ β§ 0 β
V)) |
41 | | fveq2 6842 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (πΉβπ ) = (πΉβπ₯)) |
42 | 41 | oveq2d 7373 |
. . . . . . . . . . . . 13
β’ (π = π₯ β ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ )) = ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ₯))) |
43 | | simplr 767 |
. . . . . . . . . . . . 13
β’
(((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β§ (πΉβπ₯) = 0 ) β π₯ β (π β {π})) |
44 | | simpllr 774 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β§ (πΉβπ₯) = 0 ) β (π β π« π΅ β§ π β LMod β§ π β π)) |
45 | | simpll 765 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β§ (πΉβπ₯) = 0 ) β (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) |
47 | | eldifi 4086 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π β {π}) β π₯ β π) |
48 | 47 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β π₯ β π) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β§ (πΉβπ₯) = 0 ) β π₯ β π) |
50 | 20, 21, 22, 23, 11, 24, 25, 26, 27, 5 | lincresunitlem2 46547 |
. . . . . . . . . . . . . 14
β’ ((((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) β§ π₯ β π) β ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ₯)) β πΈ) |
51 | 44, 46, 49, 50 | syl21anc 836 |
. . . . . . . . . . . . 13
β’
(((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β§ (πΉβπ₯) = 0 ) β ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ₯)) β πΈ) |
52 | 5, 42, 43, 51 | fvmptd3 6971 |
. . . . . . . . . . . 12
β’
(((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β§ (πΉβπ₯) = 0 ) β (πΊβπ₯) = ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ₯))) |
53 | | oveq2 7365 |
. . . . . . . . . . . . 13
β’ ((πΉβπ₯) = 0 β ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ₯)) = ((πΌβ(πβ(πΉβπ))) Β· 0 )) |
54 | 21 | lmodring 20330 |
. . . . . . . . . . . . . . . . 17
β’ (π β LMod β π
β Ring) |
55 | 54 | 3ad2ant2 1134 |
. . . . . . . . . . . . . . . 16
β’ ((π β π« π΅ β§ π β LMod β§ π β π) β π
β Ring) |
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β π
β Ring) |
57 | 20, 21, 22, 23, 11, 24, 25, 26, 27, 5 | lincresunitlem1 46546 |
. . . . . . . . . . . . . . . 16
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π)) β (πΌβ(πβ(πΉβπ))) β πΈ) |
58 | 57 | ancoms 459 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β (πΌβ(πβ(πΉβπ))) β πΈ) |
59 | 22, 27, 11 | ringrz 20012 |
. . . . . . . . . . . . . . 15
β’ ((π
β Ring β§ (πΌβ(πβ(πΉβπ))) β πΈ) β ((πΌβ(πβ(πΉβπ))) Β· 0 ) = 0 ) |
60 | 56, 58, 59 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β ((πΌβ(πβ(πΉβπ))) Β· 0 ) = 0 ) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β ((πΌβ(πβ(πΉβπ))) Β· 0 ) = 0 ) |
62 | 53, 61 | sylan9eqr 2798 |
. . . . . . . . . . . 12
β’
(((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β§ (πΉβπ₯) = 0 ) β ((πΌβ(πβ(πΉβπ))) Β· (πΉβπ₯)) = 0 ) |
63 | 52, 62 | eqtrd 2776 |
. . . . . . . . . . 11
β’
(((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β§ (πΉβπ₯) = 0 ) β (πΊβπ₯) = 0 ) |
64 | 63 | ex 413 |
. . . . . . . . . 10
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ π₯ β (π β {π})) β ((πΉβπ₯) = 0 β (πΊβπ₯) = 0 )) |
65 | 64 | ralrimiva 3143 |
. . . . . . . . 9
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β βπ₯ β (π β {π})((πΉβπ₯) = 0 β (πΊβπ₯) = 0 )) |
66 | | suppfnss 8120 |
. . . . . . . . . 10
β’ (((πΊ Fn (π β {π}) β§ πΉ Fn π) β§ ((π β {π}) β π β§ π β π« π΅ β§ 0 β V)) β
(βπ₯ β (π β {π})((πΉβπ₯) = 0 β (πΊβπ₯) = 0 ) β (πΊ supp 0 ) β (πΉ supp 0 ))) |
67 | 66 | imp 407 |
. . . . . . . . 9
β’ ((((πΊ Fn (π β {π}) β§ πΉ Fn π) β§ ((π β {π}) β π β§ π β π« π΅ β§ 0 β V)) β§
βπ₯ β (π β {π})((πΉβπ₯) = 0 β (πΊβπ₯) = 0 )) β (πΊ supp 0 ) β (πΉ supp 0 )) |
68 | 36, 40, 65, 67 | syl21anc 836 |
. . . . . . . 8
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β (πΊ supp 0 ) β (πΉ supp 0 )) |
69 | 68 | adantr 481 |
. . . . . . 7
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ πΉ finSupp 0 ) β (πΊ supp 0 ) β (πΉ supp 0 )) |
70 | | suppssfifsupp 9320 |
. . . . . . 7
β’ (((πΊ β V β§ Fun πΊ β§ 0 β V) β§ ((πΉ supp 0 ) β Fin β§ (πΊ supp 0 ) β (πΉ supp 0 ))) β πΊ finSupp 0 ) |
71 | 8, 10, 13, 15, 69, 70 | syl32anc 1378 |
. . . . . 6
β’ ((((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β§ πΉ finSupp 0 ) β πΊ finSupp 0 ) |
72 | 71 | ex 413 |
. . . . 5
β’ (((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β§ (π β π« π΅ β§ π β LMod β§ π β π)) β (πΉ finSupp 0 β πΊ finSupp 0 )) |
73 | 72 | ex 413 |
. . . 4
β’ ((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β ((π β π« π΅ β§ π β LMod β§ π β π) β (πΉ finSupp 0 β πΊ finSupp 0 ))) |
74 | 73 | com23 86 |
. . 3
β’ ((πΉ β (πΈ βm π) β§ (πΉβπ) β π) β (πΉ finSupp 0 β ((π β π« π΅ β§ π β LMod β§ π β π) β πΊ finSupp 0 ))) |
75 | 74 | 3impia 1117 |
. 2
β’ ((πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 ) β ((π β π« π΅ β§ π β LMod β§ π β π) β πΊ finSupp 0 )) |
76 | 75 | impcom 408 |
1
β’ (((π β π« π΅ β§ π β LMod β§ π β π) β§ (πΉ β (πΈ βm π) β§ (πΉβπ) β π β§ πΉ finSupp 0 )) β πΊ finSupp 0 ) |