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 ) → ( 𝑀 ∈ 𝑆 → ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑘 ∈ 𝐾 ( 𝑖 𝑀 𝑗 ) = ( 𝐴 ‘ 𝑘 ) ) ) )