lincresunit3lem3

	Ref	Expression
Hypotheses	lincresunit3lem3.b	$⊢ B = {Base}_{M}$
	lincresunit3lem3.r	$⊢ R = Scalar (M)$
	lincresunit3lem3.e	$⊢ E = {Base}_{R}$
	lincresunit3lem3.u	$⊢ U = Unit (R)$
	lincresunit3lem3.n	$⊢ N = {inv}_{g} (R)$
	lincresunit3lem3.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
Assertion	lincresunit3lem3	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to (N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		lincresunit3lem3.b	$⊢ B = {Base}_{M}$
2		lincresunit3lem3.r	$⊢ R = Scalar (M)$
3		lincresunit3lem3.e	$⊢ E = {Base}_{R}$
4		lincresunit3lem3.u	$⊢ U = Unit (R)$
5		lincresunit3lem3.n	$⊢ N = {inv}_{g} (R)$
6		lincresunit3lem3.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
7		3simpa	$⊢ (M \in LMod \land X \in B \land Y \in B) \to (M \in LMod \land X \in B)$
8	7	adantr	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to (M \in LMod \land X \in B)$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	1 2 6 9	lmodvs1	$⊢ (M \in LMod \land X \in B) \to 1_{R} \underset{˙}{\cdot} X = X$
11	8 10	syl	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to 1_{R} \underset{˙}{\cdot} X = X$
12	2	lmodring	$⊢ M \in LMod \to R \in Ring$
13	12	3ad2ant1	$⊢ (M \in LMod \land X \in B \land Y \in B) \to R \in Ring$
14	13	adantr	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to R \in Ring$
15	4 5	unitnegcl	$⊢ (R \in Ring \land A \in U) \to N (A) \in U$
16	12 15	sylan	$⊢ (M \in LMod \land A \in U) \to N (A) \in U$
17	16	3ad2antl1	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to N (A) \in U$
18	14 17	jca	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to (R \in Ring \land N (A) \in U)$
19		eqid	$⊢ {inv}_{r} (R) = {inv}_{r} (R)$
20		eqid	$⊢ \cdot_{R} = \cdot_{R}$
21	4 19 20 9	unitlinv	$⊢ (R \in Ring \land N (A) \in U) \to {inv}_{r} (R) (N (A)) \cdot_{R} N (A) = 1_{R}$
22	18 21	syl	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to {inv}_{r} (R) (N (A)) \cdot_{R} N (A) = 1_{R}$
23	22	eqcomd	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to 1_{R} = {inv}_{r} (R) (N (A)) \cdot_{R} N (A)$
24	23	oveq1d	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to 1_{R} \underset{˙}{\cdot} X = ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} X$
25	11 24	eqtr3d	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to X = ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} X$
26	25	adantr	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to X = ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} X$
27		simpl1	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to M \in LMod$
28	4 19 3	ringinvcl	$⊢ (R \in Ring \land N (A) \in U) \to {inv}_{r} (R) (N (A)) \in E$
29	18 28	syl	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to {inv}_{r} (R) (N (A)) \in E$
30	2	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
31	30	3ad2ant1	$⊢ (M \in LMod \land X \in B \land Y \in B) \to R \in Grp$
32	3 4	unitcl	$⊢ A \in U \to A \in E$
33	3 5	grpinvcl	$⊢ (R \in Grp \land A \in E) \to N (A) \in E$
34	31 32 33	syl2an	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to N (A) \in E$
35		simpl2	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to X \in B$
36	29 34 35	3jca	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to ({inv}_{r} (R) (N (A)) \in E \land N (A) \in E \land X \in B)$
37	27 36	jca	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to (M \in LMod \land ({inv}_{r} (R) (N (A)) \in E \land N (A) \in E \land X \in B))$
38	37	adantr	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to (M \in LMod \land ({inv}_{r} (R) (N (A)) \in E \land N (A) \in E \land X \in B))$
39	1 2 6 3 20	lmodvsass	$⊢ (M \in LMod \land ({inv}_{r} (R) (N (A)) \in E \land N (A) \in E \land X \in B)) \to ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} X = {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} X)$
40	38 39	syl	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} X = {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} X)$
41		oveq2	$⊢ N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y \to {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} X) = {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} Y)$
42	41	adantl	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} X) = {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} Y)$
43	27	adantr	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to M \in LMod$
44		simpl3	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to Y \in B$
45	29 34 44	3jca	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to ({inv}_{r} (R) (N (A)) \in E \land N (A) \in E \land Y \in B)$
46	45	adantr	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to ({inv}_{r} (R) (N (A)) \in E \land N (A) \in E \land Y \in B)$
47	43 46	jca	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to (M \in LMod \land ({inv}_{r} (R) (N (A)) \in E \land N (A) \in E \land Y \in B))$
48	1 2 6 3 20	lmodvsass	$⊢ (M \in LMod \land ({inv}_{r} (R) (N (A)) \in E \land N (A) \in E \land Y \in B)) \to ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} Y = {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} Y)$
49	47 48	syl	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} Y = {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} Y)$
50	18	adantr	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to (R \in Ring \land N (A) \in U)$
51	50 21	syl	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to {inv}_{r} (R) (N (A)) \cdot_{R} N (A) = 1_{R}$
52	51	oveq1d	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} Y = 1_{R} \underset{˙}{\cdot} Y$
53	49 52	eqtr3d	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to {inv}_{r} (R) (N (A)) \underset{˙}{\cdot} (N (A) \underset{˙}{\cdot} Y) = 1_{R} \underset{˙}{\cdot} Y$
54	40 42 53	3eqtrd	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to ({inv}_{r} (R) (N (A)) \cdot_{R} N (A)) \underset{˙}{\cdot} X = 1_{R} \underset{˙}{\cdot} Y$
55		3simpb	$⊢ (M \in LMod \land X \in B \land Y \in B) \to (M \in LMod \land Y \in B)$
56	55	adantr	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to (M \in LMod \land Y \in B)$
57	56	adantr	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to (M \in LMod \land Y \in B)$
58	1 2 6 9	lmodvs1	$⊢ (M \in LMod \land Y \in B) \to 1_{R} \underset{˙}{\cdot} Y = Y$
59	57 58	syl	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to 1_{R} \underset{˙}{\cdot} Y = Y$
60	26 54 59	3eqtrd	$⊢ (((M \in LMod \land X \in B \land Y \in B) \land A \in U) \land N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y) \to X = Y$
61	60	ex	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to (N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y \to X = Y)$
62		oveq2	$⊢ X = Y \to N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y$
63	61 62	impbid1	$⊢ ((M \in LMod \land X \in B \land Y \in B) \land A \in U) \to (N (A) \underset{˙}{\cdot} X = N (A) \underset{˙}{\cdot} Y \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem lincresunit3lem3

Proof