Theorem mnringnmulrdOLD

Description: Obsolete version of mnringnmulrd as of 1-Nov-2024. Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	mnringnmulrdOLD.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
	mnringnmulrdOLD.2	⊢ 𝐸 = Slot 𝑁
	mnringnmulrdOLD.3	⊢ 𝑁 ∈ ℕ
	mnringnmulrdOLD.4	⊢ 𝑁 ≠ ( .r ‘ ndx )
	mnringnmulrdOLD.5	⊢ 𝐴 = ( Base ‘ 𝑀 )
	mnringnmulrdOLD.6	⊢ 𝑉 = ( 𝑅 freeLMod 𝐴 )
	mnringnmulrdOLD.7	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
	mnringnmulrdOLD.8	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
Assertion	mnringnmulrdOLD	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑉 ) = ( 𝐸 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		mnringnmulrdOLD.1	⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2		mnringnmulrdOLD.2	⊢ 𝐸 = Slot 𝑁
3		mnringnmulrdOLD.3	⊢ 𝑁 ∈ ℕ
4		mnringnmulrdOLD.4	⊢ 𝑁 ≠ ( .r ‘ ndx )
5		mnringnmulrdOLD.5	⊢ 𝐴 = ( Base ‘ 𝑀 )
6		mnringnmulrdOLD.6	⊢ 𝑉 = ( 𝑅 freeLMod 𝐴 )
7		mnringnmulrdOLD.7	⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
8		mnringnmulrdOLD.8	⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
9	2 3	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
10	2 3	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁
11	10 4	eqnetri	⊢ ( 𝐸 ‘ ndx ) ≠ ( .r ‘ ndx )
12	9 11	setsnid	⊢ ( 𝐸 ‘ 𝑉 ) = ( 𝐸 ‘ ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑉 ) , 𝑦 ∈ ( Base ‘ 𝑉 ) ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑅 ) ) ) ) ) ) ⟩ ) )
13		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
14		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
16		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
17	1 13 14 5 15 6 16 7 8	mnringvald	⊢ ( 𝜑 → 𝐹 = ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑉 ) , 𝑦 ∈ ( Base ‘ 𝑉 ) ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑅 ) ) ) ) ) ) ⟩ ) )
18	17	fveq2d	⊢ ( 𝜑 → ( 𝐸 ‘ 𝐹 ) = ( 𝐸 ‘ ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑉 ) , 𝑦 ∈ ( Base ‘ 𝑉 ) ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑅 ) ) ) ) ) ) ⟩ ) ) )
19	12 18	eqtr4id	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑉 ) = ( 𝐸 ‘ 𝐹 ) )