Step | Hyp | Ref
| Expression |
1 | | ioran 510 |
. . . . . 6
⊢ (¬
((𝐴‘𝑥) ≠
(0g‘𝑀)
∨ (𝐵‘𝑥) ≠
(0g‘𝑀))
↔ (¬ (𝐴‘𝑥) ≠ (0g‘𝑀) ∧ ¬ (𝐵‘𝑥) ≠ (0g‘𝑀))) |
2 | | nne 2786 |
. . . . . . 7
⊢ (¬
(𝐴‘𝑥) ≠ (0g‘𝑀) ↔ (𝐴‘𝑥) = (0g‘𝑀)) |
3 | | nne 2786 |
. . . . . . 7
⊢ (¬
(𝐵‘𝑥) ≠ (0g‘𝑀) ↔ (𝐵‘𝑥) = (0g‘𝑀)) |
4 | 2, 3 | anbi12i 729 |
. . . . . 6
⊢ ((¬
(𝐴‘𝑥) ≠ (0g‘𝑀) ∧ ¬ (𝐵‘𝑥) ≠ (0g‘𝑀)) ↔ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) |
5 | 1, 4 | bitri 263 |
. . . . 5
⊢ (¬
((𝐴‘𝑥) ≠
(0g‘𝑀)
∨ (𝐵‘𝑥) ≠
(0g‘𝑀))
↔ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) |
6 | | elmapfn 7766 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴 Fn 𝑉) |
7 | 6 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐴 Fn 𝑉) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝐴 Fn 𝑉) |
9 | | elmapfn 7766 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵 Fn 𝑉) |
10 | 9 | ad2antll 761 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐵 Fn 𝑉) |
11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝐵 Fn 𝑉) |
12 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝑉 ∈ 𝑋) |
13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → 𝑉 ∈ 𝑋) |
14 | | inidm 3784 |
. . . . . . . . . 10
⊢ (𝑉 ∩ 𝑉) = 𝑉 |
15 | | simplrl 796 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (𝐴‘𝑥) = (0g‘𝑀)) |
16 | | simplrr 797 |
. . . . . . . . . 10
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → (𝐵‘𝑥) = (0g‘𝑀)) |
17 | 8, 11, 13, 13, 14, 15, 16 | ofval 6804 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) ∧ 𝑥 ∈ 𝑉) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) = ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀))) |
18 | 17 | an32s 842 |
. . . . . . . 8
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) = ((0g‘𝑀)(+g‘𝑀)(0g‘𝑀))) |
19 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑀) =
(Base‘𝑀) |
20 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘𝑀) = (0g‘𝑀) |
21 | 19, 20 | mndidcl 17131 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ Mnd →
(0g‘𝑀)
∈ (Base‘𝑀)) |
22 | 21 | ancli 572 |
. . . . . . . . . 10
⊢ (𝑀 ∈ Mnd → (𝑀 ∈ Mnd ∧
(0g‘𝑀)
∈ (Base‘𝑀))) |
23 | 22 | ad4antr 764 |
. . . . . . . . 9
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → (𝑀 ∈ Mnd ∧ (0g‘𝑀) ∈ (Base‘𝑀))) |
24 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝑀) = (+g‘𝑀) |
25 | 19, 24, 20 | mndlid 17134 |
. . . . . . . . 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 2644 |
. . . . . . 7
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) = (0g‘𝑀)) |
28 | | nne 2786 |
. . . . . . 7
⊢ (¬
((𝐴
∘𝑓 (+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀) ↔ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) = (0g‘𝑀)) |
29 | 27, 28 | sylibr 223 |
. . . . . 6
⊢
(((((𝑀 ∈ Mnd
∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) ∧ ((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀))) → ¬ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)) |
30 | 29 | ex 449 |
. . . . 5
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴‘𝑥) = (0g‘𝑀) ∧ (𝐵‘𝑥) = (0g‘𝑀)) → ¬ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀))) |
31 | 5, 30 | syl5bi 231 |
. . . 4
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (¬ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀)) → ¬ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀))) |
32 | 31 | con4d 113 |
. . 3
⊢ ((((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑥 ∈ 𝑉) → (((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀) → ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀)))) |
33 | 32 | ss2rabdv 3646 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} ⊆ {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))}) |
34 | 7, 10, 12, 12, 14 | offn 6806 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓
(+g‘𝑀)𝐵) Fn 𝑉) |
35 | | fnfun 5902 |
. . . . 5
⊢ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) Fn 𝑉 → Fun (𝐴 ∘𝑓
(+g‘𝑀)𝐵)) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → Fun (𝐴 ∘𝑓
(+g‘𝑀)𝐵)) |
37 | | ovex 6577 |
. . . . 5
⊢ (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∈ V |
38 | 37 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∈ V) |
39 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝑀) ∈ V |
40 | 39 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) →
(0g‘𝑀)
∈ V) |
41 | | suppval1 7188 |
. . . 4
⊢ ((Fun
(𝐴
∘𝑓 (+g‘𝑀)𝐵) ∧ (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∈ V ∧ (0g‘𝑀) ∈ V) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
42 | 36, 38, 40, 41 | syl3anc 1318 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
43 | 12, 7, 10 | offvalfv 41914 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 ∘𝑓
(+g‘𝑀)𝐵) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)))) |
44 | 43 | dmeqd 5248 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) = dom (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)))) |
45 | | ovex 6577 |
. . . . . 6
⊢ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣)) ∈ V |
46 | | eqid 2610 |
. . . . . 6
⊢ (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) = (𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) |
47 | 45, 46 | dmmpti 5936 |
. . . . 5
⊢ dom
(𝑣 ∈ 𝑉 ↦ ((𝐴‘𝑣)(+g‘𝑀)(𝐵‘𝑣))) = 𝑉 |
48 | 44, 47 | syl6eq 2660 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) = 𝑉) |
49 | | rabeq 3166 |
. . . 4
⊢ (dom
(𝐴
∘𝑓 (+g‘𝑀)𝐵) = 𝑉 → {𝑥 ∈ dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
50 | 48, 49 | syl 17 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → {𝑥 ∈ dom (𝐴 ∘𝑓
(+g‘𝑀)𝐵) ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
51 | 42, 50 | eqtrd 2644 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ ((𝐴 ∘𝑓
(+g‘𝑀)𝐵)‘𝑥) ≠ (0g‘𝑀)}) |
52 | | elmapfun 7767 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → Fun 𝐴) |
53 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴 ∈ (𝑅 ↑𝑚 𝑉)) |
54 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) →
(0g‘𝑀)
∈ V) |
55 | | suppval1 7188 |
. . . . . . 7
⊢ ((Fun
𝐴 ∧ 𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧
(0g‘𝑀)
∈ V) → (𝐴 supp
(0g‘𝑀)) =
{𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
56 | 52, 53, 54, 55 | syl3anc 1318 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
57 | | elmapi 7765 |
. . . . . . 7
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → 𝐴:𝑉⟶𝑅) |
58 | | fdm 5964 |
. . . . . . 7
⊢ (𝐴:𝑉⟶𝑅 → dom 𝐴 = 𝑉) |
59 | | rabeq 3166 |
. . . . . . 7
⊢ (dom
𝐴 = 𝑉 → {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
60 | 57, 58, 59 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → {𝑥 ∈ dom 𝐴 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
61 | 56, 60 | eqtrd 2644 |
. . . . 5
⊢ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
62 | 61 | ad2antrl 760 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐴 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)}) |
63 | | elmapfun 7767 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → Fun 𝐵) |
64 | 63 | ad2antll 761 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → Fun 𝐵) |
65 | | simprr 792 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → 𝐵 ∈ (𝑅 ↑𝑚 𝑉)) |
66 | | suppval1 7188 |
. . . . . 6
⊢ ((Fun
𝐵 ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉) ∧
(0g‘𝑀)
∈ V) → (𝐵 supp
(0g‘𝑀)) =
{𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
67 | 64, 65, 40, 66 | syl3anc 1318 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐵 supp (0g‘𝑀)) = {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
68 | | elmapi 7765 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → 𝐵:𝑉⟶𝑅) |
69 | | fdm 5964 |
. . . . . . . 8
⊢ (𝐵:𝑉⟶𝑅 → dom 𝐵 = 𝑉) |
70 | 68, 69 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ (𝑅 ↑𝑚 𝑉) → dom 𝐵 = 𝑉) |
71 | 70 | ad2antll 761 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → dom 𝐵 = 𝑉) |
72 | | rabeq 3166 |
. . . . . 6
⊢ (dom
𝐵 = 𝑉 → {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
73 | 71, 72 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → {𝑥 ∈ dom 𝐵 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)} = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
74 | 67, 73 | eqtrd 2644 |
. . . 4
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → (𝐵 supp (0g‘𝑀)) = {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) |
75 | 62, 74 | uneq12d 3730 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))) = ({𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} ∪ {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)})) |
76 | | unrab 3857 |
. . 3
⊢ ({𝑥 ∈ 𝑉 ∣ (𝐴‘𝑥) ≠ (0g‘𝑀)} ∪ {𝑥 ∈ 𝑉 ∣ (𝐵‘𝑥) ≠ (0g‘𝑀)}) = {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))} |
77 | 75, 76 | syl6eq 2660 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))) = {𝑥 ∈ 𝑉 ∣ ((𝐴‘𝑥) ≠ (0g‘𝑀) ∨ (𝐵‘𝑥) ≠ (0g‘𝑀))}) |
78 | 33, 51, 77 | 3sstr4d 3611 |
1
⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝐵 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝐴 ∘𝑓
(+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀)))) |