Theorem mattposcl

Description: The transpose of a square matrix is a square matrix of the same size. (Contributed by SO, 9-Jul-2018)

	Ref	Expression
Hypotheses	mattposcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mattposcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	mattposcl	⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mattposcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mattposcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	1 3 2	matbas2i	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
5		elmapi	⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
6		tposf	⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) → tpos 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
7	4 5 6	3syl	⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
8		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
9	1 2	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
10	9	simpld	⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
11		xpfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
12	11	anidms	⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ Fin )
13	10 12	syl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 × 𝑁 ) ∈ Fin )
14		elmapg	⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ ( 𝑁 × 𝑁 ) ∈ Fin ) → ( tpos 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ↔ tpos 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) ) )
15	8 13 14	sylancr	⊢ ( 𝑀 ∈ 𝐵 → ( tpos 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ↔ tpos 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) ) )
16	7 15	mpbird	⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
17	1 3	matbas2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
18	9 17	syl	⊢ ( 𝑀 ∈ 𝐵 → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
19	18 2	eqtr4di	⊢ ( 𝑀 ∈ 𝐵 → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
20	16 19	eleqtrd	⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ 𝐵 )