Proof of Theorem gsumlsscl
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
2 | | lmodabl 18910 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Abel) |
3 | 2 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑀 ∈ Abel) |
4 | 3 | adantr 481 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝑀 ∈ Abel) |
5 | | ssexg 4804 |
. . . . . 6
⊢ ((𝑉 ⊆ 𝑍 ∧ 𝑍 ∈ 𝑆) → 𝑉 ∈ V) |
6 | 5 | ancoms 469 |
. . . . 5
⊢ ((𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑉 ∈ V) |
7 | 6 | 3adant1 1079 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑉 ∈ V) |
8 | 7 | adantr 481 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝑉 ∈ V) |
9 | | 3simpa 1058 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → (𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆)) |
10 | | gsumlsscl.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑀) |
11 | 10 | lsssubg 18957 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆) → 𝑍 ∈ (SubGrp‘𝑀)) |
12 | 9, 11 | syl 17 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑍 ∈ (SubGrp‘𝑀)) |
13 | 12 | adantr 481 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝑍 ∈ (SubGrp‘𝑀)) |
14 | 9 | adantr 481 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆)) |
15 | 14 | adantr 481 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) ∧ 𝑣 ∈ 𝑉) → (𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆)) |
16 | | elmapi 7879 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) → 𝐹:𝑉⟶𝐵) |
17 | | ffvelrn 6357 |
. . . . . . . . 9
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) ∈ 𝐵) |
18 | 17 | ex 450 |
. . . . . . . 8
⊢ (𝐹:𝑉⟶𝐵 → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝐵)) |
19 | 16, 18 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝐵)) |
20 | 19 | ad2antrl 764 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝐵)) |
21 | 20 | imp 445 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) ∈ 𝐵) |
22 | | ssel 3597 |
. . . . . . . 8
⊢ (𝑉 ⊆ 𝑍 → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍)) |
23 | 22 | 3ad2ant3 1084 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍)) |
24 | 23 | adantr 481 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍)) |
25 | 24 | imp 445 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑍) |
26 | | gsumlsscl.r |
. . . . . 6
⊢ 𝑅 = (Scalar‘𝑀) |
27 | | eqid 2622 |
. . . . . 6
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
28 | | gsumlsscl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
29 | 26, 27, 28, 10 | lssvscl 18955 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆) ∧ ((𝐹‘𝑣) ∈ 𝐵 ∧ 𝑣 ∈ 𝑍)) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝑍) |
30 | 15, 21, 25, 29 | syl12anc 1324 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝑍) |
31 | | eqid 2622 |
. . . 4
⊢ (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) = (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) |
32 | 30, 31 | fmptd 6385 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)):𝑉⟶𝑍) |
33 | | simp1 1061 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑀 ∈ LMod) |
34 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝑀) =
(Base‘𝑀) |
35 | 34, 10 | lssss 18937 |
. . . . . . . . . 10
⊢ (𝑍 ∈ 𝑆 → 𝑍 ⊆ (Base‘𝑀)) |
36 | | sstr 3611 |
. . . . . . . . . . 11
⊢ ((𝑉 ⊆ 𝑍 ∧ 𝑍 ⊆ (Base‘𝑀)) → 𝑉 ⊆ (Base‘𝑀)) |
37 | 36 | expcom 451 |
. . . . . . . . . 10
⊢ (𝑍 ⊆ (Base‘𝑀) → (𝑉 ⊆ 𝑍 → 𝑉 ⊆ (Base‘𝑀))) |
38 | 35, 37 | syl 17 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑆 → (𝑉 ⊆ 𝑍 → 𝑉 ⊆ (Base‘𝑀))) |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ (𝑀 ∈ LMod → (𝑍 ∈ 𝑆 → (𝑉 ⊆ 𝑍 → 𝑉 ⊆ (Base‘𝑀)))) |
40 | 39 | 3imp 1256 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑉 ⊆ (Base‘𝑀)) |
41 | | elpwg 4166 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (𝑉 ∈ 𝒫
(Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
42 | 7, 41 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → (𝑉 ∈ 𝒫 (Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
43 | 40, 42 | mpbird 247 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
44 | 33, 43 | jca 554 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
45 | 44 | adantr 481 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
46 | | simprl 794 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝐹 ∈ (𝐵 ↑𝑚 𝑉)) |
47 | | simprr 796 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝐹 finSupp (0g‘𝑅)) |
48 | 26, 28 | scmfsupp 42159 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
49 | 45, 46, 47, 48 | syl3anc 1326 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
50 | 1, 4, 8, 13, 32, 49 | gsumsubgcl 18320 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) ∈ 𝑍) |
51 | 50 | ex 450 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → ((𝐹 ∈ (𝐵 ↑𝑚 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) ∈ 𝑍)) |