Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . 7
⊢ ((𝐴‘𝑤) = (0g‘𝑀) → (𝐶(.r‘𝑀)(𝐴‘𝑤)) = (𝐶(.r‘𝑀)(0g‘𝑀))) |
2 | | simpll1 1100 |
. . . . . . . 8
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → 𝑀 ∈ Ring) |
3 | | simpll3 1102 |
. . . . . . . 8
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → 𝐶 ∈ 𝑅) |
4 | | rmsuppss.r |
. . . . . . . . 9
⊢ 𝑅 = (Base‘𝑀) |
5 | | eqid 2622 |
. . . . . . . . 9
⊢
(.r‘𝑀) = (.r‘𝑀) |
6 | | eqid 2622 |
. . . . . . . . 9
⊢
(0g‘𝑀) = (0g‘𝑀) |
7 | 4, 5, 6 | ringrz 18588 |
. . . . . . . 8
⊢ ((𝑀 ∈ Ring ∧ 𝐶 ∈ 𝑅) → (𝐶(.r‘𝑀)(0g‘𝑀)) = (0g‘𝑀)) |
8 | 2, 3, 7 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → (𝐶(.r‘𝑀)(0g‘𝑀)) = (0g‘𝑀)) |
9 | 1, 8 | sylan9eqr 2678 |
. . . . . 6
⊢
(((((𝑀 ∈ Ring
∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) ∧ (𝐴‘𝑤) = (0g‘𝑀)) → (𝐶(.r‘𝑀)(𝐴‘𝑤)) = (0g‘𝑀)) |
10 | 9 | ex 450 |
. . . . 5
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → ((𝐴‘𝑤) = (0g‘𝑀) → (𝐶(.r‘𝑀)(𝐴‘𝑤)) = (0g‘𝑀))) |
11 | 10 | necon3d 2815 |
. . . 4
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → ((𝐶(.r‘𝑀)(𝐴‘𝑤)) ≠ (0g‘𝑀) → (𝐴‘𝑤) ≠ (0g‘𝑀))) |
12 | 11 | ss2rabdv 3683 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → {𝑤 ∈ 𝑉 ∣ (𝐶(.r‘𝑀)(𝐴‘𝑤)) ≠ (0g‘𝑀)} ⊆ {𝑤 ∈ 𝑉 ∣ (𝐴‘𝑤) ≠ (0g‘𝑀)}) |
13 | | elmapi 7879 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴:𝑉⟶𝑅) |
14 | | fdm 6051 |
. . . . . 6
⊢ (𝐴:𝑉⟶𝑅 → dom 𝐴 = 𝑉) |
15 | 13, 14 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → dom 𝐴 = 𝑉) |
16 | 15 | adantl 482 |
. . . 4
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → dom 𝐴 = 𝑉) |
17 | | rabeq 3192 |
. . . 4
⊢ (dom
𝐴 = 𝑉 → {𝑤 ∈ dom 𝐴 ∣ (𝐴‘𝑤) ≠ (0g‘𝑀)} = {𝑤 ∈ 𝑉 ∣ (𝐴‘𝑤) ≠ (0g‘𝑀)}) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → {𝑤 ∈ dom 𝐴 ∣ (𝐴‘𝑤) ≠ (0g‘𝑀)} = {𝑤 ∈ 𝑉 ∣ (𝐴‘𝑤) ≠ (0g‘𝑀)}) |
19 | 12, 18 | sseqtr4d 3642 |
. 2
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → {𝑤 ∈ 𝑉 ∣ (𝐶(.r‘𝑀)(𝐴‘𝑤)) ≠ (0g‘𝑀)} ⊆ {𝑤 ∈ dom 𝐴 ∣ (𝐴‘𝑤) ≠ (0g‘𝑀)}) |
20 | | fveq2 6191 |
. . . . 5
⊢ (𝑣 = 𝑤 → (𝐴‘𝑣) = (𝐴‘𝑤)) |
21 | 20 | oveq2d 6666 |
. . . 4
⊢ (𝑣 = 𝑤 → (𝐶(.r‘𝑀)(𝐴‘𝑣)) = (𝐶(.r‘𝑀)(𝐴‘𝑤))) |
22 | 21 | cbvmptv 4750 |
. . 3
⊢ (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) = (𝑤 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑤))) |
23 | | simpl2 1065 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑉 ∈ 𝑋) |
24 | | fvexd 6203 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) →
(0g‘𝑀)
∈ V) |
25 | | ovexd 6680 |
. . 3
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → (𝐶(.r‘𝑀)(𝐴‘𝑤)) ∈ V) |
26 | 22, 23, 24, 25 | mptsuppd 7318 |
. 2
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = {𝑤 ∈ 𝑉 ∣ (𝐶(.r‘𝑀)(𝐴‘𝑤)) ≠ (0g‘𝑀)}) |
27 | | elmapfun 7881 |
. . . 4
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → Fun 𝐴) |
28 | 27 | adantl 482 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → Fun 𝐴) |
29 | | simpr 477 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) |
30 | | suppval1 7301 |
. . 3
⊢ ((Fun
𝐴 ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧
(0g‘𝑀)
∈ V) → (𝐴 supp
(0g‘𝑀)) =
{𝑤 ∈ dom 𝐴 ∣ (𝐴‘𝑤) ≠ (0g‘𝑀)}) |
31 | 28, 29, 24, 30 | syl3anc 1326 |
. 2
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → (𝐴 supp (0g‘𝑀)) = {𝑤 ∈ dom 𝐴 ∣ (𝐴‘𝑤) ≠ (0g‘𝑀)}) |
32 | 19, 26, 31 | 3sstr4d 3648 |
1
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 ∈ 𝑅) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) ⊆ (𝐴 supp (0g‘𝑀))) |