Theorem matinvgcell

Description: Additive inversion in the matrix ring is cell-wise. (Contributed by AV, 17-Nov-2019)

	Ref	Expression
Hypotheses	matplusgcell.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matplusgcell.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	matinvgcell.v	⊢ 𝑉 = ( invg ‘ 𝑅 )
	matinvgcell.w	⊢ 𝑊 = ( invg ‘ 𝐴 )
Assertion	matinvgcell	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑊 ‘ 𝑋 ) 𝐽 ) = ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		matplusgcell.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matplusgcell.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		matinvgcell.v	⊢ 𝑉 = ( invg ‘ 𝑅 )
4		matinvgcell.w	⊢ 𝑊 = ( invg ‘ 𝐴 )
5	1 2	matrcl	⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6	5	simpld	⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
7		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Ring )
8	1	matgrp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp )
9	6 7 8	syl2an2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝐴 ∈ Grp )
10		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
11	2 10	grpidcl	⊢ ( 𝐴 ∈ Grp → ( 0g ‘ 𝐴 ) ∈ 𝐵 )
12	9 11	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ 𝐴 ) ∈ 𝐵 )
13		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
14	12 13	jca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( ( 0g ‘ 𝐴 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
15	14	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 0g ‘ 𝐴 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
16		eqid	⊢ ( -g ‘ 𝐴 ) = ( -g ‘ 𝐴 )
17		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
18	1 2 16 17	matsubgcell	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 0g ‘ 𝐴 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( ( 0g ‘ 𝐴 ) ( -g ‘ 𝐴 ) 𝑋 ) 𝐽 ) = ( ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) ( -g ‘ 𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
19	15 18	syld3an2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( ( 0g ‘ 𝐴 ) ( -g ‘ 𝐴 ) 𝑋 ) 𝐽 ) = ( ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) ( -g ‘ 𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
20	2 16 4 10	grpinvval2	⊢ ( ( 𝐴 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑊 ‘ 𝑋 ) = ( ( 0g ‘ 𝐴 ) ( -g ‘ 𝐴 ) 𝑋 ) )
21	9 13 20	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑊 ‘ 𝑋 ) = ( ( 0g ‘ 𝐴 ) ( -g ‘ 𝐴 ) 𝑋 ) )
22	21	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑊 ‘ 𝑋 ) = ( ( 0g ‘ 𝐴 ) ( -g ‘ 𝐴 ) 𝑋 ) )
23	22	oveqd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑊 ‘ 𝑋 ) 𝐽 ) = ( 𝐼 ( ( 0g ‘ 𝐴 ) ( -g ‘ 𝐴 ) 𝑋 ) 𝐽 ) )
24		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
25	24	3ad2ant1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑅 ∈ Grp )
26		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) )
27	2	eleq2i	⊢ ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( Base ‘ 𝐴 ) )
28	27	biimpi	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
29	28	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
30		df-3an	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) ↔ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) )
31	26 29 30	sylanbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) )
32		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
33	1 32	matecl	⊢ ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
34	31 33	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
35		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
36	32 17 3 35	grpinvval2	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝐼 𝑋 𝐽 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) = ( ( 0g ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
37	25 34 36	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) = ( ( 0g ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
38	6	anim1i	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
39	38	ancoms	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
40	1 35	mat0op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐴 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
41	39 40	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ 𝐴 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
42	41	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 0g ‘ 𝐴 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 0g ‘ 𝑅 ) ) )
43		eqidd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ ( 𝑥 = 𝐼 ∧ 𝑦 = 𝐽 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) )
44	26	simpld	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
45		simp3r	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐽 ∈ 𝑁 )
46		fvexd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
47	42 43 44 45 46	ovmpod	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) = ( 0g ‘ 𝑅 ) )
48	47	eqcomd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) = ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) )
49	48	oveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 0g ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 𝐼 𝑋 𝐽 ) ) = ( ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) ( -g ‘ 𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
50	37 49	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) = ( ( 𝐼 ( 0g ‘ 𝐴 ) 𝐽 ) ( -g ‘ 𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
51	19 23 50	3eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑊 ‘ 𝑋 ) 𝐽 ) = ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) )