Metamath Proof Explorer

Theorem lmod1lem3

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

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

Proof

Step Hyp Ref Expression
1 lmod1.m ⊢ 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ⟩ } )
2 eqidd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) )
3 simprr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 )
4 simplr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
5 1 lmodsca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑀 ) )
6 5 fveq2d ⊢ ( 𝑅 ∈ Ring → ( +g ‘ 𝑅 ) = ( +g ‘ ( Scalar ‘ 𝑀 ) ) )
7 4 6 syl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( Scalar ‘ 𝑀 ) ) )
8 7 eqcomd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( +g ‘ ( Scalar ‘ 𝑀 ) ) = ( +g ‘ 𝑅 ) )
9 8 oveqd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) = ( 𝑞 ( +g ‘ 𝑅 ) 𝑟 ) )
10 simprl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑞 ∈ ( Base ‘ 𝑅 ) )
11 simprr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑟 ∈ ( Base ‘ 𝑅 ) )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14 12 13 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑞 ( +g ‘ 𝑅 ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
15 4 10 11 14 syl3anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( +g ‘ 𝑅 ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
16 9 15 eqeltrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
17 snidg ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } )
18 17 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝐼 ∈ { 𝐼 } )
19 18 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝐼 ∈ { 𝐼 } )
20 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝐼 ∈ 𝑉 )
21 20 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → 𝐼 ∈ 𝑉 )
22 2 3 16 19 21 ovmpod ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) 𝐼 ) = 𝐼 )
23 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
24 snex ⊢ { 𝐼 } ∈ V
25 23 24 pm3.2i ⊢ ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V )
26 mpoexga ⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ { 𝐼 } ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V )
27 25 26 mp1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V )
28 1 lmodvsca ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) ∈ V → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
29 27 28 syl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) = ( ·𝑠 ‘ 𝑀 ) )
30 29 eqcomd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ·𝑠 ‘ 𝑀 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) )
31 30 oveqd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ { 𝐼 } ↦ 𝑦 ) 𝐼 ) )
32 simprr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = 𝑞 ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 )
33 30 32 10 19 19 ovmpod ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
34 simprr ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) ∧ ( 𝑥 = 𝑟 ∧ 𝑦 = 𝐼 ) ) → 𝑦 = 𝐼 )
35 30 34 11 19 19 ovmpod ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = 𝐼 )
36 33 35 oveq12d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) = ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) )
37 snex ⊢ { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V
38 1 lmodplusg ⊢ ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ∈ V → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
39 37 38 mp1i ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } = ( +g ‘ 𝑀 ) )
40 39 eqcomd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( +g ‘ 𝑀 ) = { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } )
41 40 oveqd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝐼 ) = ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) )
42 df-ov ⊢ ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ )
43 opex ⊢ ⟨ 𝐼 , 𝐼 ⟩ ∈ V
44 20 43 jctil ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) )
45 44 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) )
46 fvsng ⊢ ( ( ⟨ 𝐼 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
47 45 46 syl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ‘ ⟨ 𝐼 , 𝐼 ⟩ ) = 𝐼 )
48 42 47 syl5eq ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝐼 { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } 𝐼 ) = 𝐼 )
49 36 41 48 3eqtrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) = 𝐼 )
50 22 31 49 3eqtr4d ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑞 ( +g ‘ ( Scalar ‘ 𝑀 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑀 ) 𝐼 ) = ( ( 𝑞 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ( +g ‘ 𝑀 ) ( 𝑟 ( ·𝑠 ‘ 𝑀 ) 𝐼 ) ) )