scmateALT

Description: Alternate proof of scmate : An entry of an N x N scalar matrix over the ring R . This prove makes use of scmatmats but is longer and requires more distinct variables. (Contributed by AV, 19-Dec-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	scmatmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	scmatmat.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
	scmate.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	scmate.0	⊢ 0 = ( 0_g ‘ 𝑅 )
Assertion	scmateALT	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		scmatmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		scmatmat.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
4		scmate.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		scmate.0	⊢ 0 = ( 0_g ‘ 𝑅 )
6	1 2 3 4 5	scmatmats	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } )
7	6	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝑆 ↔ 𝑀 ∈ { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } ) )
8		oveq	⊢ ( 𝑚 = 𝑀 → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
9	8	eqeq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ↔ ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) )
10	9	2ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) )
11	10	rexbidv	⊢ ( 𝑚 = 𝑀 → ( ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ↔ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) )
12	11	elrab	⊢ ( 𝑀 ∈ { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } ↔ ( 𝑀 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) )
13		oveq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 𝑀 𝑗 ) = ( 𝐼 𝑀 𝑗 ) )
14		eqeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 = 𝑗 ↔ 𝐼 = 𝑗 ) )
15	14	ifbid	⊢ ( 𝑖 = 𝐼 → if ( 𝑖 = 𝑗 , 𝑐 , 0 ) = if ( 𝐼 = 𝑗 , 𝑐 , 0 ) )
16	13 15	eqeq12d	⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ↔ ( 𝐼 𝑀 𝑗 ) = if ( 𝐼 = 𝑗 , 𝑐 , 0 ) ) )
17		oveq2	⊢ ( 𝑗 = 𝐽 → ( 𝐼 𝑀 𝑗 ) = ( 𝐼 𝑀 𝐽 ) )
18		eqeq2	⊢ ( 𝑗 = 𝐽 → ( 𝐼 = 𝑗 ↔ 𝐼 = 𝐽 ) )
19	18	ifbid	⊢ ( 𝑗 = 𝐽 → if ( 𝐼 = 𝑗 , 𝑐 , 0 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) )
20	17 19	eqeq12d	⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 𝑀 𝑗 ) = if ( 𝐼 = 𝑗 , 𝑐 , 0 ) ↔ ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) )
21	16 20	rspc2v	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) )
22	21	reximdv	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) )
23	22	com12	⊢ ( ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) )
24	23	adantl	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) )
25	24	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑀 ∈ 𝐵 ∧ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑀 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) ) )
26	12 25	syl5bi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) ) )
27	7 26	sylbid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝑆 → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) ) )
28	27	ex	⊢ ( 𝑁 ∈ Fin → ( 𝑅 ∈ Ring → ( 𝑀 ∈ 𝑆 → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) ) ) )
29	28	3imp1	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) )

Metamath Proof Explorer

Theorem scmateALT

Proof