Theorem lmod1lem2

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

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

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		mpoexga	⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V )
6	4 5	mp1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ 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		snex	⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
16	1	lmodplusg	⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
17	15 16	mp1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
18	17	eqcomd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( +g ‘ 𝑀 ) = { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } )
19	18	oveqd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
20		df-ov	⊢ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ )
21		opex	⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
22		simp1	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → 𝐼 ∈ 𝑉 )
23		fvsng	⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
24	21 22 23	sylancr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
25	20 24	syl5eq	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
26	19 25	eqtrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) = 𝐼 )
27	26	oveq2d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) )
28	3	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → { 𝐼 } ∈ V )
29	2 28 5	sylancr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V )
30	29 7	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
31	30	eqcomd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ·𝑠 ‘ 𝑀 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) )
32	31 10 11 13 13	ovmpod	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
33	32 32	oveq12d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) = ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) )
34	33 26	eqtrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) = 𝐼 )
35	14 27 34	3eqtr4d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) ) = ( ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )