Theorem 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	$$⊢AtposFB=BFA$$

Proof

Step	Hyp	Ref	Expression
1		brtpos	$$⊢y\in \mathrm{V}\to \left(⟨A,B⟩tposFy\leftrightarrow ⟨B,A⟩Fy\right)$$
2	1	elv	$$⊢⟨A,B⟩tposFy\leftrightarrow ⟨B,A⟩Fy$$
3	2	iotabii	$$⊢\left(\iota y|⟨A,B⟩tposFy\right)=\left(\iota y|⟨B,A⟩Fy\right)$$
4		df-fv	$$⊢tposF\left(⟨A,B⟩\right)=\left(\iota y|⟨A,B⟩tposFy\right)$$
5		df-fv	$$⊢F\left(⟨B,A⟩\right)=\left(\iota y|⟨B,A⟩Fy\right)$$
6	3 4 5	3eqtr4i	$$⊢tposF\left(⟨A,B⟩\right)=F\left(⟨B,A⟩\right)$$
7		df-ov	$$⊢AtposFB=tposF\left(⟨A,B⟩\right)$$
8		df-ov	$$⊢BFA=F\left(⟨B,A⟩\right)$$
9	6 7 8	3eqtr4i	$$⊢AtposFB=BFA$$