lmod1lem5

		Ref	Expression
	Hypothesis	lmod1.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\}$
	Assertion	lmod1lem5	$⊢ (I \in V \land R \in Ring) \to 1_{Scalar (M)} \cdot_{M} I = I$

Proof

Step	Hyp	Ref	Expression
1		lmod1.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\}$
2		fvex	$⊢ {Base}_{R} \in V$
3		snex	$⊢ \{I\} \in V$
4	2 3	pm3.2i	$⊢ ({Base}_{R} \in V \land \{I\} \in V)$
5	4	a1i	$⊢ (I \in V \land R \in Ring) \to ({Base}_{R} \in V \land \{I\} \in V)$
6		mpoexga	$⊢ ({Base}_{R} \in V \land \{I\} \in V) \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) \in V$
7	1	lmodvsca	$⊢ (x \in {Base}_{R}, y \in \{I\} ⟼ y) \in V \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) = \cdot_{M}$
8	5 6 7	3syl	$⊢ (I \in V \land R \in Ring) \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) = \cdot_{M}$
9	8	eqcomd	$⊢ (I \in V \land R \in Ring) \to \cdot_{M} = (x \in {Base}_{R}, y \in \{I\} ⟼ y)$
10		simprr	$⊢ ((I \in V \land R \in Ring) \land (x = 1_{Scalar (M)} \land y = I)) \to y = I$
11	1	lmodsca	$⊢ R \in Ring \to R = Scalar (M)$
12	11	adantl	$⊢ (I \in V \land R \in Ring) \to R = Scalar (M)$
13	12	eqcomd	$⊢ (I \in V \land R \in Ring) \to Scalar (M) = R$
14	13	fveq2d	$⊢ (I \in V \land R \in Ring) \to 1_{Scalar (M)} = 1_{R}$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16		eqid	$⊢ 1_{R} = 1_{R}$
17	15 16	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
18	17	adantl	$⊢ (I \in V \land R \in Ring) \to 1_{R} \in {Base}_{R}$
19	14 18	eqeltrd	$⊢ (I \in V \land R \in Ring) \to 1_{Scalar (M)} \in {Base}_{R}$
20		snidg	$⊢ I \in V \to I \in \{I\}$
21	20	adantr	$⊢ (I \in V \land R \in Ring) \to I \in \{I\}$
22	9 10 19 21 21	ovmpod	$⊢ (I \in V \land R \in Ring) \to 1_{Scalar (M)} \cdot_{M} I = I$

Metamath Proof Explorer

Theorem lmod1lem5

Proof