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 𝑋 ) )

Metamath Proof Explorer

Theorem mattposm

Proof