Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑣 = 𝑤 → (𝐴‘𝑣) = (𝐴‘𝑤)) |
2 | 1 | oveq2d 6565 |
. . . 4
⊢ (𝑣 = 𝑤 → (𝐶(.r‘𝑀)(𝐴‘𝑣)) = (𝐶(.r‘𝑀)(𝐴‘𝑤))) |
3 | 2 | cbvmptv 4678 |
. . 3
⊢ (𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) = (𝑤 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑤))) |
4 | | simpl2 1058 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑉 ∈ 𝑋) |
5 | | fvex 6113 |
. . . 4
⊢
(0g‘𝑀) ∈ V |
6 | 5 | a1i 11 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) →
(0g‘𝑀)
∈ V) |
7 | | ovex 6577 |
. . . 4
⊢ (𝐶(.r‘𝑀)(𝐴‘𝑤)) ∈ V |
8 | 7 | a1i 11 |
. . 3
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → (𝐶(.r‘𝑀)(𝐴‘𝑤)) ∈ V) |
9 | 3, 4, 6, 8 | mptsuppd 7205 |
. 2
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = {𝑤 ∈ 𝑉 ∣ (𝐶(.r‘𝑀)(𝐴‘𝑤)) ≠ (0g‘𝑀)}) |
10 | | simpll3 1095 |
. . . . . 6
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → 𝐶 = (0g‘𝑀)) |
11 | 10 | oveq1d 6564 |
. . . . 5
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → (𝐶(.r‘𝑀)(𝐴‘𝑤)) = ((0g‘𝑀)(.r‘𝑀)(𝐴‘𝑤))) |
12 | | simpll1 1093 |
. . . . . 6
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → 𝑀 ∈ Ring) |
13 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴:𝑉⟶𝑅) |
14 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑤 ∈ 𝑉) → (𝐴‘𝑤) ∈ 𝑅) |
15 | | rmsuppss.r |
. . . . . . . . . . 11
⊢ 𝑅 = (Base‘𝑀) |
16 | 14, 15 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ ((𝐴:𝑉⟶𝑅 ∧ 𝑤 ∈ 𝑉) → (𝐴‘𝑤) ∈ (Base‘𝑀)) |
17 | 16 | ex 449 |
. . . . . . . . 9
⊢ (𝐴:𝑉⟶𝑅 → (𝑤 ∈ 𝑉 → (𝐴‘𝑤) ∈ (Base‘𝑀))) |
18 | 13, 17 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝑤 ∈ 𝑉 → (𝐴‘𝑤) ∈ (Base‘𝑀))) |
19 | 18 | adantl 481 |
. . . . . . 7
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑤 ∈ 𝑉 → (𝐴‘𝑤) ∈ (Base‘𝑀))) |
20 | 19 | imp 444 |
. . . . . 6
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → (𝐴‘𝑤) ∈ (Base‘𝑀)) |
21 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑀) =
(Base‘𝑀) |
22 | | eqid 2610 |
. . . . . . 7
⊢
(.r‘𝑀) = (.r‘𝑀) |
23 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑀) = (0g‘𝑀) |
24 | 21, 22, 23 | ringlz 18410 |
. . . . . 6
⊢ ((𝑀 ∈ Ring ∧ (𝐴‘𝑤) ∈ (Base‘𝑀)) → ((0g‘𝑀)(.r‘𝑀)(𝐴‘𝑤)) = (0g‘𝑀)) |
25 | 12, 20, 24 | syl2anc 691 |
. . . . 5
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → ((0g‘𝑀)(.r‘𝑀)(𝐴‘𝑤)) = (0g‘𝑀)) |
26 | 11, 25 | eqtrd 2644 |
. . . 4
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → (𝐶(.r‘𝑀)(𝐴‘𝑤)) = (0g‘𝑀)) |
27 | 26 | neeq1d 2841 |
. . 3
⊢ ((((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) ∧ 𝑤 ∈ 𝑉) → ((𝐶(.r‘𝑀)(𝐴‘𝑤)) ≠ (0g‘𝑀) ↔
(0g‘𝑀)
≠ (0g‘𝑀))) |
28 | 27 | rabbidva 3163 |
. 2
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → {𝑤 ∈ 𝑉 ∣ (𝐶(.r‘𝑀)(𝐴‘𝑤)) ≠ (0g‘𝑀)} = {𝑤 ∈ 𝑉 ∣ (0g‘𝑀) ≠
(0g‘𝑀)}) |
29 | | neirr 2791 |
. . . . 5
⊢ ¬
(0g‘𝑀)
≠ (0g‘𝑀) |
30 | 29 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ¬
(0g‘𝑀)
≠ (0g‘𝑀)) |
31 | 30 | ralrimivw 2950 |
. . 3
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ∀𝑤 ∈ 𝑉 ¬ (0g‘𝑀) ≠
(0g‘𝑀)) |
32 | | rabeq0 3911 |
. . 3
⊢ ({𝑤 ∈ 𝑉 ∣ (0g‘𝑀) ≠
(0g‘𝑀)} =
∅ ↔ ∀𝑤
∈ 𝑉 ¬
(0g‘𝑀)
≠ (0g‘𝑀)) |
33 | 31, 32 | sylibr 223 |
. 2
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → {𝑤 ∈ 𝑉 ∣ (0g‘𝑀) ≠
(0g‘𝑀)} =
∅) |
34 | 9, 28, 33 | 3eqtrd 2648 |
1
⊢ (((𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = (0g‘𝑀)) ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) → ((𝑣 ∈ 𝑉 ↦ (𝐶(.r‘𝑀)(𝐴‘𝑣))) supp (0g‘𝑀)) = ∅) |