| Step | Hyp | Ref
| Expression |
| 1 | | ioran 986 |
. . . . . 6
⊢ (¬
((𝐴‘𝑥) ≠
(0g‘𝑀)
∨ (𝐵‘𝑥) ≠
(0g‘𝑀))
↔ (¬ (𝐴‘𝑥) ≠ (0g‘𝑀) ∧ ¬ (𝐵‘𝑥) ≠ (0g‘𝑀))) |
| 2 | | nne 2944 |
. . . . . . 7
⊢ (¬
(𝐴‘𝑥) ≠ (0g‘𝑀) ↔ (𝐴‘𝑥) = (0g‘𝑀)) |
| 3 | | nne 2944 |
. . . . . . 7
⊢ (¬
(𝐵‘𝑥) ≠ (0g‘𝑀) ↔ (𝐵‘𝑥) = (0g‘𝑀)) |
| 4 | 2, 3 | anbi12i 628 |
. . . . . 6
⊢ ((¬
(𝐴‘𝑥) ≠ (0g‘𝑀) ∧ ¬ (𝐵‘𝑥) ≠ (0g‘𝑀)) ↔ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) |
| 5 | 1, 4 | bitri 275 |
. . . . 5
⊢ (¬
((𝐴‘𝑥) ≠
(0g‘𝑀)
∨ (𝐵‘𝑥) ≠
(0g‘𝑀))
↔ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) |
| 6 | | elmapfn 8905 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 Fn 𝑉) |
| 7 | 6 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐴 Fn 𝑉) |
| 8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝐴 Fn 𝑉) |
| 9 | | elmapfn 8905 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵 Fn 𝑉) |
| 10 | 9 | ad2antll 729 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐵 Fn 𝑉) |
| 11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝐵 Fn 𝑉) |
| 12 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝑉 ∈ 𝑋) |
| 13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝑉 ∈ 𝑋) |
| 14 | | inidm 4227 |
. . . . . . . . . 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 7708 |
. . . . . . . . 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 18762 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ (Base‘𝑀)) |
| 22 | 21 | ancli 548 |
. . . . . . . . . 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 18767 |
. . . . . . . . 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 234 |
. . . . . 6
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ¬ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)) |
| 30 | 29 | ex 412 |
. . . . 5
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀)) → ¬ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀))) |
| 31 | 5, 30 | biimtrid 242 |
. . . 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 4076 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘f
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))}) |
| 34 | 7, 10, 12, 12 | offun 7711 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → Fun (𝐴 ∘f
(+g‘𝑀)𝐵)) |
| 35 | | ovexd 7466 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 ∘f
(+g‘𝑀)𝐵) ∈ V) |
| 36 | | fvexd 6921 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (0g‘𝑀) ∈ V) |
| 37 | | suppval1 8191 |
. . . 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 7719 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐴 ∘f
(+g‘𝑀)𝐵) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)))) |
| 40 | 39 | dmeqd 5916 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → dom (𝐴 ∘f
(+g‘𝑀)𝐵) = dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)))) |
| 41 | | ovex 7464 |
. . . . . 6
⊢ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)) ∈ V |
| 42 | | eqid 2737 |
. . . . . 6
⊢ (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) |
| 43 | 41, 42 | dmmpti 6712 |
. . . . 5
⊢ dom
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) = 𝑉 |
| 44 | 40, 43 | eqtrdi 2793 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → dom (𝐴 ∘f
(+g‘𝑀)𝐵) = 𝑉) |
| 45 | 44 | rabeqdv 3452 |
. . 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 8906 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → Fun 𝐴) |
| 48 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴 ∈ (𝑅 ↑m 𝑉)) |
| 49 | | fvexd 6921 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (0g‘𝑀) ∈ V) |
| 50 | | suppval1 8191 |
. . . . . . 7
⊢ ((Fun
𝐴 ∧ 𝐴 ∈ (𝑅 ↑m 𝑉) ∧ (0g‘𝑀) ∈ V) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
| 51 | 47, 48, 49, 50 | syl3anc 1373 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
| 52 | | elmapi 8889 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑m 𝑉) → 𝐴:𝑉⟶𝑅) |
| 53 | | fdm 6745 |
. . . . . . 7
⊢ (𝐴:𝑉⟶𝑅 → dom 𝐴 = 𝑉) |
| 54 | | rabeq 3451 |
. . . . . . 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 8906 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → Fun 𝐵) |
| 59 | 58 | ad2antll 729 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → Fun 𝐵) |
| 60 | | simprr 773 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → 𝐵 ∈ (𝑅 ↑m 𝑉)) |
| 61 | | suppval1 8191 |
. . . . . 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 8889 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → 𝐵:𝑉⟶𝑅) |
| 64 | 63 | fdmd 6746 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑m 𝑉) → dom 𝐵 = 𝑉) |
| 65 | 64 | ad2antll 729 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → dom 𝐵 = 𝑉) |
| 66 | 65 | rabeqdv 3452 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
| 67 | 62, 66 | eqtrd 2777 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → (𝐵 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
| 68 | 57, 67 | uneq12d 4169 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))) = ({𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} ∪ {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)})) |
| 69 | | unrab 4315 |
. . 3
⊢ ({𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} ∪ {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) = {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))} |
| 70 | 68, 69 | eqtrdi 2793 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))) = {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))}) |
| 71 | 33, 46, 70 | 3sstr4d 4039 |
1
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 ∘f
(+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀)))) |