Metamath Proof Explorer


Theorem cpmatelimp2

Description: Another implication of a set being a constant polynomial matrix. (Contributed by AV, 17-Nov-2019)

Ref Expression
Hypotheses cpmat.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpmat.p 𝑃 = ( Poly1𝑅 )
cpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
cpmat.b 𝐵 = ( Base ‘ 𝐶 )
cpmatel2.k 𝐾 = ( Base ‘ 𝑅 )
cpmatel2.a 𝐴 = ( algSc ‘ 𝑃 )
Assertion cpmatelimp2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀𝑆 → ( 𝑀𝐵 ∧ ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 cpmat.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 cpmat.p 𝑃 = ( Poly1𝑅 )
3 cpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
4 cpmat.b 𝐵 = ( Base ‘ 𝐶 )
5 cpmatel2.k 𝐾 = ( Base ‘ 𝑅 )
6 cpmatel2.a 𝐴 = ( algSc ‘ 𝑃 )
7 1 2 3 4 cpmatpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝑆 ) → 𝑀𝐵 )
8 7 3expa ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀𝑆 ) → 𝑀𝐵 )
9 1 2 3 4 5 6 cpmatel2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) → ( 𝑀𝑆 ↔ ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )
10 9 3expa ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀𝐵 ) → ( 𝑀𝑆 ↔ ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )
11 10 biimpd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀𝐵 ) → ( 𝑀𝑆 → ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )
12 11 impancom ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀𝑆 ) → ( 𝑀𝐵 → ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )
13 8 12 jcai ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀𝑆 ) → ( 𝑀𝐵 ∧ ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) )
14 13 ex ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀𝑆 → ( 𝑀𝐵 ∧ ∀ 𝑖𝑁𝑗𝑁𝑘𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴𝑘 ) ) ) )