Proof of Theorem lincext3
Step | Hyp | Ref
| Expression |
1 | | simp1l 1085 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → 𝑀 ∈ LMod) |
2 | | simp1r 1086 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → 𝑆 ∈ 𝒫 𝐵) |
3 | | simp2 1062 |
. . . 4
⊢ ((𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) → 𝑋 ∈ 𝑆) |
4 | 3 | 3ad2ant2 1083 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → 𝑋 ∈ 𝑆) |
5 | | lincext.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑀) |
6 | | lincext.r |
. . . . 5
⊢ 𝑅 = (Scalar‘𝑀) |
7 | | lincext.e |
. . . . 5
⊢ 𝐸 = (Base‘𝑅) |
8 | | lincext.0 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
9 | | lincext.z |
. . . . 5
⊢ 𝑍 = (0g‘𝑀) |
10 | | lincext.n |
. . . . 5
⊢ 𝑁 = (invg‘𝑅) |
11 | | lincext.f |
. . . . 5
⊢ 𝐹 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧))) |
12 | 5, 6, 7, 8, 9, 10,
11 | lincext1 42243 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → 𝐹 ∈ (𝐸 ↑𝑚 𝑆)) |
13 | 12 | 3adant3 1081 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → 𝐹 ∈ (𝐸 ↑𝑚 𝑆)) |
14 | 5, 6, 7, 8, 9, 10,
11 | lincext2 42244 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ 𝐺 finSupp 0 ) → 𝐹 finSupp 0 ) |
15 | 14 | 3adant3r 1323 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → 𝐹 finSupp 0 ) |
16 | | elmapi 7879 |
. . . . . 6
⊢ (𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})) → 𝐺:(𝑆 ∖ {𝑋})⟶𝐸) |
17 | 11 | fdmdifeqresdif 42120 |
. . . . . 6
⊢ (𝐺:(𝑆 ∖ {𝑋})⟶𝐸 → 𝐺 = (𝐹 ↾ (𝑆 ∖ {𝑋}))) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})) → 𝐺 = (𝐹 ↾ (𝑆 ∖ {𝑋}))) |
19 | 18 | 3ad2ant3 1084 |
. . . 4
⊢ ((𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) → 𝐺 = (𝐹 ↾ (𝑆 ∖ {𝑋}))) |
20 | 19 | 3ad2ant2 1083 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → 𝐺 = (𝐹 ↾ (𝑆 ∖ {𝑋}))) |
21 | | eqid 2622 |
. . . 4
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
22 | | eqid 2622 |
. . . 4
⊢
(+g‘𝑀) = (+g‘𝑀) |
23 | 5, 6, 7, 21, 22, 8 | lincdifsn 42213 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵 ∧ 𝑋 ∈ 𝑆) ∧ (𝐹 ∈ (𝐸 ↑𝑚 𝑆) ∧ 𝐹 finSupp 0 ) ∧ 𝐺 = (𝐹 ↾ (𝑆 ∖ {𝑋}))) → (𝐹( linC ‘𝑀)𝑆) = ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋}))(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋))) |
24 | 1, 2, 4, 13, 15, 20, 23 | syl321anc 1348 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → (𝐹( linC ‘𝑀)𝑆) = ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋}))(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋))) |
25 | | oveq1 6657 |
. . . . . 6
⊢ ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})) = (𝑌( ·𝑠
‘𝑀)𝑋) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋}))(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) = ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋))) |
26 | 25 | eqcoms 2630 |
. . . . 5
⊢ ((𝑌(
·𝑠 ‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋}))(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) = ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋))) |
27 | 26 | adantl 482 |
. . . 4
⊢ ((𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋}))) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋}))(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) = ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋))) |
28 | 27 | 3ad2ant3 1084 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋}))(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) = ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋))) |
29 | | eqid 2622 |
. . . . . . . 8
⊢
(invg‘𝑀) = (invg‘𝑀) |
30 | | simpll 790 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → 𝑀 ∈ LMod) |
31 | | elelpwi 4171 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑆 ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑋 ∈ 𝐵) |
32 | 31 | expcom 451 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ 𝒫 𝐵 → (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵)) |
33 | 32 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) → (𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵)) |
34 | 33 | com12 32 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝑆 → ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑋 ∈ 𝐵)) |
35 | 34 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) → ((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) → 𝑋 ∈ 𝐵)) |
36 | 35 | impcom 446 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → 𝑋 ∈ 𝐵) |
37 | | simpr1 1067 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → 𝑌 ∈ 𝐸) |
38 | 5, 6, 21, 29, 7, 10, 30, 36, 37 | lmodvsneg 18907 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → ((invg‘𝑀)‘(𝑌( ·𝑠
‘𝑀)𝑋)) = ((𝑁‘𝑌)( ·𝑠
‘𝑀)𝑋)) |
39 | 11 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → 𝐹 = (𝑧 ∈ 𝑆 ↦ if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧)))) |
40 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑋 → if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧)) = (𝑁‘𝑌)) |
41 | 40 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) ∧ 𝑧 = 𝑋) → if(𝑧 = 𝑋, (𝑁‘𝑌), (𝐺‘𝑧)) = (𝑁‘𝑌)) |
42 | 3 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → 𝑋 ∈ 𝑆) |
43 | | fvexd 6203 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → (𝑁‘𝑌) ∈ V) |
44 | 39, 41, 42, 43 | fvmptd 6288 |
. . . . . . . . 9
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → (𝐹‘𝑋) = (𝑁‘𝑌)) |
45 | 44 | eqcomd 2628 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → (𝑁‘𝑌) = (𝐹‘𝑋)) |
46 | 45 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → ((𝑁‘𝑌)( ·𝑠
‘𝑀)𝑋) = ((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) |
47 | 38, 46 | eqtr2d 2657 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → ((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋) = ((invg‘𝑀)‘(𝑌( ·𝑠
‘𝑀)𝑋))) |
48 | 47 | oveq2d 6666 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) = ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((invg‘𝑀)‘(𝑌( ·𝑠
‘𝑀)𝑋)))) |
49 | 5, 6, 21, 7 | lmodvscl 18880 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝐵) → (𝑌( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) |
50 | 30, 37, 36, 49 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → (𝑌( ·𝑠
‘𝑀)𝑋) ∈ 𝐵) |
51 | 5, 22, 9, 29 | lmodvnegid 18905 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑌(
·𝑠 ‘𝑀)𝑋) ∈ 𝐵) → ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((invg‘𝑀)‘(𝑌( ·𝑠
‘𝑀)𝑋))) = 𝑍) |
52 | 30, 50, 51 | syl2anc 693 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((invg‘𝑀)‘(𝑌( ·𝑠
‘𝑀)𝑋))) = 𝑍) |
53 | 48, 52 | eqtrd 2656 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋})))) → ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) = 𝑍) |
54 | 53 | 3adant3 1081 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → ((𝑌( ·𝑠
‘𝑀)𝑋)(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) = 𝑍) |
55 | 28, 54 | eqtrd 2656 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → ((𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋}))(+g‘𝑀)((𝐹‘𝑋)( ·𝑠
‘𝑀)𝑋)) = 𝑍) |
56 | 24, 55 | eqtrd 2656 |
1
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ 𝒫 𝐵) ∧ (𝑌 ∈ 𝐸 ∧ 𝑋 ∈ 𝑆 ∧ 𝐺 ∈ (𝐸 ↑𝑚 (𝑆 ∖ {𝑋}))) ∧ (𝐺 finSupp 0 ∧ (𝑌( ·𝑠
‘𝑀)𝑋) = (𝐺( linC ‘𝑀)(𝑆 ∖ {𝑋})))) → (𝐹( linC ‘𝑀)𝑆) = 𝑍) |