Theorem lmod1lem1

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

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

Proof

Step	Hyp	Ref	Expression
1		lmod1.m	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
2		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
3		snex	⊢ { 𝐼 } ∈ V
4	3	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → { 𝐼 } ∈ V )
5		mpoexga	⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V )
6	2 4 5	sylancr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V )
7	1	lmodvsca	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
8	6 7	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
9	8	eqcomd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ·𝑠 ‘ 𝑀 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) )
10		simprr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 = 𝑟 ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 )
11		simp3	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → 𝑟 ∈ ( Base ‘ 𝑅 ) )
12		snidg	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } )
13	12	3ad2ant1	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → 𝐼 ∈ { 𝐼 } )
14	9 10 11 13 13	ovmpod	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
15	14 13	eqeltrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ∈ { 𝐼 } )