Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvhvaddcbv | Structured version Visualization version GIF version |
Description: Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.) |
Ref | Expression |
---|---|
dvhvaddval.a | ⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^{st} ‘𝑓) ∘ (1^{st} ‘𝑔)), ((2^{nd} ‘𝑓) ⨣ (2^{nd} ‘𝑔))⟩) |
Ref | Expression |
---|---|
dvhvaddcbv | ⊢ + = (ℎ ∈ (𝑇 × 𝐸), 𝑖 ∈ (𝑇 × 𝐸) ↦ ⟨((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑖)), ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑖))⟩) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvhvaddval.a | . 2 ⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^{st} ‘𝑓) ∘ (1^{st} ‘𝑔)), ((2^{nd} ‘𝑓) ⨣ (2^{nd} ‘𝑔))⟩) | |
2 | fveq2 6433 | . . . . 5 ⊢ (𝑓 = ℎ → (1^{st} ‘𝑓) = (1^{st} ‘ℎ)) | |
3 | 2 | coeq1d 5516 | . . . 4 ⊢ (𝑓 = ℎ → ((1^{st} ‘𝑓) ∘ (1^{st} ‘𝑔)) = ((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑔))) |
4 | fveq2 6433 | . . . . 5 ⊢ (𝑓 = ℎ → (2^{nd} ‘𝑓) = (2^{nd} ‘ℎ)) | |
5 | 4 | oveq1d 6920 | . . . 4 ⊢ (𝑓 = ℎ → ((2^{nd} ‘𝑓) ⨣ (2^{nd} ‘𝑔)) = ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑔))) |
6 | 3, 5 | opeq12d 4631 | . . 3 ⊢ (𝑓 = ℎ → ⟨((1^{st} ‘𝑓) ∘ (1^{st} ‘𝑔)), ((2^{nd} ‘𝑓) ⨣ (2^{nd} ‘𝑔))⟩ = ⟨((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑔)), ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑔))⟩) |
7 | fveq2 6433 | . . . . 5 ⊢ (𝑔 = 𝑖 → (1^{st} ‘𝑔) = (1^{st} ‘𝑖)) | |
8 | 7 | coeq2d 5517 | . . . 4 ⊢ (𝑔 = 𝑖 → ((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑔)) = ((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑖))) |
9 | fveq2 6433 | . . . . 5 ⊢ (𝑔 = 𝑖 → (2^{nd} ‘𝑔) = (2^{nd} ‘𝑖)) | |
10 | 9 | oveq2d 6921 | . . . 4 ⊢ (𝑔 = 𝑖 → ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑔)) = ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑖))) |
11 | 8, 10 | opeq12d 4631 | . . 3 ⊢ (𝑔 = 𝑖 → ⟨((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑔)), ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑔))⟩ = ⟨((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑖)), ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑖))⟩) |
12 | 6, 11 | cbvmpt2v 6995 | . 2 ⊢ (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ ⟨((1^{st} ‘𝑓) ∘ (1^{st} ‘𝑔)), ((2^{nd} ‘𝑓) ⨣ (2^{nd} ‘𝑔))⟩) = (ℎ ∈ (𝑇 × 𝐸), 𝑖 ∈ (𝑇 × 𝐸) ↦ ⟨((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑖)), ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑖))⟩) |
13 | 1, 12 | eqtri 2849 | 1 ⊢ + = (ℎ ∈ (𝑇 × 𝐸), 𝑖 ∈ (𝑇 × 𝐸) ↦ ⟨((1^{st} ‘ℎ) ∘ (1^{st} ‘𝑖)), ((2^{nd} ‘ℎ) ⨣ (2^{nd} ‘𝑖))⟩) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ⟨cop 4403 × cxp 5340 ∘ ccom 5346 ‘cfv 6123 (class class class)co 6905 ↦ cmpt2 6907 1^{st} c1st 7426 2^{nd} c2nd 7427 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-co 5351 df-iota 6086 df-fv 6131 df-ov 6908 df-oprab 6909 df-mpt2 6910 |
This theorem is referenced by: dvhvaddval 37165 |
Copyright terms: Public domain | W3C validator |