Proof of Theorem gsumlsscl
Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
⊢
(0g‘𝑀) = (0g‘𝑀) |
2 | | lmodabl 19951 |
. . . . 5
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Abel) |
3 | 2 | 3ad2ant1 1135 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑀 ∈ Abel) |
4 | 3 | adantr 484 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝑀 ∈ Abel) |
5 | | ssexg 5221 |
. . . . . 6
⊢ ((𝑉 ⊆ 𝑍 ∧ 𝑍 ∈ 𝑆) → 𝑉 ∈ V) |
6 | 5 | ancoms 462 |
. . . . 5
⊢ ((𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑉 ∈ V) |
7 | 6 | 3adant1 1132 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑉 ∈ V) |
8 | 7 | adantr 484 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝑉 ∈ V) |
9 | | 3simpa 1150 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → (𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆)) |
10 | | gsumlsscl.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑀) |
11 | 10 | lsssubg 19999 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆) → 𝑍 ∈ (SubGrp‘𝑀)) |
12 | 9, 11 | syl 17 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑍 ∈ (SubGrp‘𝑀)) |
13 | 12 | adantr 484 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝑍 ∈ (SubGrp‘𝑀)) |
14 | 9 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆)) |
15 | 14 | adantr 484 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) ∧ 𝑣 ∈ 𝑉) → (𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆)) |
16 | | elmapi 8535 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐵 ↑m 𝑉) → 𝐹:𝑉⟶𝐵) |
17 | | ffvelrn 6907 |
. . . . . . . . 9
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) ∈ 𝐵) |
18 | 17 | ex 416 |
. . . . . . . 8
⊢ (𝐹:𝑉⟶𝐵 → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝐵)) |
19 | 16, 18 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐵 ↑m 𝑉) → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝐵)) |
20 | 19 | ad2antrl 728 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑣 ∈ 𝑉 → (𝐹‘𝑣) ∈ 𝐵)) |
21 | 20 | imp 410 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) ∧ 𝑣 ∈ 𝑉) → (𝐹‘𝑣) ∈ 𝐵) |
22 | | ssel 3898 |
. . . . . . . 8
⊢ (𝑉 ⊆ 𝑍 → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍)) |
23 | 22 | 3ad2ant3 1137 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍)) |
24 | 23 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑣 ∈ 𝑉 → 𝑣 ∈ 𝑍)) |
25 | 24 | imp 410 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑍) |
26 | | gsumlsscl.r |
. . . . . 6
⊢ 𝑅 = (Scalar‘𝑀) |
27 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
28 | | gsumlsscl.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
29 | 26, 27, 28, 10 | lssvscl 19997 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆) ∧ ((𝐹‘𝑣) ∈ 𝐵 ∧ 𝑣 ∈ 𝑍)) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝑍) |
30 | 15, 21, 25, 29 | syl12anc 837 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) ∧ 𝑣 ∈ 𝑉) → ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣) ∈ 𝑍) |
31 | 30 | fmpttd 6937 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)):𝑉⟶𝑍) |
32 | | simp1 1138 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑀 ∈ LMod) |
33 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑀) =
(Base‘𝑀) |
34 | 33, 10 | lssss 19978 |
. . . . . . . . . 10
⊢ (𝑍 ∈ 𝑆 → 𝑍 ⊆ (Base‘𝑀)) |
35 | | sstr 3914 |
. . . . . . . . . . 11
⊢ ((𝑉 ⊆ 𝑍 ∧ 𝑍 ⊆ (Base‘𝑀)) → 𝑉 ⊆ (Base‘𝑀)) |
36 | 35 | expcom 417 |
. . . . . . . . . 10
⊢ (𝑍 ⊆ (Base‘𝑀) → (𝑉 ⊆ 𝑍 → 𝑉 ⊆ (Base‘𝑀))) |
37 | 34, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝑍 ∈ 𝑆 → (𝑉 ⊆ 𝑍 → 𝑉 ⊆ (Base‘𝑀))) |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (𝑀 ∈ LMod → (𝑍 ∈ 𝑆 → (𝑉 ⊆ 𝑍 → 𝑉 ⊆ (Base‘𝑀)))) |
39 | 38 | 3imp 1113 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑉 ⊆ (Base‘𝑀)) |
40 | | elpwg 4521 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (𝑉 ∈ 𝒫
(Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
41 | 7, 40 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → (𝑉 ∈ 𝒫 (Base‘𝑀) ↔ 𝑉 ⊆ (Base‘𝑀))) |
42 | 39, 41 | mpbird 260 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → 𝑉 ∈ 𝒫 (Base‘𝑀)) |
43 | 32, 42 | jca 515 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
44 | 43 | adantr 484 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 (Base‘𝑀))) |
45 | | simprl 771 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝐹 ∈ (𝐵 ↑m 𝑉)) |
46 | | simprr 773 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → 𝐹 finSupp (0g‘𝑅)) |
47 | 26, 28 | scmfsupp 45395 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫
(Base‘𝑀)) ∧ 𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
48 | 44, 45, 46, 47 | syl3anc 1373 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣)) finSupp (0g‘𝑀)) |
49 | 1, 4, 8, 13, 31, 48 | gsumsubgcl 19310 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) ∧ (𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅))) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) ∈ 𝑍) |
50 | 49 | ex 416 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑍 ∈ 𝑆 ∧ 𝑉 ⊆ 𝑍) → ((𝐹 ∈ (𝐵 ↑m 𝑉) ∧ 𝐹 finSupp (0g‘𝑅)) → (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝐹‘𝑣)( ·𝑠
‘𝑀)𝑣))) ∈ 𝑍)) |