ovtpos

Description: The transposition swaps the arguments in a two-argument function. When F is a matrix, which is to say a function from ( 1 ... m ) X. ( 1 ... n ) to RR or some ring, tpos F is the transposition of F , which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	ovtpos	$⊢ A tpos F B = B F A$

Proof

Step	Hyp	Ref	Expression
1		brtpos	$⊢ y \in V \to (⟨A, B⟩ tpos F y \leftrightarrow ⟨B, A⟩ F y)$
2	1	elv	$⊢ ⟨A, B⟩ tpos F y \leftrightarrow ⟨B, A⟩ F y$
3	2	iotabii	$⊢ (ι y \| ⟨A, B⟩ tpos F y) = (ι y \| ⟨B, A⟩ F y)$
4		df-fv	$⊢ tpos F (⟨A, B⟩) = (ι y \| ⟨A, B⟩ tpos F y)$
5		df-fv	$⊢ F (⟨B, A⟩) = (ι y \| ⟨B, A⟩ F y)$
6	3 4 5	3eqtr4i	$⊢ tpos F (⟨A, B⟩) = F (⟨B, A⟩)$
7		df-ov	$⊢ A tpos F B = tpos F (⟨A, B⟩)$
8		df-ov	$⊢ B F A = F (⟨B, A⟩)$
9	6 7 8	3eqtr4i	$⊢ A tpos F B = B F A$

Metamath Proof Explorer

Theorem ovtpos

Proof