Theorem lmod1lem5

Description: Lemma 5 for lmod1 . (Contributed by AV, 28-Apr-2019)

	Ref	Expression
Hypothesis	lmod1.m	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
Assertion	lmod1lem5	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		lmod1.m	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
2		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
3		snex	⊢ { 𝐼 } ∈ V
4	2 3	pm3.2i	⊢ ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V )
5	4	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) )
6		mpoexga	⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V )
7	1	lmodvsca	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
8	5 6 7	3syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
9	8	eqcomd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ·𝑠 ‘ 𝑀 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) )
10		simprr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 = ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 )
11	1	lmodsca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑀 ) )
12	11	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝑀 ) )
13	12	eqcomd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝑀 ) = 𝑅 )
14	13	fveq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( 1r ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ 𝑅 ) )
15		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
17	15 16	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
18	17	adantl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
19	14 18	eqeltrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∈ ( Base ‘ 𝑅 ) )
20		snidg	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } )
21	20	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝐼 ∈ { 𝐼 } )
22	9 10 19 21 21	ovmpod	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )