m2cpminvid2lem

Description: Lemma for m2cpminvid2 . (Contributed by AV, 12-Nov-2019) (Revised by AV, 14-Dec-2019)

	Ref	Expression
Hypotheses	m2cpminvid2lem.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	m2cpminvid2lem.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
Assertion	m2cpminvid2lem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ∀ 𝑛 ∈ ℕ₀ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		m2cpminvid2lem.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		m2cpminvid2lem.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
3		eqid	⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
4		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
5	1 2 3 4	cpmatelimp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝑆 → ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ) ) )
6	5	3impia	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ) )
7	6	simprd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) )
8	7	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) )
9		fvoveq1	⊢ ( 𝑖 = 𝑥 → ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe₁ ‘ ( 𝑥 𝑀 𝑗 ) ) )
10	9	fveq1d	⊢ ( 𝑖 = 𝑥 → ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑗 ) ) ‘ 𝑘 ) )
11	10	eqeq1d	⊢ ( 𝑖 = 𝑥 → ( ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ↔ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ) )
12	11	ralbidv	⊢ ( 𝑖 = 𝑥 → ( ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ↔ ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ) )
13		oveq2	⊢ ( 𝑗 = 𝑦 → ( 𝑥 𝑀 𝑗 ) = ( 𝑥 𝑀 𝑦 ) )
14	13	fveq2d	⊢ ( 𝑗 = 𝑦 → ( coe₁ ‘ ( 𝑥 𝑀 𝑗 ) ) = ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) )
15	14	fveq1d	⊢ ( 𝑗 = 𝑦 → ( ( coe₁ ‘ ( 𝑥 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑘 ) )
16	15	eqeq1d	⊢ ( 𝑗 = 𝑦 → ( ( ( coe₁ ‘ ( 𝑥 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ↔ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ) )
17	16	ralbidv	⊢ ( 𝑗 = 𝑦 → ( ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ↔ ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ) )
18	12 17	rspc2v	⊢ ( ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) → ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ) )
19	18	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) → ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ) )
20		fveqeq2	⊢ ( 𝑘 = 𝑛 → ( ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ↔ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) )
21	20	cbvralvw	⊢ ( ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) ↔ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
22		simpl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
23		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
24		simprl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑥 ∈ 𝑁 )
25		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑦 ∈ 𝑁 )
26	1 2 3 4	cpmatpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
27	26	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑀 ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
28	3 23 4 24 25 27	matecld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ 𝑃 ) )
29		0nn0	⊢ 0 ∈ ℕ₀
30		eqid	⊢ ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) = ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) )
31		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
32	30 23 2 31	coe1fvalcl	⊢ ( ( ( 𝑥 𝑀 𝑦 ) ∈ ( Base ‘ 𝑃 ) ∧ 0 ∈ ℕ₀ ) → ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
33	28 29 32	sylancl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) )
34	22 33	jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) )
35	34	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) )
36		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
37		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
38	2 36 31 37	coe1scl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑙 ∈ ℕ₀ ↦ if ( 𝑙 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) ) )
39	35 38	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) = ( 𝑙 ∈ ℕ₀ ↦ if ( 𝑙 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) ) )
40	39	fveq1d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( 𝑙 ∈ ℕ₀ ↦ if ( 𝑙 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) ) ‘ 𝑛 ) )
41		eqidd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ ℕ₀ ↦ if ( 𝑙 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) ) = ( 𝑙 ∈ ℕ₀ ↦ if ( 𝑙 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) ) )
42		eqeq1	⊢ ( 𝑙 = 𝑛 → ( 𝑙 = 0 ↔ 𝑛 = 0 ) )
43	42	ifbid	⊢ ( 𝑙 = 𝑛 → if ( 𝑙 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) = if ( 𝑛 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) )
44	43	adantl	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑙 = 𝑛 ) → if ( 𝑙 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) = if ( 𝑛 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) )
45		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀ )
46	45	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ₀ )
47		fvex	⊢ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ V
48		fvex	⊢ ( 0_g ‘ 𝑅 ) ∈ V
49	47 48	ifex	⊢ if ( 𝑛 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) ∈ V
50	49	a1i	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) ∈ V )
51	41 44 46 50	fvmptd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ₀ ↦ if ( 𝑙 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) ) ‘ 𝑛 ) = if ( 𝑛 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) )
52		nnne0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
53	52	neneqd	⊢ ( 𝑛 ∈ ℕ → ¬ 𝑛 = 0 )
54	53	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ¬ 𝑛 = 0 )
55	54	iffalsed	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 = 0 , ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) , ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑅 ) )
56	40 51 55	3eqtrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) )
57		eqcom	⊢ ( ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ↔ ( 0_g ‘ 𝑅 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )
58	57	biimpi	⊢ ( ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) → ( 0_g ‘ 𝑅 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )
59	56 58	sylan9eq	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) → ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )
60	59	ex	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) → ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ) )
61	60	ralimdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ) )
62	61	imp	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) → ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )
63	34	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) → ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) )
64	2 36 31	ply1sclid	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) = ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) )
65	64	eqcomd	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) )
66	63 65	syl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) → ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) )
67	62 66	jca	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ∧ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
68	67	ex	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( 0_g ‘ 𝑅 ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ∧ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) )
69	21 68	syl5bi	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ∧ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) )
70	19 69	syld	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∀ 𝑘 ∈ ℕ ( ( coe₁ ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) = ( 0_g ‘ 𝑅 ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ∧ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) )
71	8 70	mpd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ∧ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
72		c0ex	⊢ 0 ∈ V
73		fveq2	⊢ ( 𝑛 = 0 → ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) )
74		fveq2	⊢ ( 𝑛 = 0 → ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) )
75	73 74	eqeq12d	⊢ ( 𝑛 = 0 → ( ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ↔ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) )
76	75	ralunsn	⊢ ( 0 ∈ V → ( ∀ 𝑛 ∈ ( ℕ ∪ { 0 } ) ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ↔ ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ∧ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) )
77	72 76	mp1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ∀ 𝑛 ∈ ( ℕ ∪ { 0 } ) ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ↔ ( ∀ 𝑛 ∈ ℕ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ∧ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 0 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) )
78	71 77	mpbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ∀ 𝑛 ∈ ( ℕ ∪ { 0 } ) ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )
79		df-n0	⊢ ℕ₀ = ( ℕ ∪ { 0 } )
80	79	raleqi	⊢ ( ∀ 𝑛 ∈ ℕ₀ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( ℕ ∪ { 0 } ) ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )
81	78 80	sylibr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ∀ 𝑛 ∈ ℕ₀ ( ( coe₁ ‘ ( ( algSc ‘ 𝑃 ) ‘ ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 0 ) ) ) ‘ 𝑛 ) = ( ( coe₁ ‘ ( 𝑥 𝑀 𝑦 ) ) ‘ 𝑛 ) )

Metamath Proof Explorer

Theorem m2cpminvid2lem

Proof