Proof of Theorem suppco
Step | Hyp | Ref
| Expression |
1 | | coexg 7707 |
. . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘ 𝐺) ∈ V) |
2 | | simpl 486 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → 𝑍 ∈ V) |
3 | | suppimacnv 7916 |
. . . . 5
⊢ (((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍}))) |
4 | 1, 2, 3 | syl2an2 686 |
. . . 4
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍}))) |
5 | | cnvco 5754 |
. . . . . 6
⊢ ◡(𝐹 ∘ 𝐺) = (◡𝐺 ∘ ◡𝐹) |
6 | 5 | imaeq1i 5926 |
. . . . 5
⊢ (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍})) |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍}))) |
8 | | imaco 6115 |
. . . . 5
⊢ ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍})) = (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍}))) |
9 | | simprl 771 |
. . . . . . 7
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → 𝐹 ∈ 𝑉) |
10 | | suppimacnv 7916 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
11 | 9, 2, 10 | syl2anc 587 |
. . . . . 6
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) |
12 | 11 | imaeq2d 5929 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (◡𝐺 “ (𝐹 supp 𝑍)) = (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍})))) |
13 | 8, 12 | eqtr4id 2797 |
. . . 4
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍})) = (◡𝐺 “ (𝐹 supp 𝑍))) |
14 | 4, 7, 13 | 3eqtrd 2781 |
. . 3
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍))) |
15 | 14 | ex 416 |
. 2
⊢ (𝑍 ∈ V → ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍)))) |
16 | | prcnel 3431 |
. . . . . 6
⊢ (¬
𝑍 ∈ V → ¬
𝑍 ∈
V) |
17 | 16 | intnand 492 |
. . . . 5
⊢ (¬
𝑍 ∈ V → ¬
((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V)) |
18 | | supp0prc 7906 |
. . . . 5
⊢ (¬
((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅) |
19 | 17, 18 | syl 17 |
. . . 4
⊢ (¬
𝑍 ∈ V → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅) |
20 | 16 | intnand 492 |
. . . . . . 7
⊢ (¬
𝑍 ∈ V → ¬
(𝐹 ∈ V ∧ 𝑍 ∈ V)) |
21 | | supp0prc 7906 |
. . . . . . 7
⊢ (¬
(𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅) |
22 | 20, 21 | syl 17 |
. . . . . 6
⊢ (¬
𝑍 ∈ V → (𝐹 supp 𝑍) = ∅) |
23 | 22 | imaeq2d 5929 |
. . . . 5
⊢ (¬
𝑍 ∈ V → (◡𝐺 “ (𝐹 supp 𝑍)) = (◡𝐺 “ ∅)) |
24 | | ima0 5945 |
. . . . 5
⊢ (◡𝐺 “ ∅) = ∅ |
25 | 23, 24 | eqtrdi 2794 |
. . . 4
⊢ (¬
𝑍 ∈ V → (◡𝐺 “ (𝐹 supp 𝑍)) = ∅) |
26 | 19, 25 | eqtr4d 2780 |
. . 3
⊢ (¬
𝑍 ∈ V → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍))) |
27 | 26 | a1d 25 |
. 2
⊢ (¬
𝑍 ∈ V → ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍)))) |
28 | 15, 27 | pm2.61i 185 |
1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍))) |