Proof of Theorem lindslinindimp2lem4
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → 𝑀 ∈ LMod) |
2 | 1 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑀 ∈ LMod) |
3 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑆 ⊆ (Base‘𝑀)) |
4 | | elpwg 4116 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀))) |
5 | 4 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∈ 𝒫 (Base‘𝑀) ↔ 𝑆 ⊆ (Base‘𝑀))) |
6 | 3, 5 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑆 ∈ 𝒫 (Base‘𝑀)) |
7 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
8 | 7 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → 𝑥 ∈ 𝑆) |
9 | 2, 6, 8 | 3jca 1235 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) |
10 | 9 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) |
11 | | simpl 472 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 )) |
12 | | lindslinind.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥})) |
13 | 12 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))) |
14 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑀) =
(Base‘𝑀) |
15 | | lindslinind.r |
. . . . . . . . . . 11
⊢ 𝑅 = (Scalar‘𝑀) |
16 | | lindslinind.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝑅) |
17 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
18 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(+g‘𝑀) = (+g‘𝑀) |
19 | | lindslinind.0 |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑅) |
20 | 14, 15, 16, 17, 18, 19 | lincdifsn 42007 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫
(Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ 𝐺 = (𝑓 ↾ (𝑆 ∖ {𝑥}))) → (𝑓( linC ‘𝑀)𝑆) = ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
21 | 10, 11, 13, 20 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑓( linC ‘𝑀)𝑆) = ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
22 | 21 | eqeq1d 2612 |
. . . . . . . 8
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 ↔ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = 𝑍)) |
23 | | lmodgrp 18693 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp) |
24 | 23 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) → 𝑀 ∈ Grp) |
25 | 24 | ad2antrl 760 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑀 ∈ Grp) |
26 | 1 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑀 ∈ LMod) |
27 | | elmapi 7765 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) → 𝑓:𝑆⟶𝐵) |
28 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝑆⟶𝐵 ∧ 𝑥 ∈ 𝑆) → (𝑓‘𝑥) ∈ 𝐵) |
29 | 28 | expcom 450 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑆 → (𝑓:𝑆⟶𝐵 → (𝑓‘𝑥) ∈ 𝐵)) |
30 | 29 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓:𝑆⟶𝐵 → (𝑓‘𝑥) ∈ 𝐵)) |
31 | 30 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝑆⟶𝐵 → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵)) |
32 | 27, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵)) |
33 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵)) |
34 | 33 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑓‘𝑥) ∈ 𝐵) |
35 | | ssel2 3563 |
. . . . . . . . . . 11
⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑀)) |
36 | 35 | ad2antll 761 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑥 ∈ (Base‘𝑀)) |
37 | 14, 15, 17, 16 | lmodvscl 18703 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ LMod ∧ (𝑓‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ (Base‘𝑀)) → ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
38 | 26, 34, 36, 37 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀)) |
39 | | difexg 4735 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑉 → (𝑆 ∖ {𝑥}) ∈ V) |
40 | 39 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ∈ V) |
41 | | ssdifss 3703 |
. . . . . . . . . . . . 13
⊢ (𝑆 ⊆ (Base‘𝑀) → (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)) |
42 | 41 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)) |
43 | 40, 42 | jca 553 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑆 ∖ {𝑥}) ∈ V ∧ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀))) |
44 | 43 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑆 ∖ {𝑥}) ∈ V ∧ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀))) |
45 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod)) |
46 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) → 𝑆 ⊆ (Base‘𝑀)) |
47 | 46 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑆 ⊆ (Base‘𝑀)) |
48 | 7 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑥 ∈ 𝑆) |
49 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) → 𝑓 ∈ (𝐵 ↑𝑚 𝑆)) |
50 | 49 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝑓 ∈ (𝐵 ↑𝑚 𝑆)) |
51 | | lindslinind.z |
. . . . . . . . . . . . 13
⊢ 𝑍 = (0g‘𝑀) |
52 | | lindslinind.y |
. . . . . . . . . . . . 13
⊢ 𝑌 = ((invg‘𝑅)‘(𝑓‘𝑥)) |
53 | 15, 16, 19, 51, 52, 12 | lindslinindimp2lem2 42042 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆 ∧ 𝑓 ∈ (𝐵 ↑𝑚 𝑆))) → 𝐺 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))) |
54 | 45, 47, 48, 50, 53 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥}))) |
55 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) |
56 | 55 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) |
57 | 15, 16, 19, 51, 52, 12 | lindslinindimp2lem3 42043 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 )) → 𝐺 finSupp 0 ) |
58 | 45, 56, 11, 57 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 finSupp 0 ) |
59 | 54, 58 | jca 553 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝐺 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥})) ∧ 𝐺 finSupp 0 )) |
60 | 14, 15, 16, 19 | lincfsuppcl 41996 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ LMod ∧ ((𝑆 ∖ {𝑥}) ∈ V ∧ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀)) ∧ (𝐺 ∈ (𝐵 ↑𝑚 (𝑆 ∖ {𝑥})) ∧ 𝐺 finSupp 0 )) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀)) |
61 | 26, 44, 59, 60 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀)) |
62 | | eqid 2610 |
. . . . . . . . . 10
⊢
(invg‘𝑀) = (invg‘𝑀) |
63 | 14, 18, 51, 62 | grpinvid2 17294 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Grp ∧ ((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥) ∈ (Base‘𝑀) ∧ (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ∈ (Base‘𝑀)) → (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = 𝑍)) |
64 | 25, 38, 61, 63 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥}))(+g‘𝑀)((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = 𝑍)) |
65 | 22, 64 | bitr4d 270 |
. . . . . . 7
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 ↔ ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})))) |
66 | | eqcom 2617 |
. . . . . . . 8
⊢
(((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) ↔ (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥))) |
67 | 15 | fveq2i 6106 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘(Scalar‘𝑀)) |
68 | 16, 67 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ 𝐵 =
(Base‘(Scalar‘𝑀)) |
69 | 68 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ (𝐵 ↑𝑚
(𝑆 ∖ {𝑥})) =
((Base‘(Scalar‘𝑀)) ↑𝑚 (𝑆 ∖ {𝑥})) |
70 | 54, 69 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → 𝐺 ∈ ((Base‘(Scalar‘𝑀)) ↑𝑚
(𝑆 ∖ {𝑥}))) |
71 | | elpwg 4116 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∖ {𝑥}) ∈ V → ((𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀))) |
72 | 40, 71 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀) ↔ (𝑆 ∖ {𝑥}) ⊆ (Base‘𝑀))) |
73 | 42, 72 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀)) |
74 | 73 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀)) |
75 | | lincval 41992 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ LMod ∧ 𝐺 ∈
((Base‘(Scalar‘𝑀)) ↑𝑚 (𝑆 ∖ {𝑥})) ∧ (𝑆 ∖ {𝑥}) ∈ 𝒫 (Base‘𝑀)) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠
‘𝑀)𝑦)))) |
76 | 26, 70, 74, 75 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠
‘𝑀)𝑦)))) |
77 | 76 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) ↔ (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠
‘𝑀)𝑦))) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)))) |
78 | 12 | fveq1i 6104 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺‘𝑦) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦) |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → (𝐺‘𝑦) = ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦)) |
80 | | fvres 6117 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝑆 ∖ {𝑥}) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦) = (𝑓‘𝑦)) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → ((𝑓 ↾ (𝑆 ∖ {𝑥}))‘𝑦) = (𝑓‘𝑦)) |
82 | 79, 81 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → (𝐺‘𝑦) = (𝑓‘𝑦)) |
83 | 82 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) ∧ 𝑦 ∈ (𝑆 ∖ {𝑥})) → ((𝐺‘𝑦)( ·𝑠
‘𝑀)𝑦) = ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦)) |
84 | 83 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠
‘𝑀)𝑦)) = (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) |
85 | 84 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦)))) |
86 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(invg‘𝑅) = (invg‘𝑅) |
87 | 28 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓:𝑆⟶𝐵 → (𝑥 ∈ 𝑆 → (𝑓‘𝑥) ∈ 𝐵)) |
88 | 27, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) → (𝑥 ∈ 𝑆 → (𝑓‘𝑥) ∈ 𝐵)) |
89 | 88 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑆 → (𝑓 ∈ (𝐵 ↑𝑚 𝑆) → (𝑓‘𝑥) ∈ 𝐵)) |
90 | 89 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓 ∈ (𝐵 ↑𝑚 𝑆) → (𝑓‘𝑥) ∈ 𝐵)) |
91 | 90 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵)) |
92 | 91 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑓‘𝑥) ∈ 𝐵)) |
93 | 92 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (𝑓‘𝑥) ∈ 𝐵) |
94 | 14, 15, 17, 62, 16, 86, 26, 36, 93 | lmodvsneg 18730 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥)) |
95 | 52 | eqcomi 2619 |
. . . . . . . . . . . . . 14
⊢
((invg‘𝑅)‘(𝑓‘𝑥)) = 𝑌 |
96 | 95 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑅)‘(𝑓‘𝑥)) = 𝑌) |
97 | 96 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (((invg‘𝑅)‘(𝑓‘𝑥))( ·𝑠
‘𝑀)𝑥) = (𝑌( ·𝑠
‘𝑀)𝑥)) |
98 | 94, 97 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝑌( ·𝑠
‘𝑀)𝑥)) |
99 | 85, 98 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠
‘𝑀)𝑦))) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) ↔ (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥))) |
100 | 99 | biimpd 218 |
. . . . . . . . 9
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝐺‘𝑦)( ·𝑠
‘𝑀)𝑦))) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥))) |
101 | 77, 100 | sylbid 229 |
. . . . . . . 8
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) = ((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥))) |
102 | 66, 101 | syl5bi 231 |
. . . . . . 7
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → (((invg‘𝑀)‘((𝑓‘𝑥)( ·𝑠
‘𝑀)𝑥)) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑥})) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥))) |
103 | 65, 102 | sylbid 229 |
. . . . . 6
⊢ (((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) ∧ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆))) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥))) |
104 | 103 | ex 449 |
. . . . 5
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥)))) |
105 | 104 | com23 84 |
. . . 4
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ) → ((𝑓( linC ‘𝑀)𝑆) = 𝑍 → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥)))) |
106 | 105 | 3impia 1253 |
. . 3
⊢ ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥))) |
107 | 106 | com12 32 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆)) → ((𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥))) |
108 | 107 | 3impia 1253 |
1
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ LMod) ∧ (𝑆 ⊆ (Base‘𝑀) ∧ 𝑥 ∈ 𝑆) ∧ (𝑓 ∈ (𝐵 ↑𝑚 𝑆) ∧ 𝑓 finSupp 0 ∧ (𝑓( linC ‘𝑀)𝑆) = 𝑍)) → (𝑀 Σg (𝑦 ∈ (𝑆 ∖ {𝑥}) ↦ ((𝑓‘𝑦)( ·𝑠
‘𝑀)𝑦))) = (𝑌( ·𝑠
‘𝑀)𝑥)) |