Proof of Theorem suppco
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | coexg 7951 | . . . . 5
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 ∘ 𝐺) ∈ V) | 
| 2 |  | simpl 482 | . . . . 5
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → 𝑍 ∈ V) | 
| 3 |  | suppimacnv 8199 | . . . . 5
⊢ (((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍}))) | 
| 4 | 1, 2, 3 | syl2an2 686 | . . . 4
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍}))) | 
| 5 |  | cnvco 5896 | . . . . . 6
⊢ ◡(𝐹 ∘ 𝐺) = (◡𝐺 ∘ ◡𝐹) | 
| 6 | 5 | imaeq1i 6075 | . . . . 5
⊢ (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍})) | 
| 7 | 6 | a1i 11 | . . . 4
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (◡(𝐹 ∘ 𝐺) “ (V ∖ {𝑍})) = ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍}))) | 
| 8 |  | imaco 6271 | . . . . 5
⊢ ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍})) = (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍}))) | 
| 9 |  | simprl 771 | . . . . . . 7
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → 𝐹 ∈ 𝑉) | 
| 10 |  | suppimacnv 8199 | . . . . . . 7
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) | 
| 11 | 9, 2, 10 | syl2anc 584 | . . . . . 6
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (𝐹 supp 𝑍) = (◡𝐹 “ (V ∖ {𝑍}))) | 
| 12 | 11 | imaeq2d 6078 | . . . . 5
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → (◡𝐺 “ (𝐹 supp 𝑍)) = (◡𝐺 “ (◡𝐹 “ (V ∖ {𝑍})))) | 
| 13 | 8, 12 | eqtr4id 2796 | . . . 4
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((◡𝐺 ∘ ◡𝐹) “ (V ∖ {𝑍})) = (◡𝐺 “ (𝐹 supp 𝑍))) | 
| 14 | 4, 7, 13 | 3eqtrd 2781 | . . 3
⊢ ((𝑍 ∈ V ∧ (𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊)) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍))) | 
| 15 | 14 | ex 412 | . 2
⊢ (𝑍 ∈ V → ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍)))) | 
| 16 |  | prcnel 3507 | . . . . . 6
⊢ (¬
𝑍 ∈ V → ¬
𝑍 ∈
V) | 
| 17 | 16 | intnand 488 | . . . . 5
⊢ (¬
𝑍 ∈ V → ¬
((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V)) | 
| 18 |  | supp0prc 8188 | . . . . 5
⊢ (¬
((𝐹 ∘ 𝐺) ∈ V ∧ 𝑍 ∈ V) → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅) | 
| 19 | 17, 18 | syl 17 | . . . 4
⊢ (¬
𝑍 ∈ V → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅) | 
| 20 | 16 | intnand 488 | . . . . . . 7
⊢ (¬
𝑍 ∈ V → ¬
(𝐹 ∈ V ∧ 𝑍 ∈ V)) | 
| 21 |  | supp0prc 8188 | . . . . . . 7
⊢ (¬
(𝐹 ∈ V ∧ 𝑍 ∈ V) → (𝐹 supp 𝑍) = ∅) | 
| 22 | 20, 21 | syl 17 | . . . . . 6
⊢ (¬
𝑍 ∈ V → (𝐹 supp 𝑍) = ∅) | 
| 23 | 22 | imaeq2d 6078 | . . . . 5
⊢ (¬
𝑍 ∈ V → (◡𝐺 “ (𝐹 supp 𝑍)) = (◡𝐺 “ ∅)) | 
| 24 |  | ima0 6095 | . . . . 5
⊢ (◡𝐺 “ ∅) = ∅ | 
| 25 | 23, 24 | eqtrdi 2793 | . . . 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 182 | 1
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍))) |