matsubgcell

Description: Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019)

	Ref	Expression
Hypotheses	matplusgcell.a	$⊢ A = N Mat R$
	matplusgcell.b	$⊢ B = {Base}_{A}$
	matsubgcell.s	$⊢ S = -_{A}$
	matsubgcell.m	$⊢ \underset{˙}{-} = -_{R}$
Assertion	matsubgcell	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X S Y) J = (I X J) \underset{˙}{-} (I Y J)$

Proof

Step	Hyp	Ref	Expression
1		matplusgcell.a	$⊢ A = N Mat R$
2		matplusgcell.b	$⊢ B = {Base}_{A}$
3		matsubgcell.s	$⊢ S = -_{A}$
4		matsubgcell.m	$⊢ \underset{˙}{-} = -_{R}$
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	6	adantr	$⊢ (X \in B \land Y \in B) \to N \in Fin$
8	7	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to N \in Fin$
9		simp1	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to R \in Ring$
10		eqid	$⊢ R freeLMod (N \times N) = R freeLMod (N \times N)$
11	1 10	matsubg	$⊢ (N \in Fin \land R \in Ring) \to -_{(R freeLMod (N \times N))} = -_{A}$
12	8 9 11	syl2anc	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to -_{(R freeLMod (N \times N))} = -_{A}$
13	3 12	eqtr4id	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to S = -_{(R freeLMod (N \times N))}$
14	13	oveqd	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to X S Y = X -_{(R freeLMod (N \times N))} Y$
15		eqid	$⊢ {Base}_{(R freeLMod (N \times N))} = {Base}_{(R freeLMod (N \times N))}$
16		xpfi	$⊢ (N \in Fin \land N \in Fin) \to N \times N \in Fin$
17	16	anidms	$⊢ N \in Fin \to N \times N \in Fin$
18	17	adantr	$⊢ (N \in Fin \land R \in V) \to N \times N \in Fin$
19	5 18	syl	$⊢ X \in B \to N \times N \in Fin$
20	19	adantr	$⊢ (X \in B \land Y \in B) \to N \times N \in Fin$
21	20	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to N \times N \in Fin$
22	2	eleq2i	$⊢ X \in B \leftrightarrow X \in {Base}_{A}$
23	22	biimpi	$⊢ X \in B \to X \in {Base}_{A}$
24	1 10	matbas	$⊢ (N \in Fin \land R \in V) \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
25	5 24	syl	$⊢ X \in B \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
26	23 25	eleqtrrd	$⊢ X \in B \to X \in {Base}_{(R freeLMod (N \times N))}$
27	26	adantr	$⊢ (X \in B \land Y \in B) \to X \in {Base}_{(R freeLMod (N \times N))}$
28	27	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to X \in {Base}_{(R freeLMod (N \times N))}$
29	2	eleq2i	$⊢ Y \in B \leftrightarrow Y \in {Base}_{A}$
30	29	biimpi	$⊢ Y \in B \to Y \in {Base}_{A}$
31	1 2	matrcl	$⊢ Y \in B \to (N \in Fin \land R \in V)$
32	31 24	syl	$⊢ Y \in B \to {Base}_{(R freeLMod (N \times N))} = {Base}_{A}$
33	30 32	eleqtrrd	$⊢ Y \in B \to Y \in {Base}_{(R freeLMod (N \times N))}$
34	33	adantl	$⊢ (X \in B \land Y \in B) \to Y \in {Base}_{(R freeLMod (N \times N))}$
35	34	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to Y \in {Base}_{(R freeLMod (N \times N))}$
36		eqid	$⊢ -_{(R freeLMod (N \times N))} = -_{(R freeLMod (N \times N))}$
37	10 15 9 21 28 35 4 36	frlmsubgval	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to X -_{(R freeLMod (N \times N))} Y = X {\underset{˙}{-}}_{f} Y$
38	14 37	eqtrd	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to X S Y = X {\underset{˙}{-}}_{f} Y$
39	38	oveqd	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X S Y) J = I (X {\underset{˙}{-}}_{f} Y) J$
40		df-ov	$⊢ I (X {\underset{˙}{-}}_{f} Y) J = (X {\underset{˙}{-}}_{f} Y) (⟨I, J⟩)$
41		opelxpi	$⊢ (I \in N \land J \in N) \to ⟨I, J⟩ \in (N \times N)$
42	41	anim2i	$⊢ ((X \in B \land Y \in B) \land (I \in N \land J \in N)) \to ((X \in B \land Y \in B) \land ⟨I, J⟩ \in (N \times N))$
43	42	3adant1	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to ((X \in B \land Y \in B) \land ⟨I, J⟩ \in (N \times N))$
44		eqid	$⊢ {Base}_{R} = {Base}_{R}$
45	1 44 2	matbas2i	$⊢ X \in B \to X \in ({Base}_{R}^{(N \times N)})$
46		elmapfn	$⊢ X \in ({Base}_{R}^{(N \times N)}) \to X Fn (N \times N)$
47	45 46	syl	$⊢ X \in B \to X Fn (N \times N)$
48	47	adantr	$⊢ (X \in B \land Y \in B) \to X Fn (N \times N)$
49	1 44 2	matbas2i	$⊢ Y \in B \to Y \in ({Base}_{R}^{(N \times N)})$
50		elmapfn	$⊢ Y \in ({Base}_{R}^{(N \times N)}) \to Y Fn (N \times N)$
51	49 50	syl	$⊢ Y \in B \to Y Fn (N \times N)$
52	51	adantl	$⊢ (X \in B \land Y \in B) \to Y Fn (N \times N)$
53		inidm	$⊢ (N \times N) \cap (N \times N) = N \times N$
54		df-ov	$⊢ I X J = X (⟨I, J⟩)$
55	54	eqcomi	$⊢ X (⟨I, J⟩) = I X J$
56	55	a1i	$⊢ ((X \in B \land Y \in B) \land ⟨I, J⟩ \in (N \times N)) \to X (⟨I, J⟩) = I X J$
57		df-ov	$⊢ I Y J = Y (⟨I, J⟩)$
58	57	eqcomi	$⊢ Y (⟨I, J⟩) = I Y J$
59	58	a1i	$⊢ ((X \in B \land Y \in B) \land ⟨I, J⟩ \in (N \times N)) \to Y (⟨I, J⟩) = I Y J$
60	48 52 20 20 53 56 59	ofval	$⊢ ((X \in B \land Y \in B) \land ⟨I, J⟩ \in (N \times N)) \to (X {\underset{˙}{-}}_{f} Y) (⟨I, J⟩) = (I X J) \underset{˙}{-} (I Y J)$
61	43 60	syl	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to (X {\underset{˙}{-}}_{f} Y) (⟨I, J⟩) = (I X J) \underset{˙}{-} (I Y J)$
62	40 61	syl5eq	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X {\underset{˙}{-}}_{f} Y) J = (I X J) \underset{˙}{-} (I Y J)$
63	39 62	eqtrd	$⊢ (R \in Ring \land (X \in B \land Y \in B) \land (I \in N \land J \in N)) \to I (X S Y) J = (I X J) \underset{˙}{-} (I Y J)$

Metamath Proof Explorer

Theorem matsubgcell

Proof