Step | Hyp | Ref
| Expression |
1 | | ioran 511 |
. . . . . 6
⊢ (¬
((𝐴‘𝑥) ≠
(0g‘𝑀)
∨ (𝐵‘𝑥) ≠
(0g‘𝑀))
↔ (¬ (𝐴‘𝑥) ≠ (0g‘𝑀) ∧ ¬ (𝐵‘𝑥) ≠ (0g‘𝑀))) |
2 | | nne 2798 |
. . . . . . 7
⊢ (¬
(𝐴‘𝑥) ≠ (0g‘𝑀) ↔ (𝐴‘𝑥) = (0g‘𝑀)) |
3 | | nne 2798 |
. . . . . . 7
⊢ (¬
(𝐵‘𝑥) ≠ (0g‘𝑀) ↔ (𝐵‘𝑥) = (0g‘𝑀)) |
4 | 2, 3 | anbi12i 733 |
. . . . . 6
⊢ ((¬
(𝐴‘𝑥) ≠ (0g‘𝑀) ∧ ¬ (𝐵‘𝑥) ≠ (0g‘𝑀)) ↔ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) |
5 | 1, 4 | bitri 264 |
. . . . 5
⊢ (¬
((𝐴‘𝑥) ≠
(0g‘𝑀)
∨ (𝐵‘𝑥) ≠
(0g‘𝑀))
↔ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) |
6 | | elmapfn 7880 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴 Fn 𝑉) |
7 | 6 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐴 Fn 𝑉) |
8 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝐴 Fn 𝑉) |
9 | | elmapfn 7880 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵 Fn 𝑉) |
10 | 9 | ad2antll 765 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐵 Fn 𝑉) |
11 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝐵 Fn 𝑉) |
12 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑉 ∈ 𝑋) |
13 | 12 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝑉 ∈ 𝑋) |
14 | | inidm 3822 |
. . . . . . . . . 10
⊢ (𝑉 ∩ 𝑉) = 𝑉 |
15 | | simplrl 800 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) = (0g‘𝑀)) |
16 | | simplrr 801 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) = (0g‘𝑀)) |
17 | 8, 11, 13, 13, 14, 15, 16 | ofval 6906 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) = ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀))) |
18 | 17 | an32s 846 |
. . . . . . . 8
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) = ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀))) |
19 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Base‘𝑀) =
(Base‘𝑀) |
20 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(0g‘𝑀) = (0g‘𝑀) |
21 | 19, 20 | mndidcl 17308 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ (Base‘𝑀)) |
22 | 21 | ancli 574 |
. . . . . . . . . 10
⊢ (𝑀 ∈ Mnd → (𝑀 ∈ Mnd ∧
(0g‘𝑀)
∈ (Base‘𝑀))) |
23 | 22 | ad4antr 768 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → (𝑀 ∈ Mnd ∧ (0g‘𝑀) ∈ (Base‘𝑀))) |
24 | | eqid 2622 |
. . . . . . . . . 10
⊢
(+g‘𝑀) = (+g‘𝑀) |
25 | 19, 24, 20 | mndlid 17311 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧
(0g‘𝑀)
∈ (Base‘𝑀))
→ ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀)) = (0g‘𝑀)) |
26 | 23, 25 | syl 17 |
. . . . . . . 8
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀)) = (0g‘𝑀)) |
27 | 18, 26 | eqtrd 2656 |
. . . . . . 7
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) = (0g‘𝑀)) |
28 | | nne 2798 |
. . . . . . 7
⊢ (¬
((𝐴
∘𝑓 (+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀) ↔ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) = (0g‘𝑀)) |
29 | 27, 28 | sylibr 224 |
. . . . . 6
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ¬ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)) |
30 | 29 | ex 450 |
. . . . 5
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀)) → ¬ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀))) |
31 | 5, 30 | syl5bi 232 |
. . . 4
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (¬ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀)) → ¬ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀))) |
32 | 31 | con4d 114 |
. . 3
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀) → ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀)))) |
33 | 32 | ss2rabdv 3683 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))}) |
34 | 7, 10, 12, 12, 14 | offn 6908 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓
(+g‘𝑀)𝐵) Fn 𝑉) |
35 | | fnfun 5988 |
. . . . 5
⊢ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) Fn 𝑉 → Fun (𝐴 ∘𝑓
(+g‘𝑀)𝐵)) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → Fun (𝐴 ∘𝑓
(+g‘𝑀)𝐵)) |
37 | | ovex 6678 |
. . . . 5
⊢ (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∈ V |
38 | 37 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∈ V) |
39 | | fvexd 6203 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) →
(0g‘𝑀)
∈ V) |
40 | | suppval1 7301 |
. . . 4
⊢ ((Fun
(𝐴
∘𝑓 (+g‘𝑀)𝐵) ∧ (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∈ V ∧ (0g‘𝑀) ∈ V) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
41 | 36, 38, 39, 40 | syl3anc 1326 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
42 | 12, 7, 10 | offvalfv 42121 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓
(+g‘𝑀)𝐵) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)))) |
43 | 42 | dmeqd 5326 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) = dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)))) |
44 | | ovex 6678 |
. . . . . 6
⊢ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)) ∈ V |
45 | | eqid 2622 |
. . . . . 6
⊢ (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) |
46 | 44, 45 | dmmpti 6023 |
. . . . 5
⊢ dom
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) = 𝑉 |
47 | 43, 46 | syl6eq 2672 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) = 𝑉) |
48 | | rabeq 3192 |
. . . 4
⊢ (dom
(𝐴
∘𝑓 (+g‘𝑀)𝐵) = 𝑉 → {𝑥 ∈ dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
49 | 47, 48 | syl 17 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → {𝑥 ∈ dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
50 | 41, 49 | eqtrd 2656 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
51 | | elmapfun 7881 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → Fun 𝐴) |
52 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) |
53 | | fvexd 6203 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) →
(0g‘𝑀)
∈ V) |
54 | | suppval1 7301 |
. . . . . . 7
⊢ ((Fun
𝐴 ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧
(0g‘𝑀)
∈ V) → (𝐴 supp
(0g‘𝑀)) =
{𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
55 | 51, 52, 53, 54 | syl3anc 1326 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
56 | | elmapi 7879 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴:𝑉⟶𝑅) |
57 | | fdm 6051 |
. . . . . . 7
⊢ (𝐴:𝑉⟶𝑅 → dom 𝐴 = 𝑉) |
58 | | rabeq 3192 |
. . . . . . 7
⊢ (dom
𝐴 = 𝑉 → {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
59 | 56, 57, 58 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
60 | 55, 59 | eqtrd 2656 |
. . . . 5
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
61 | 60 | ad2antrl 764 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
62 | | elmapfun 7881 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → Fun 𝐵) |
63 | 62 | ad2antll 765 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → Fun 𝐵) |
64 | | simprr 796 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) |
65 | | suppval1 7301 |
. . . . . 6
⊢ ((Fun
𝐵 ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉) ∧
(0g‘𝑀)
∈ V) → (𝐵 supp
(0g‘𝑀)) =
{𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
66 | 63, 64, 39, 65 | syl3anc 1326 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐵 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
67 | | elmapi 7879 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵:𝑉⟶𝑅) |
68 | | fdm 6051 |
. . . . . . . 8
⊢ (𝐵:𝑉⟶𝑅 → dom 𝐵 = 𝑉) |
69 | 67, 68 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → dom 𝐵 = 𝑉) |
70 | 69 | ad2antll 765 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → dom 𝐵 = 𝑉) |
71 | | rabeq 3192 |
. . . . . 6
⊢ (dom
𝐵 = 𝑉 → {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
72 | 70, 71 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
73 | 66, 72 | eqtrd 2656 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐵 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
74 | 61, 73 | uneq12d 3768 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))) = ({𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} ∪ {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)})) |
75 | | unrab 3898 |
. . 3
⊢ ({𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} ∪ {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) = {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))} |
76 | 74, 75 | syl6eq 2672 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))) = {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))}) |
77 | 33, 50, 76 | 3sstr4d 3648 |
1
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀)))) |