![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovtpos | Structured version Visualization version GIF version |
Description: The transposition swaps the arguments in a two-argument function. When 𝐹 is a matrix, which is to say a function from (1...𝑚) × (1...𝑛) to ℝ or some ring, tpos 𝐹 is the transposition of 𝐹, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.) |
Ref | Expression |
---|---|
ovtpos | ⊢ (𝐴tpos 𝐹𝐵) = (𝐵𝐹𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3418 | . . . . 5 ⊢ 𝑦 ∈ V | |
2 | brtpos 7627 | . . . . 5 ⊢ (𝑦 ∈ V → (〈𝐴, 𝐵〉tpos 𝐹𝑦 ↔ 〈𝐵, 𝐴〉𝐹𝑦)) | |
3 | 1, 2 | ax-mp 5 | . . . 4 ⊢ (〈𝐴, 𝐵〉tpos 𝐹𝑦 ↔ 〈𝐵, 𝐴〉𝐹𝑦) |
4 | 3 | iotabii 6109 | . . 3 ⊢ (℩𝑦〈𝐴, 𝐵〉tpos 𝐹𝑦) = (℩𝑦〈𝐵, 𝐴〉𝐹𝑦) |
5 | df-fv 6132 | . . 3 ⊢ (tpos 𝐹‘〈𝐴, 𝐵〉) = (℩𝑦〈𝐴, 𝐵〉tpos 𝐹𝑦) | |
6 | df-fv 6132 | . . 3 ⊢ (𝐹‘〈𝐵, 𝐴〉) = (℩𝑦〈𝐵, 𝐴〉𝐹𝑦) | |
7 | 4, 5, 6 | 3eqtr4i 2860 | . 2 ⊢ (tpos 𝐹‘〈𝐴, 𝐵〉) = (𝐹‘〈𝐵, 𝐴〉) |
8 | df-ov 6909 | . 2 ⊢ (𝐴tpos 𝐹𝐵) = (tpos 𝐹‘〈𝐴, 𝐵〉) | |
9 | df-ov 6909 | . 2 ⊢ (𝐵𝐹𝐴) = (𝐹‘〈𝐵, 𝐴〉) | |
10 | 7, 8, 9 | 3eqtr4i 2860 | 1 ⊢ (𝐴tpos 𝐹𝐵) = (𝐵𝐹𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1658 ∈ wcel 2166 Vcvv 3415 〈cop 4404 class class class wbr 4874 ℩cio 6085 ‘cfv 6124 (class class class)co 6906 tpos ctpos 7617 |
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-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 |
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-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-sbc 3664 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-mpt 4954 df-id 5251 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-iota 6087 df-fun 6126 df-fn 6127 df-fv 6132 df-ov 6909 df-tpos 7618 |
This theorem is referenced by: tpossym 7650 oppchom 16728 oppcco 16730 oppcmon 16751 funcoppc 16888 fulloppc 16935 fthoppc 16936 fthepi 16941 yonedalem22 17272 oppgplus 18130 oppglsm 18409 opprmul 18981 mamutpos 20633 mdettpos 20786 madutpos 20817 mdetpmtr2 30436 |
Copyright terms: Public domain | W3C validator |