Metamath Proof Explorer

Theorem mamutpos

Description: Behavior of transposes in matrix products, see also the statement in Lang p. 505. (Contributed by Stefan O'Rear, 9-Jul-2018)

Ref Expression
Hypotheses mamutpos.f ⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
mamutpos.g ⊢ 𝐺 = ( 𝑅 maMul ⟨ 𝑃 , 𝑁 , 𝑀 ⟩ )
mamutpos.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mamutpos.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mamutpos.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
mamutpos.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mamutpos.p ⊢ ( 𝜑 → 𝑃 ∈ Fin )
mamutpos.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
mamutpos.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) )
Assertion mamutpos ( 𝜑 → tpos ( 𝑋 𝐹 𝑌 ) = ( tpos 𝑌 𝐺 tpos 𝑋 ) )

Proof

Step Hyp Ref Expression
1 mamutpos.f ⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
2 mamutpos.g ⊢ 𝐺 = ( 𝑅 maMul ⟨ 𝑃 , 𝑁 , 𝑀 ⟩ )
3 mamutpos.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 mamutpos.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
5 mamutpos.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
6 mamutpos.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
7 mamutpos.p ⊢ ( 𝜑 → 𝑃 ∈ Fin )
8 mamutpos.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
9 mamutpos.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) )
10 eqid ⊢ ( 𝑗 ∈ 𝑀 , 𝑖 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) ) = ( 𝑗 ∈ 𝑀 , 𝑖 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) )
11 10 tposmpo ⊢ tpos ( 𝑗 ∈ 𝑀 , 𝑖 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) ) = ( 𝑖 ∈ 𝑃 , 𝑗 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) )
12 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → 𝜑 )
13 12 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ CRing )
14 elmapi ⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
15 12 8 14 3syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
16 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑗 ∈ 𝑀 )
17 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
18 15 16 17 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑗 𝑋 𝑘 ) ∈ 𝐵 )
19 elmapi ⊢ ( 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) → 𝑌 : ( 𝑁 × 𝑃 ) ⟶ 𝐵 )
20 12 9 19 3syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑌 : ( 𝑁 × 𝑃 ) ⟶ 𝐵 )
21 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → 𝑖 ∈ 𝑃 )
22 20 17 21 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝑌 𝑖 ) ∈ 𝐵 )
23 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
24 3 23 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑗 𝑋 𝑘 ) ∈ 𝐵 ∧ ( 𝑘 𝑌 𝑖 ) ∈ 𝐵 ) → ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) = ( ( 𝑘 𝑌 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑋 𝑘 ) ) )
25 13 18 22 24 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) = ( ( 𝑘 𝑌 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑋 𝑘 ) ) )
26 ovtpos ⊢ ( 𝑖 tpos 𝑌 𝑘 ) = ( 𝑘 𝑌 𝑖 )
27 ovtpos ⊢ ( 𝑘 tpos 𝑋 𝑗 ) = ( 𝑗 𝑋 𝑘 )
28 26 27 oveq12i ⊢ ( ( 𝑖 tpos 𝑌 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 tpos 𝑋 𝑗 ) ) = ( ( 𝑘 𝑌 𝑖 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑋 𝑘 ) )
29 25 28 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) = ( ( 𝑖 tpos 𝑌 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 tpos 𝑋 𝑗 ) ) )
30 29 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 tpos 𝑌 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 tpos 𝑋 𝑗 ) ) ) )
31 30 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ∧ 𝑗 ∈ 𝑀 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 tpos 𝑌 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 tpos 𝑋 𝑗 ) ) ) ) )
32 31 mpoeq3dva ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑃 , 𝑗 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) ) = ( 𝑖 ∈ 𝑃 , 𝑗 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 tpos 𝑌 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 tpos 𝑋 𝑗 ) ) ) ) ) )
33 11 32 eqtrid ⊢ ( 𝜑 → tpos ( 𝑗 ∈ 𝑀 , 𝑖 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) ) = ( 𝑖 ∈ 𝑃 , 𝑗 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 tpos 𝑌 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 tpos 𝑋 𝑗 ) ) ) ) ) )
34 1 3 23 4 5 6 7 8 9 mamuval ⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( 𝑗 ∈ 𝑀 , 𝑖 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) ) )
35 34 tposeqd ⊢ ( 𝜑 → tpos ( 𝑋 𝐹 𝑌 ) = tpos ( 𝑗 ∈ 𝑀 , 𝑖 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑗 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑖 ) ) ) ) ) )
36 tposmap ⊢ ( 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) → tpos 𝑌 ∈ ( 𝐵 ↑m ( 𝑃 × 𝑁 ) ) )
37 9 36 syl ⊢ ( 𝜑 → tpos 𝑌 ∈ ( 𝐵 ↑m ( 𝑃 × 𝑁 ) ) )
38 tposmap ⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) → tpos 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) )
39 8 38 syl ⊢ ( 𝜑 → tpos 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑀 ) ) )
40 2 3 23 4 7 6 5 37 39 mamuval ⊢ ( 𝜑 → ( tpos 𝑌 𝐺 tpos 𝑋 ) = ( 𝑖 ∈ 𝑃 , 𝑗 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 tpos 𝑌 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 tpos 𝑋 𝑗 ) ) ) ) ) )
41 33 35 40 3eqtr4d ⊢ ( 𝜑 → tpos ( 𝑋 𝐹 𝑌 ) = ( tpos 𝑌 𝐺 tpos 𝑋 ) )