ldepsprlem

	Ref	Expression
Hypotheses	snlindsntor.b	$⊢ B = {Base}_{M}$
	snlindsntor.r	$⊢ R = Scalar (M)$
	snlindsntor.s	$⊢ S = {Base}_{R}$
	snlindsntor.0	$⊢ \underset{˙}{0} = 0_{R}$
	snlindsntor.z	$⊢ Z = 0_{M}$
	snlindsntor.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	ldepsprlem.1	$⊢ \underset{˙}{1} = 1_{R}$
	ldepsprlem.n	$⊢ N = {inv}_{g} (R)$
Assertion	ldepsprlem	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (X = A \underset{˙}{\cdot} Y \to (\underset{˙}{1} \underset{˙}{\cdot} X) +_{M} (N (A) \underset{˙}{\cdot} Y) = Z)$

Proof

Step	Hyp	Ref	Expression
1		snlindsntor.b	$⊢ B = {Base}_{M}$
2		snlindsntor.r	$⊢ R = Scalar (M)$
3		snlindsntor.s	$⊢ S = {Base}_{R}$
4		snlindsntor.0	$⊢ \underset{˙}{0} = 0_{R}$
5		snlindsntor.z	$⊢ Z = 0_{M}$
6		snlindsntor.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
7		ldepsprlem.1	$⊢ \underset{˙}{1} = 1_{R}$
8		ldepsprlem.n	$⊢ N = {inv}_{g} (R)$
9		oveq2	$⊢ X = A \underset{˙}{\cdot} Y \to \underset{˙}{1} \underset{˙}{\cdot} X = \underset{˙}{1} \underset{˙}{\cdot} (A \underset{˙}{\cdot} Y)$
10	9	oveq1d	$⊢ X = A \underset{˙}{\cdot} Y \to (\underset{˙}{1} \underset{˙}{\cdot} X) +_{M} (N (A) \underset{˙}{\cdot} Y) = (\underset{˙}{1} \underset{˙}{\cdot} (A \underset{˙}{\cdot} Y)) +_{M} (N (A) \underset{˙}{\cdot} Y)$
11		simpl	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to M \in LMod$
12	2 3 7	lmod1cl	$⊢ M \in LMod \to \underset{˙}{1} \in S$
13	12	adantr	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to \underset{˙}{1} \in S$
14		simpr3	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to A \in S$
15		simpr2	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to Y \in B$
16		eqid	$⊢ \cdot_{R} = \cdot_{R}$
17	1 2 6 3 16	lmodvsass	$⊢ (M \in LMod \land (\underset{˙}{1} \in S \land A \in S \land Y \in B)) \to (\underset{˙}{1} \cdot_{R} A) \underset{˙}{\cdot} Y = \underset{˙}{1} \underset{˙}{\cdot} (A \underset{˙}{\cdot} Y)$
18	11 13 14 15 17	syl13anc	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (\underset{˙}{1} \cdot_{R} A) \underset{˙}{\cdot} Y = \underset{˙}{1} \underset{˙}{\cdot} (A \underset{˙}{\cdot} Y)$
19	18	eqcomd	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to \underset{˙}{1} \underset{˙}{\cdot} (A \underset{˙}{\cdot} Y) = (\underset{˙}{1} \cdot_{R} A) \underset{˙}{\cdot} Y$
20	19	oveq1d	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (\underset{˙}{1} \underset{˙}{\cdot} (A \underset{˙}{\cdot} Y)) +_{M} (N (A) \underset{˙}{\cdot} Y) = ((\underset{˙}{1} \cdot_{R} A) \underset{˙}{\cdot} Y) +_{M} (N (A) \underset{˙}{\cdot} Y)$
21	2	lmodring	$⊢ M \in LMod \to R \in Ring$
22		simp3	$⊢ (X \in B \land Y \in B \land A \in S) \to A \in S$
23	3 16 7	ringlidm	$⊢ (R \in Ring \land A \in S) \to \underset{˙}{1} \cdot_{R} A = A$
24	21 22 23	syl2an	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to \underset{˙}{1} \cdot_{R} A = A$
25	24	oveq1d	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (\underset{˙}{1} \cdot_{R} A) \underset{˙}{\cdot} Y = A \underset{˙}{\cdot} Y$
26	25	oveq1d	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to ((\underset{˙}{1} \cdot_{R} A) \underset{˙}{\cdot} Y) +_{M} (N (A) \underset{˙}{\cdot} Y) = (A \underset{˙}{\cdot} Y) +_{M} (N (A) \underset{˙}{\cdot} Y)$
27	2	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
28	3 8	grpinvcl	$⊢ (R \in Grp \land A \in S) \to N (A) \in S$
29	27 22 28	syl2an	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to N (A) \in S$
30		eqid	$⊢ +_{M} = +_{M}$
31		eqid	$⊢ +_{R} = +_{R}$
32	1 30 2 6 3 31	lmodvsdir	$⊢ (M \in LMod \land (A \in S \land N (A) \in S \land Y \in B)) \to (A +_{R} N (A)) \underset{˙}{\cdot} Y = (A \underset{˙}{\cdot} Y) +_{M} (N (A) \underset{˙}{\cdot} Y)$
33	11 14 29 15 32	syl13anc	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (A +_{R} N (A)) \underset{˙}{\cdot} Y = (A \underset{˙}{\cdot} Y) +_{M} (N (A) \underset{˙}{\cdot} Y)$
34	3 31 4 8	grprinv	$⊢ (R \in Grp \land A \in S) \to A +_{R} N (A) = \underset{˙}{0}$
35	27 22 34	syl2an	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to A +_{R} N (A) = \underset{˙}{0}$
36	35	oveq1d	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (A +_{R} N (A)) \underset{˙}{\cdot} Y = \underset{˙}{0} \underset{˙}{\cdot} Y$
37	1 2 6 4 5	lmod0vs	$⊢ (M \in LMod \land Y \in B) \to \underset{˙}{0} \underset{˙}{\cdot} Y = Z$
38	37	3ad2antr2	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to \underset{˙}{0} \underset{˙}{\cdot} Y = Z$
39	36 38	eqtrd	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (A +_{R} N (A)) \underset{˙}{\cdot} Y = Z$
40	26 33 39	3eqtr2d	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to ((\underset{˙}{1} \cdot_{R} A) \underset{˙}{\cdot} Y) +_{M} (N (A) \underset{˙}{\cdot} Y) = Z$
41	20 40	eqtrd	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (\underset{˙}{1} \underset{˙}{\cdot} (A \underset{˙}{\cdot} Y)) +_{M} (N (A) \underset{˙}{\cdot} Y) = Z$
42	10 41	sylan9eqr	$⊢ ((M \in LMod \land (X \in B \land Y \in B \land A \in S)) \land X = A \underset{˙}{\cdot} Y) \to (\underset{˙}{1} \underset{˙}{\cdot} X) +_{M} (N (A) \underset{˙}{\cdot} Y) = Z$
43	42	ex	$⊢ (M \in LMod \land (X \in B \land Y \in B \land A \in S)) \to (X = A \underset{˙}{\cdot} Y \to (\underset{˙}{1} \underset{˙}{\cdot} X) +_{M} (N (A) \underset{˙}{\cdot} Y) = Z)$

Metamath Proof Explorer

Theorem ldepsprlem

Proof