matinvgcell

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

	Ref	Expression
Hypotheses	matplusgcell.a	$⊢ A = N Mat R$
	matplusgcell.b	$⊢ B = {Base}_{A}$
	matinvgcell.v	$⊢ V = {inv}_{g} (R)$
	matinvgcell.w	$⊢ W = {inv}_{g} (A)$
Assertion	matinvgcell	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to I W (X) J = V (I X J)$

Proof

Step	Hyp	Ref	Expression
1		matplusgcell.a	$⊢ A = N Mat R$
2		matplusgcell.b	$⊢ B = {Base}_{A}$
3		matinvgcell.v	$⊢ V = {inv}_{g} (R)$
4		matinvgcell.w	$⊢ W = {inv}_{g} (A)$
5	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
6	5	simpld	$⊢ X \in B \to N \in Fin$
7		simpl	$⊢ (R \in Ring \land X \in B) \to R \in Ring$
8	1	matgrp	$⊢ (N \in Fin \land R \in Ring) \to A \in Grp$
9	6 7 8	syl2an2	$⊢ (R \in Ring \land X \in B) \to A \in Grp$
10		eqid	$⊢ 0_{A} = 0_{A}$
11	2 10	grpidcl	$⊢ A \in Grp \to 0_{A} \in B$
12	9 11	syl	$⊢ (R \in Ring \land X \in B) \to 0_{A} \in B$
13		simpr	$⊢ (R \in Ring \land X \in B) \to X \in B$
14	12 13	jca	$⊢ (R \in Ring \land X \in B) \to (0_{A} \in B \land X \in B)$
15	14	3adant3	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to (0_{A} \in B \land X \in B)$
16		eqid	$⊢ -_{A} = -_{A}$
17		eqid	$⊢ -_{R} = -_{R}$
18	1 2 16 17	matsubgcell	$⊢ (R \in Ring \land (0_{A} \in B \land X \in B) \land (I \in N \land J \in N)) \to I (0_{A} -_{A} X) J = (I 0_{A} J) -_{R} (I X J)$
19	15 18	syld3an2	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to I (0_{A} -_{A} X) J = (I 0_{A} J) -_{R} (I X J)$
20	2 16 4 10	grpinvval2	$⊢ (A \in Grp \land X \in B) \to W (X) = 0_{A} -_{A} X$
21	9 13 20	syl2anc	$⊢ (R \in Ring \land X \in B) \to W (X) = 0_{A} -_{A} X$
22	21	3adant3	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to W (X) = 0_{A} -_{A} X$
23	22	oveqd	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to I W (X) J = I (0_{A} -_{A} X) J$
24		ringgrp	$⊢ R \in Ring \to R \in Grp$
25	24	3ad2ant1	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to R \in Grp$
26		simp3	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to (I \in N \land J \in N)$
27	2	eleq2i	$⊢ X \in B \leftrightarrow X \in {Base}_{A}$
28	27	biimpi	$⊢ X \in B \to X \in {Base}_{A}$
29	28	3ad2ant2	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to X \in {Base}_{A}$
30		df-3an	$⊢ (I \in N \land J \in N \land X \in {Base}_{A}) \leftrightarrow ((I \in N \land J \in N) \land X \in {Base}_{A})$
31	26 29 30	sylanbrc	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to (I \in N \land J \in N \land X \in {Base}_{A})$
32		eqid	$⊢ {Base}_{R} = {Base}_{R}$
33	1 32	matecl	$⊢ (I \in N \land J \in N \land X \in {Base}_{A}) \to I X J \in {Base}_{R}$
34	31 33	syl	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to I X J \in {Base}_{R}$
35		eqid	$⊢ 0_{R} = 0_{R}$
36	32 17 3 35	grpinvval2	$⊢ (R \in Grp \land I X J \in {Base}_{R}) \to V (I X J) = 0_{R} -_{R} (I X J)$
37	25 34 36	syl2anc	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to V (I X J) = 0_{R} -_{R} (I X J)$
38	6	anim1i	$⊢ (X \in B \land R \in Ring) \to (N \in Fin \land R \in Ring)$
39	38	ancoms	$⊢ (R \in Ring \land X \in B) \to (N \in Fin \land R \in Ring)$
40	1 35	mat0op	$⊢ (N \in Fin \land R \in Ring) \to 0_{A} = (x \in N, y \in N ⟼ 0_{R})$
41	39 40	syl	$⊢ (R \in Ring \land X \in B) \to 0_{A} = (x \in N, y \in N ⟼ 0_{R})$
42	41	3adant3	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to 0_{A} = (x \in N, y \in N ⟼ 0_{R})$
43		eqidd	$⊢ ((R \in Ring \land X \in B \land (I \in N \land J \in N)) \land (x = I \land y = J)) \to 0_{R} = 0_{R}$
44	26	simpld	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to I \in N$
45		simp3r	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to J \in N$
46		fvexd	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to 0_{R} \in V$
47	42 43 44 45 46	ovmpod	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to I 0_{A} J = 0_{R}$
48	47	eqcomd	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to 0_{R} = I 0_{A} J$
49	48	oveq1d	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to 0_{R} -_{R} (I X J) = (I 0_{A} J) -_{R} (I X J)$
50	37 49	eqtrd	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to V (I X J) = (I 0_{A} J) -_{R} (I X J)$
51	19 23 50	3eqtr4d	$⊢ (R \in Ring \land X \in B \land (I \in N \land J \in N)) \to I W (X) J = V (I X J)$

Metamath Proof Explorer

Theorem matinvgcell

Proof