Metamath Proof Explorer


Theorem lmod1zr

Description: The (smallest) structure representing azero module over a zero ring. (Contributed by AV, 29-Apr-2019)

Ref Expression
Hypotheses lmod1zr.r 𝑅 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
lmod1zr.m 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } )
Assertion lmod1zr ( ( 𝐼𝑉𝑍𝑊 ) → 𝑀 ∈ LMod )

Proof

Step Hyp Ref Expression
1 lmod1zr.r 𝑅 = { ⟨ ( Base ‘ ndx ) , { 𝑍 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ⟩ }
2 lmod1zr.m 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } )
3 elsni ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } → 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ )
4 fveq2 ( 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ → ( 2nd𝑝 ) = ( 2nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) )
5 4 adantl ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ ) → ( 2nd𝑝 ) = ( 2nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) )
6 op2ndg ( ( 𝑍𝑊𝐼𝑉 ) → ( 2nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) = 𝐼 )
7 6 ancoms ( ( 𝐼𝑉𝑍𝑊 ) → ( 2nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) = 𝐼 )
8 snidg ( 𝐼𝑉𝐼 ∈ { 𝐼 } )
9 8 adantr ( ( 𝐼𝑉𝑍𝑊 ) → 𝐼 ∈ { 𝐼 } )
10 7 9 eqeltrd ( ( 𝐼𝑉𝑍𝑊 ) → ( 2nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) ∈ { 𝐼 } )
11 10 adantr ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ ) → ( 2nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) ∈ { 𝐼 } )
12 5 11 eqeltrd ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ ) → ( 2nd𝑝 ) ∈ { 𝐼 } )
13 3 12 sylan2 ( ( ( 𝐼𝑉𝑍𝑊 ) ∧ 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ) → ( 2nd𝑝 ) ∈ { 𝐼 } )
14 13 fmpttd ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2nd𝑝 ) ) : { ⟨ 𝑍 , 𝐼 ⟩ } ⟶ { 𝐼 } )
15 opex 𝑍 , 𝐼 ⟩ ∈ V
16 simpl ( ( 𝐼𝑉𝑍𝑊 ) → 𝐼𝑉 )
17 fsng ( ( ⟨ 𝑍 , 𝐼 ⟩ ∈ V ∧ 𝐼𝑉 ) → ( ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2nd𝑝 ) ) : { ⟨ 𝑍 , 𝐼 ⟩ } ⟶ { 𝐼 } ↔ ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2nd𝑝 ) ) = { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ) )
18 15 16 17 sylancr ( ( 𝐼𝑉𝑍𝑊 ) → ( ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2nd𝑝 ) ) : { ⟨ 𝑍 , 𝐼 ⟩ } ⟶ { 𝐼 } ↔ ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2nd𝑝 ) ) = { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ) )
19 14 18 mpbid ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2nd𝑝 ) ) = { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } )
20 xpsng ( ( 𝑍𝑊𝐼𝑉 ) → ( { 𝑍 } × { 𝐼 } ) = { ⟨ 𝑍 , 𝐼 ⟩ } )
21 20 ancoms ( ( 𝐼𝑉𝑍𝑊 ) → ( { 𝑍 } × { 𝐼 } ) = { ⟨ 𝑍 , 𝐼 ⟩ } )
22 21 eqcomd ( ( 𝐼𝑉𝑍𝑊 ) → { ⟨ 𝑍 , 𝐼 ⟩ } = ( { 𝑍 } × { 𝐼 } ) )
23 22 mpteq1d ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2nd𝑝 ) ) = ( 𝑝 ∈ ( { 𝑍 } × { 𝐼 } ) ↦ ( 2nd𝑝 ) ) )
24 19 23 eqtr3d ( ( 𝐼𝑉𝑍𝑊 ) → { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } = ( 𝑝 ∈ ( { 𝑍 } × { 𝐼 } ) ↦ ( 2nd𝑝 ) ) )
25 vex 𝑧 ∈ V
26 vex 𝑖 ∈ V
27 25 26 op2ndd ( 𝑝 = ⟨ 𝑧 , 𝑖 ⟩ → ( 2nd𝑝 ) = 𝑖 )
28 27 mpompt ( 𝑝 ∈ ( { 𝑍 } × { 𝐼 } ) ↦ ( 2nd𝑝 ) ) = ( 𝑧 ∈ { 𝑍 } , 𝑖 ∈ { 𝐼 } ↦ 𝑖 )
29 28 a1i ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝑝 ∈ ( { 𝑍 } × { 𝐼 } ) ↦ ( 2nd𝑝 ) ) = ( 𝑧 ∈ { 𝑍 } , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) )
30 snex { 𝑍 } ∈ V
31 1 rngbase ( { 𝑍 } ∈ V → { 𝑍 } = ( Base ‘ 𝑅 ) )
32 30 31 mp1i ( ( 𝐼𝑉𝑍𝑊 ) → { 𝑍 } = ( Base ‘ 𝑅 ) )
33 eqidd ( ( 𝐼𝑉𝑍𝑊 ) → { 𝐼 } = { 𝐼 } )
34 mpoeq12 ( ( { 𝑍 } = ( Base ‘ 𝑅 ) ∧ { 𝐼 } = { 𝐼 } ) → ( 𝑧 ∈ { 𝑍 } , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) = ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) )
35 32 33 34 syl2anc ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝑧 ∈ { 𝑍 } , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) = ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) )
36 24 29 35 3eqtrd ( ( 𝐼𝑉𝑍𝑊 ) → { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } = ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) )
37 36 opeq2d ( ( 𝐼𝑉𝑍𝑊 ) → ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ )
38 37 sneqd ( ( 𝐼𝑉𝑍𝑊 ) → { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } = { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ } )
39 38 uneq2d ( ( 𝐼𝑉𝑍𝑊 ) → ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ } ) )
40 2 39 eqtrid ( ( 𝐼𝑉𝑍𝑊 ) → 𝑀 = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ } ) )
41 1 ring1 ( 𝑍𝑊𝑅 ∈ Ring )
42 eqidd ( 𝑧 = 𝑎𝑖 = 𝑖 )
43 id ( 𝑖 = 𝑏𝑖 = 𝑏 )
44 42 43 cbvmpov ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) = ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ { 𝐼 } ↦ 𝑏 )
45 44 opeq2i ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ = ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ { 𝐼 } ↦ 𝑏 ) ⟩
46 45 sneqi { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ } = { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ { 𝐼 } ↦ 𝑏 ) ⟩ }
47 46 uneq2i ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ { 𝐼 } ↦ 𝑏 ) ⟩ } )
48 47 lmod1 ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ } ) ∈ LMod )
49 41 48 sylan2 ( ( 𝐼𝑉𝑍𝑊 ) → ( { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ , ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑧 ∈ ( Base ‘ 𝑅 ) , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) ⟩ } ) ∈ LMod )
50 40 49 eqeltrd ( ( 𝐼𝑉𝑍𝑊 ) → 𝑀 ∈ LMod )