lincresunit3lem1

	Ref	Expression
Hypotheses	lincresunit.b	$⊢ B = {Base}_{M}$
	lincresunit.r	$⊢ R = Scalar (M)$
	lincresunit.e	$⊢ E = {Base}_{R}$
	lincresunit.u	$⊢ U = Unit (R)$
	lincresunit.0	$⊢ \underset{˙}{0} = 0_{R}$
	lincresunit.z	$⊢ Z = 0_{M}$
	lincresunit.n	$⊢ N = {inv}_{g} (R)$
	lincresunit.i	$⊢ I = {inv}_{r} (R)$
	lincresunit.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	lincresunit.g	$⊢ G = (s \in (S ∖ \{X\}) ⟼ I (N (F (X))) \underset{˙}{\cdot} F (s))$
Assertion	lincresunit3lem1	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to N (F (X)) \cdot_{M} (G (z) \cdot_{M} z) = F (z) \cdot_{M} z$

Proof

Step	Hyp	Ref	Expression
1		lincresunit.b	$⊢ B = {Base}_{M}$
2		lincresunit.r	$⊢ R = Scalar (M)$
3		lincresunit.e	$⊢ E = {Base}_{R}$
4		lincresunit.u	$⊢ U = Unit (R)$
5		lincresunit.0	$⊢ \underset{˙}{0} = 0_{R}$
6		lincresunit.z	$⊢ Z = 0_{M}$
7		lincresunit.n	$⊢ N = {inv}_{g} (R)$
8		lincresunit.i	$⊢ I = {inv}_{r} (R)$
9		lincresunit.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
10		lincresunit.g	$⊢ G = (s \in (S ∖ \{X\}) ⟼ I (N (F (X))) \underset{˙}{\cdot} F (s))$
11		fveq2	$⊢ s = z \to F (s) = F (z)$
12	11	oveq2d	$⊢ s = z \to I (N (F (X))) \underset{˙}{\cdot} F (s) = I (N (F (X))) \underset{˙}{\cdot} F (z)$
13		simpr3	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to z \in (S ∖ \{X\})$
14		ovexd	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to I (N (F (X))) \underset{˙}{\cdot} F (z) \in V$
15	10 12 13 14	fvmptd3	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to G (z) = I (N (F (X))) \underset{˙}{\cdot} F (z)$
16	15	oveq1d	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to G (z) \cdot_{M} z = (I (N (F (X))) \underset{˙}{\cdot} F (z)) \cdot_{M} z$
17	16	oveq2d	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to N (F (X)) \cdot_{M} (G (z) \cdot_{M} z) = N (F (X)) \cdot_{M} ((I (N (F (X))) \underset{˙}{\cdot} F (z)) \cdot_{M} z)$
18		simp2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to M \in LMod$
19	18	adantr	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to M \in LMod$
20	2	lmodfgrp	$⊢ M \in LMod \to R \in Grp$
21	20	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to R \in Grp$
22	3 4	unitcl	$⊢ F (X) \in U \to F (X) \in E$
23	22	3ad2ant2	$⊢ (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\})) \to F (X) \in E$
24	3 7	grpinvcl	$⊢ (R \in Grp \land F (X) \in E) \to N (F (X)) \in E$
25	21 23 24	syl2an	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to N (F (X)) \in E$
26		3simpa	$⊢ (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\})) \to (F \in (E^{S}) \land F (X) \in U)$
27	26	anim2i	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U))$
28		eldifi	$⊢ z \in (S ∖ \{X\}) \to z \in S$
29	28	3ad2ant3	$⊢ (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\})) \to z \in S$
30	29	adantl	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to z \in S$
31	1 2 3 4 5 6 7 8 9 10	lincresunitlem2	$⊢ (((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U)) \land z \in S) \to I (N (F (X))) \underset{˙}{\cdot} F (z) \in E$
32	27 30 31	syl2anc	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to I (N (F (X))) \underset{˙}{\cdot} F (z) \in E$
33		elpwi	$⊢ S \in 𝒫 B \to S \subseteq B$
34	33	sseld	$⊢ S \in 𝒫 B \to (z \in S \to z \in B)$
35	28 34	syl5com	$⊢ z \in (S ∖ \{X\}) \to (S \in 𝒫 B \to z \in B)$
36	35	3ad2ant3	$⊢ (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\})) \to (S \in 𝒫 B \to z \in B)$
37	36	com12	$⊢ S \in 𝒫 B \to ((F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\})) \to z \in B)$
38	37	3ad2ant1	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to ((F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\})) \to z \in B)$
39	38	imp	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to z \in B$
40		eqid	$⊢ \cdot_{M} = \cdot_{M}$
41	1 2 40 3 9	lmodvsass	$⊢ (M \in LMod \land (N (F (X)) \in E \land I (N (F (X))) \underset{˙}{\cdot} F (z) \in E \land z \in B)) \to (N (F (X)) \underset{˙}{\cdot} (I (N (F (X))) \underset{˙}{\cdot} F (z))) \cdot_{M} z = N (F (X)) \cdot_{M} ((I (N (F (X))) \underset{˙}{\cdot} F (z)) \cdot_{M} z)$
42	41	eqcomd	$⊢ (M \in LMod \land (N (F (X)) \in E \land I (N (F (X))) \underset{˙}{\cdot} F (z) \in E \land z \in B)) \to N (F (X)) \cdot_{M} ((I (N (F (X))) \underset{˙}{\cdot} F (z)) \cdot_{M} z) = (N (F (X)) \underset{˙}{\cdot} (I (N (F (X))) \underset{˙}{\cdot} F (z))) \cdot_{M} z$
43	19 25 32 39 42	syl13anc	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to N (F (X)) \cdot_{M} ((I (N (F (X))) \underset{˙}{\cdot} F (z)) \cdot_{M} z) = (N (F (X)) \underset{˙}{\cdot} (I (N (F (X))) \underset{˙}{\cdot} F (z))) \cdot_{M} z$
44	2	lmodring	$⊢ M \in LMod \to R \in Ring$
45	44	3ad2ant2	$⊢ (S \in 𝒫 B \land M \in LMod \land X \in S) \to R \in Ring$
46	45	adantr	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to R \in Ring$
47		elmapi	$⊢ F \in (E^{S}) \to F : S ⟶ E$
48		ffvelrn	$⊢ (F : S ⟶ E \land z \in S) \to F (z) \in E$
49	47 28 48	syl2an	$⊢ (F \in (E^{S}) \land z \in (S ∖ \{X\})) \to F (z) \in E$
50	49	3adant2	$⊢ (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\})) \to F (z) \in E$
51	50	adantl	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to F (z) \in E$
52		simp2	$⊢ (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\})) \to F (X) \in U$
53	52	adantl	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to F (X) \in U$
54	3 4 7 8 9	invginvrid	$⊢ (R \in Ring \land F (z) \in E \land F (X) \in U) \to N (F (X)) \underset{˙}{\cdot} (I (N (F (X))) \underset{˙}{\cdot} F (z)) = F (z)$
55	46 51 53 54	syl3anc	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to N (F (X)) \underset{˙}{\cdot} (I (N (F (X))) \underset{˙}{\cdot} F (z)) = F (z)$
56	55	oveq1d	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to (N (F (X)) \underset{˙}{\cdot} (I (N (F (X))) \underset{˙}{\cdot} F (z))) \cdot_{M} z = F (z) \cdot_{M} z$
57	17 43 56	3eqtrd	$⊢ ((S \in 𝒫 B \land M \in LMod \land X \in S) \land (F \in (E^{S}) \land F (X) \in U \land z \in (S ∖ \{X\}))) \to N (F (X)) \cdot_{M} (G (z) \cdot_{M} z) = F (z) \cdot_{M} z$

Metamath Proof Explorer

Theorem lincresunit3lem1

Proof