Step | Hyp | Ref
| Expression |
1 | | ioran 984 |
. . . . . 6
⊢ (¬
((𝐴‘𝑥) ≠
(0g‘𝑀)
∨ (𝐵‘𝑥) ≠
(0g‘𝑀))
↔ (¬ (𝐴‘𝑥) ≠ (0g‘𝑀) ∧ ¬ (𝐵‘𝑥) ≠ (0g‘𝑀))) |
2 | | nne 2944 |
. . . . . . 7
⊢ (¬
(𝐴‘𝑥) ≠ (0g‘𝑀) ↔ (𝐴‘𝑥) = (0g‘𝑀)) |
3 | | nne 2944 |
. . . . . . 7
⊢ (¬
(𝐵‘𝑥) ≠ (0g‘𝑀) ↔ (𝐵‘𝑥) = (0g‘𝑀)) |
4 | 2, 3 | anbi12i 630 |
. . . . . 6
⊢ ((¬
(𝐴‘𝑥) ≠ (0g‘𝑀) ∧ ¬ (𝐵‘𝑥) ≠ (0g‘𝑀)) ↔ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) |
5 | 1, 4 | bitri 278 |
. . . . 5
⊢ (¬
((𝐴‘𝑥) ≠
(0g‘𝑀)
∨ (𝐵‘𝑥) ≠
(0g‘𝑀))
↔ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) |
6 | | elmapfn 8546 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 Fn 𝑉) |
7 | 6 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐴 Fn 𝑉) |
8 | 7 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝐴 Fn 𝑉) |
9 | | elmapfn 8546 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵 Fn 𝑉) |
10 | 9 | ad2antll 729 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐵 Fn 𝑉) |
11 | 10 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝐵 Fn 𝑉) |
12 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝑉 ∈ 𝑋) |
13 | 12 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝑉 ∈ 𝑋) |
14 | | inidm 4133 |
. . . . . . . . . 10
⊢ (𝑉 ∩ 𝑉) = 𝑉 |
15 | | simplrl 777 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) = (0g‘𝑀)) |
16 | | simplrr 778 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) = (0g‘𝑀)) |
17 | 8, 11, 13, 13, 14, 15, 16 | ofval 7479 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) = ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀))) |
18 | 17 | an32s 652 |
. . . . . . . 8
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) = ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀))) |
19 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑀) =
(Base‘𝑀) |
20 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑀) = (0g‘𝑀) |
21 | 19, 20 | mndidcl 18188 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ (Base‘𝑀)) |
22 | 21 | ancli 552 |
. . . . . . . . . 10
⊢ (𝑀 ∈ Mnd → (𝑀 ∈ Mnd ∧
(0g‘𝑀)
∈ (Base‘𝑀))) |
23 | 22 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → (𝑀 ∈ Mnd ∧ (0g‘𝑀) ∈ (Base‘𝑀))) |
24 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑀) = (+g‘𝑀) |
25 | 19, 24, 20 | mndlid 18193 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧
(0g‘𝑀)
∈ (Base‘𝑀))
→ ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀)) = (0g‘𝑀)) |
26 | 23, 25 | syl 17 |
. . . . . . . 8
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀)) = (0g‘𝑀)) |
27 | 18, 26 | eqtrd 2777 |
. . . . . . 7
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) = (0g‘𝑀)) |
28 | | nne 2944 |
. . . . . . 7
⊢ (¬
((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀) ↔ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) = (0g‘𝑀)) |
29 | 27, 28 | sylibr 237 |
. . . . . 6
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ¬ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)) |
30 | 29 | ex 416 |
. . . . 5
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀)) → ¬ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀))) |
31 | 5, 30 | syl5bi 245 |
. . . 4
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (¬ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀)) → ¬ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀))) |
32 | 31 | con4d 115 |
. . 3
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀) → ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀)))) |
33 | 32 | ss2rabdv 3989 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))}) |
34 | 7, 10, 12, 12 | offun 7482 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → Fun (𝐴 ∘f
(+g‘𝑀)𝐵)) |
35 | | ovexd 7248 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 ∘f
(+g‘𝑀)𝐵) ∈ V) |
36 | | fvexd 6732 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (0g‘𝑀) ∈ V) |
37 | | suppval1 7909 |
. . . 4
⊢ ((Fun
(𝐴 ∘f
(+g‘𝑀)𝐵) ∧ (𝐴 ∘f
(+g‘𝑀)𝐵) ∈ V ∧ (0g‘𝑀) ∈ V) → ((𝐴 ∘f
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ dom (𝐴 ∘f
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
38 | 34, 35, 36, 37 | syl3anc 1373 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 ∘f
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ dom (𝐴 ∘f
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
39 | 12, 7, 10 | offvalfv 45351 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 ∘f
(+g‘𝑀)𝐵) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)))) |
40 | 39 | dmeqd 5774 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → dom (𝐴 ∘f
(+g‘𝑀)𝐵) = dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)))) |
41 | | ovex 7246 |
. . . . . 6
⊢ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)) ∈ V |
42 | | eqid 2737 |
. . . . . 6
⊢ (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) |
43 | 41, 42 | dmmpti 6522 |
. . . . 5
⊢ dom
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) = 𝑉 |
44 | 40, 43 | eqtrdi 2794 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → dom (𝐴 ∘f
(+g‘𝑀)𝐵) = 𝑉) |
45 | 44 | rabeqdv 3395 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → {𝑥 ∈ dom (𝐴 ∘f
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
46 | 38, 45 | eqtrd 2777 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 ∘f
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
47 | | elmapfun 8547 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → Fun 𝐴) |
48 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 ∈ (𝑅 ↑m 𝑉)) |
49 | | fvexd 6732 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (0g‘𝑀) ∈ V) |
50 | | suppval1 7909 |
. . . . . . 7
⊢ ((Fun
𝐴 ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ (0g‘𝑀) ∈ V) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
51 | 47, 48, 49, 50 | syl3anc 1373 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
52 | | elmapi 8530 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴:𝑉⟶𝑅) |
53 | | fdm 6554 |
. . . . . . 7
⊢ (𝐴:𝑉⟶𝑅 → dom 𝐴 = 𝑉) |
54 | | rabeq 3394 |
. . . . . . 7
⊢ (dom
𝐴 = 𝑉 → {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
55 | 52, 53, 54 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
56 | 51, 55 | eqtrd 2777 |
. . . . 5
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
57 | 56 | ad2antrl 728 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
58 | | elmapfun 8547 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → Fun 𝐵) |
59 | 58 | ad2antll 729 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → Fun 𝐵) |
60 | | simprr 773 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐵 ∈ (𝑅 ↑m 𝑉)) |
61 | | suppval1 7909 |
. . . . . 6
⊢ ((Fun
𝐵 ∧ 𝐵 ∈ (𝑅 ↑m 𝑉) ∧ (0g‘𝑀) ∈ V) → (𝐵 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
62 | 59, 60, 36, 61 | syl3anc 1373 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐵 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
63 | | elmapi 8530 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵:𝑉⟶𝑅) |
64 | 63 | fdmd 6556 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → dom 𝐵 = 𝑉) |
65 | 64 | ad2antll 729 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → dom 𝐵 = 𝑉) |
66 | 65 | rabeqdv 3395 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
67 | 62, 66 | eqtrd 2777 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐵 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
68 | 57, 67 | uneq12d 4078 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))) = ({𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} ∪ {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)})) |
69 | | unrab 4220 |
. . 3
⊢ ({𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} ∪ {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) = {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))} |
70 | 68, 69 | eqtrdi 2794 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))) = {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))}) |
71 | 33, 46, 70 | 3sstr4d 3948 |
1
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 ∘f
(+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀)))) |