Metamath Proof Explorer

Theorem d1mat2pmat

Description: The transformation of a matrix of dimenson 1. (Contributed by AV, 4-Aug-2019)

Ref Expression
Hypotheses d1mat2pmat.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
d1mat2pmat.b ⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
d1mat2pmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
d1mat2pmat.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
Assertion d1mat2pmat ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } )

Proof

Step Hyp Ref Expression
1 d1mat2pmat.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2 d1mat2pmat.b ⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
3 d1mat2pmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4 d1mat2pmat.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
5 snfi ⊢ { 𝐴 } ∈ Fin
6 eleq1 ⊢ ( 𝑁 = { 𝐴 } → ( 𝑁 ∈ Fin ↔ { 𝐴 } ∈ Fin ) )
7 5 6 mpbiri ⊢ ( 𝑁 = { 𝐴 } → 𝑁 ∈ Fin )
8 7 adantr ⊢ ( ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) → 𝑁 ∈ Fin )
9 8 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
10 simp1 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ 𝑉 )
11 simp3 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
12 eqid ⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
13 1 12 2 3 4 mat2pmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) )
14 9 10 11 13 syl3anc ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) )
15 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
16 fvexd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ∈ V )
17 15 15 16 3jca ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ∈ V ) )
18 17 adantl ⊢ ( ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ∈ V ) )
19 18 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ∈ V ) )
20 eqid ⊢ ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) )
21 fvoveq1 ⊢ ( 𝑖 = 𝐴 → ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( 𝑆 ‘ ( 𝐴 𝑀 𝑗 ) ) )
22 oveq2 ⊢ ( 𝑗 = 𝐴 → ( 𝐴 𝑀 𝑗 ) = ( 𝐴 𝑀 𝐴 ) )
23 22 fveq2d ⊢ ( 𝑗 = 𝐴 → ( 𝑆 ‘ ( 𝐴 𝑀 𝑗 ) ) = ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) )
24 20 21 23 mposn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ∈ V ) → ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } )
25 19 24 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } )
26 mpoeq12 ⊢ ( ( 𝑁 = { 𝐴 } ∧ 𝑁 = { 𝐴 } ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) )
27 26 eqeq1d ⊢ ( ( 𝑁 = { 𝐴 } ∧ 𝑁 = { 𝐴 } ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } ↔ ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } ) )
28 27 anidms ⊢ ( 𝑁 = { 𝐴 } → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } ↔ ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } ) )
29 28 adantr ⊢ ( ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } ↔ ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } ) )
30 29 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } ↔ ( 𝑖 ∈ { 𝐴 } , 𝑗 ∈ { 𝐴 } ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } ) )
31 25 30 mpbird ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑆 ‘ ( 𝑖 𝑀 𝑗 ) ) ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } )
32 14 31 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 = { 𝐴 } ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑀 ) = { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , ( 𝑆 ‘ ( 𝐴 𝑀 𝐴 ) ) ⟩ } )