Theorem lmod1lem4

Description: Lemma 4 for lmod1 . (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Hypothesis	lmod1.m	⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
Assertion	lmod1lem4	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( .r ‘ ( 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 ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) )
6		mpoexga	⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V )
7	1	lmodvsca	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
8	5 6 7	3syl	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
9	8	eqcomd	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ·𝑠 ‘ 𝑀 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) )
10		simprr	⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = 𝑞 ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 )
11		simprl	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑞 ∈ ( Base ‘ 𝑅 ) )
12		snidg	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } )
13	12	ad2antrr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝐼 ∈ { 𝐼 } )
14	9 10 11 13 13	ovmpod	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
15		simprr	⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = 𝑟 ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 )
16		simprr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑟 ∈ ( Base ‘ 𝑅 ) )
17	9 15 16 13 13	ovmpod	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
18	17	oveq2d	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) )
19		simprr	⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 )
20		simplr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
21	1	lmodsca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑀 ) )
22	21	fveq2d	⊢ ( 𝑅 ∈ Ring → ( .r ‘ 𝑅 ) = ( .r ‘ ( Scalar ‘ 𝑀 ) ) )
23	20 22	syl	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( .r ‘ 𝑅 ) = ( .r ‘ ( Scalar ‘ 𝑀 ) ) )
24	23	eqcomd	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( .r ‘ ( Scalar ‘ 𝑀 ) ) = ( .r ‘ 𝑅 ) )
25	24	oveqd	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) = ( 𝑞 ( .r ‘ 𝑅 ) 𝑟 ) )
26		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
28	26 27	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑞 ( .r ‘ 𝑅 ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
29	20 11 16 28	syl3anc	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( .r ‘ 𝑅 ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
30	25 29	eqeltrd	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
31	9 19 30 13 13	ovmpod	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
32	14 18 31	3eqtr4rd	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( .r ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( 𝑞 ( ·𝑠 ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )