Theorem pmat1ovscd

Description: Entries of the identity polynomial matrix over a ring represented with "lifted scalars", deduction form. (Contributed by AV, 16-Nov-2019)

	Ref	Expression
Hypotheses	pmat0opsc.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmat0opsc.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmat0opsc.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	pmat0opsc.z	⊢ 0 = ( 0g ‘ 𝑅 )
	pmat1opsc.o	⊢ 1 = ( 1r ‘ 𝑅 )
	pmat1ovscd.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	pmat1ovscd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	pmat1ovscd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
	pmat1ovscd.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
	pmat1ovscd.u	⊢ 𝑈 = ( 1r ‘ 𝐶 )
Assertion	pmat1ovscd	⊢ ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , ( 𝐴 ‘ 1 ) , ( 𝐴 ‘ 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmat0opsc.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmat0opsc.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmat0opsc.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
4		pmat0opsc.z	⊢ 0 = ( 0g ‘ 𝑅 )
5		pmat1opsc.o	⊢ 1 = ( 1r ‘ 𝑅 )
6		pmat1ovscd.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		pmat1ovscd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		pmat1ovscd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
9		pmat1ovscd.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
10		pmat1ovscd.u	⊢ 𝑈 = ( 1r ‘ 𝐶 )
11		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
12		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
13	1 2 11 12 6 7 8 9 10	pmat1ovd	⊢ ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) )
14	1 3 5 12	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = ( 1r ‘ 𝑃 ) )
15	7 14	syl	⊢ ( 𝜑 → ( 𝐴 ‘ 1 ) = ( 1r ‘ 𝑃 ) )
16	15	eqcomd	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 𝐴 ‘ 1 ) )
17	1 3 4 11	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
18	7 17	syl	⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
19	18	eqcomd	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 𝐴 ‘ 0 ) )
20	16 19	ifeq12d	⊢ ( 𝜑 → if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) = if ( 𝐼 = 𝐽 , ( 𝐴 ‘ 1 ) , ( 𝐴 ‘ 0 ) ) )
21	13 20	eqtrd	⊢ ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , ( 𝐴 ‘ 1 ) , ( 𝐴 ‘ 0 ) ) )