Metamath Proof Explorer

Theorem mattposm

Description: Multiplying two transposed matrices results in the transposition of the product of the two matrices. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses mattposm.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mattposm.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mattposm.t ⊢ · = ( .r ‘ 𝐴 )
Assertion mattposm ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → tpos ( 𝑋 · 𝑌 ) = ( tpos 𝑌 · tpos 𝑋 ) )

Proof

Step Hyp Ref Expression
1 mattposm.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mattposm.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 mattposm.t ⊢ · = ( .r ‘ 𝐴 )
4 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 simp1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ CRing )
7 1 2 matrcl ⊢ ( 𝑌 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
8 7 simpld ⊢ ( 𝑌 ∈ 𝐵 → 𝑁 ∈ Fin )
9 8 3ad2ant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑁 ∈ Fin )
10 1 5 2 matbas2i ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
11 10 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
12 1 5 2 matbas2i ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
13 12 3ad2ant3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
14 4 4 5 6 9 9 9 11 13 mamutpos ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → tpos ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) = ( tpos 𝑌 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) tpos 𝑋 ) )
15 1 4 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
16 9 6 15 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
17 3 16 eqtr4id ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → · = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
18 17 oveqd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) )
19 18 tposeqd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → tpos ( 𝑋 · 𝑌 ) = tpos ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) )
20 17 oveqd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( tpos 𝑌 · tpos 𝑋 ) = ( tpos 𝑌 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) tpos 𝑋 ) )
21 14 19 20 3eqtr4d ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → tpos ( 𝑋 · 𝑌 ) = ( tpos 𝑌 · tpos 𝑋 ) )