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	⊢ ( 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ → ( 2^nd ‘ 𝑝 ) = ( 2^nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) )
5	4	adantl	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ ) → ( 2^nd ‘ 𝑝 ) = ( 2^nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) )
6		op2ndg	⊢ ( ( 𝑍 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉 ) → ( 2^nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) = 𝐼 )
7	6	ancoms	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 2^nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) = 𝐼 )
8		snidg	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ { 𝐼 } )
9	8	adantr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐼 ∈ { 𝐼 } )
10	7 9	eqeltrd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 2^nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) ∈ { 𝐼 } )
11	10	adantr	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ ) → ( 2^nd ‘ ⟨ 𝑍 , 𝐼 ⟩ ) ∈ { 𝐼 } )
12	5 11	eqeltrd	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑝 = ⟨ 𝑍 , 𝐼 ⟩ ) → ( 2^nd ‘ 𝑝 ) ∈ { 𝐼 } )
13	3 12	sylan2	⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ) → ( 2^nd ‘ 𝑝 ) ∈ { 𝐼 } )
14	13	fmpttd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2^nd ‘ 𝑝 ) ) : { ⟨ 𝑍 , 𝐼 ⟩ } ⟶ { 𝐼 } )
15		opex	⊢ ⟨ 𝑍 , 𝐼 ⟩ ∈ V
16		simpl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐼 ∈ 𝑉 )
17		fsng	⊢ ( ( ⟨ 𝑍 , 𝐼 ⟩ ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2^nd ‘ 𝑝 ) ) : { ⟨ 𝑍 , 𝐼 ⟩ } ⟶ { 𝐼 } ↔ ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2^nd ‘ 𝑝 ) ) = { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ) )
18	15 16 17	sylancr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2^nd ‘ 𝑝 ) ) : { ⟨ 𝑍 , 𝐼 ⟩ } ⟶ { 𝐼 } ↔ ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2^nd ‘ 𝑝 ) ) = { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } ) )
19	14 18	mpbid	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2^nd ‘ 𝑝 ) ) = { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } )
20		xpsng	⊢ ( ( 𝑍 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉 ) → ( { 𝑍 } × { 𝐼 } ) = { ⟨ 𝑍 , 𝐼 ⟩ } )
21	20	ancoms	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( { 𝑍 } × { 𝐼 } ) = { ⟨ 𝑍 , 𝐼 ⟩ } )
22	21	eqcomd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { ⟨ 𝑍 , 𝐼 ⟩ } = ( { 𝑍 } × { 𝐼 } ) )
23	22	mpteq1d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑝 ∈ { ⟨ 𝑍 , 𝐼 ⟩ } ↦ ( 2^nd ‘ 𝑝 ) ) = ( 𝑝 ∈ ( { 𝑍 } × { 𝐼 } ) ↦ ( 2^nd ‘ 𝑝 ) ) )
24	19 23	eqtr3d	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { ⟨ ⟨ 𝑍 , 𝐼 ⟩ , 𝐼 ⟩ } = ( 𝑝 ∈ ( { 𝑍 } × { 𝐼 } ) ↦ ( 2^nd ‘ 𝑝 ) ) )
25		vex	⊢ 𝑧 ∈ V
26		vex	⊢ 𝑖 ∈ V
27	25 26	op2ndd	⊢ ( 𝑝 = ⟨ 𝑧 , 𝑖 ⟩ → ( 2^nd ‘ 𝑝 ) = 𝑖 )
28	27	mpompt	⊢ ( 𝑝 ∈ ( { 𝑍 } × { 𝐼 } ) ↦ ( 2^nd ‘ 𝑝 ) ) = ( 𝑧 ∈ { 𝑍 } , 𝑖 ∈ { 𝐼 } ↦ 𝑖 )
29	28	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑝 ∈ ( { 𝑍 } × { 𝐼 } ) ↦ ( 2^nd ‘ 𝑝 ) ) = ( 𝑧 ∈ { 𝑍 } , 𝑖 ∈ { 𝐼 } ↦ 𝑖 ) )
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	syl5eq	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑀 = ( { ⟨ ( 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 )

Metamath Proof Explorer

Theorem lmod1zr

Proof