Metamath Proof Explorer

Theorem mnringvald

Description: Value of the monoid ring function. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses mnringvald.1 ⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
mnringvald.2 ⊢ · = ( .r ‘ 𝑅 )
mnringvald.3 ⊢ 0 = ( 0g ‘ 𝑅 )
mnringvald.4 ⊢ 𝐴 = ( Base ‘ 𝑀 )
mnringvald.5 ⊢ + = ( +g ‘ 𝑀 )
mnringvald.6 ⊢ 𝑉 = ( 𝑅 freeLMod 𝐴 )
mnringvald.7 ⊢ 𝐵 = ( Base ‘ 𝑉 )
mnringvald.8 ⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
mnringvald.9 ⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
Assertion mnringvald ( 𝜑 → 𝐹 = ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )

Proof

Step Hyp Ref Expression
1 mnringvald.1 ⊢ 𝐹 = ( 𝑅 MndRing 𝑀 )
2 mnringvald.2 ⊢ · = ( .r ‘ 𝑅 )
3 mnringvald.3 ⊢ 0 = ( 0g ‘ 𝑅 )
4 mnringvald.4 ⊢ 𝐴 = ( Base ‘ 𝑀 )
5 mnringvald.5 ⊢ + = ( +g ‘ 𝑀 )
6 mnringvald.6 ⊢ 𝑉 = ( 𝑅 freeLMod 𝐴 )
7 mnringvald.7 ⊢ 𝐵 = ( Base ‘ 𝑉 )
8 mnringvald.8 ⊢ ( 𝜑 → 𝑅 ∈ 𝑈 )
9 mnringvald.9 ⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
10 8 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
11 9 elexd ⊢ ( 𝜑 → 𝑀 ∈ V )
12 nfv ⊢ Ⅎ 𝑣 ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 )
13 nfcvd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) → Ⅎ 𝑣 ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )
14 ovexd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) → ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ∈ V )
15 simpr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) )
16 simpll ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → 𝑟 = 𝑅 )
17 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
18 17 4 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐴 )
19 18 ad2antlr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( Base ‘ 𝑚 ) = 𝐴 )
20 16 19 oveq12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) = ( 𝑅 freeLMod 𝐴 ) )
21 15 20 eqtrd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → 𝑣 = ( 𝑅 freeLMod 𝐴 ) )
22 21 6 eqtr4di ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → 𝑣 = 𝑉 )
23 22 fveq2d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( Base ‘ 𝑣 ) = ( Base ‘ 𝑉 ) )
24 23 7 eqtr4di ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( Base ‘ 𝑣 ) = 𝐵 )
25 fveq2 ⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
26 25 5 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = + )
27 26 oveqd ⊢ ( 𝑚 = 𝑀 → ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) = ( 𝑎 + 𝑏 ) )
28 27 ad2antlr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) = ( 𝑎 + 𝑏 ) )
29 28 eqeq2d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) ↔ 𝑖 = ( 𝑎 + 𝑏 ) ) )
30 fveq2 ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
31 30 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
32 31 oveqd ⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) = ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) )
33 32 ad2antrr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) = ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) )
34 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
35 34 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
36 35 ad2antrr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 0g ‘ 𝑟 ) = 0 )
37 29 33 36 ifbieq12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) = if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) )
38 19 37 mpteq12dv ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) = ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) )
39 19 19 38 mpoeq123dv ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 𝑎 ∈ ( Base ‘ 𝑚 ) , 𝑏 ∈ ( Base ‘ 𝑚 ) ↦ ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) ) = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) )
40 22 39 oveq12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 𝑣 Σg ( 𝑎 ∈ ( Base ‘ 𝑚 ) , 𝑏 ∈ ( Base ‘ 𝑚 ) ↦ ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) = ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) )
41 24 24 40 mpoeq123dv ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝑣 ) , 𝑦 ∈ ( Base ‘ 𝑣 ) ↦ ( 𝑣 Σg ( 𝑎 ∈ ( Base ‘ 𝑚 ) , 𝑏 ∈ ( Base ‘ 𝑚 ) ↦ ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) )
42 41 opeq2d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑣 ) , 𝑦 ∈ ( Base ‘ 𝑣 ) ↦ ( 𝑣 Σg ( 𝑎 ∈ ( Base ‘ 𝑚 ) , 𝑏 ∈ ( Base ‘ 𝑚 ) ↦ ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) ) ⟩ = ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ )
43 22 42 oveq12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) ∧ 𝑣 = ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) ) → ( 𝑣 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑣 ) , 𝑦 ∈ ( Base ‘ 𝑣 ) ↦ ( 𝑣 Σg ( 𝑎 ∈ ( Base ‘ 𝑚 ) , 𝑏 ∈ ( Base ‘ 𝑚 ) ↦ ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) ) ⟩ ) = ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )
44 12 13 14 43 csbiedf ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑚 = 𝑀 ) → ⦋ ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) / 𝑣 ⦌ ( 𝑣 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑣 ) , 𝑦 ∈ ( Base ‘ 𝑣 ) ↦ ( 𝑣 Σg ( 𝑎 ∈ ( Base ‘ 𝑚 ) , 𝑏 ∈ ( Base ‘ 𝑚 ) ↦ ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) ) ⟩ ) = ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )
45 df-mnring ⊢ MndRing = ( 𝑟 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 𝑟 freeLMod ( Base ‘ 𝑚 ) ) / 𝑣 ⦌ ( 𝑣 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑣 ) , 𝑦 ∈ ( Base ‘ 𝑣 ) ↦ ( 𝑣 Σg ( 𝑎 ∈ ( Base ‘ 𝑚 ) , 𝑏 ∈ ( Base ‘ 𝑚 ) ↦ ( 𝑖 ∈ ( Base ‘ 𝑚 ) ↦ if ( 𝑖 = ( 𝑎 ( +g ‘ 𝑚 ) 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) ( .r ‘ 𝑟 ) ( 𝑦 ‘ 𝑏 ) ) , ( 0g ‘ 𝑟 ) ) ) ) ) ) ⟩ ) )
46 ovex ⊢ ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) ∈ V
47 44 45 46 ovmpoa ⊢ ( ( 𝑅 ∈ V ∧ 𝑀 ∈ V ) → ( 𝑅 MndRing 𝑀 ) = ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )
48 10 11 47 syl2anc ⊢ ( 𝜑 → ( 𝑅 MndRing 𝑀 ) = ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )
49 1 48 syl5eq ⊢ ( 𝜑 → 𝐹 = ( 𝑉 sSet ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑉 Σg ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐴 ↦ ( 𝑖 ∈ 𝐴 ↦ if ( 𝑖 = ( 𝑎 + 𝑏 ) , ( ( 𝑥 ‘ 𝑎 ) · ( 𝑦 ‘ 𝑏 ) ) , 0 ) ) ) ) ) ⟩ ) )