Metamath Proof Explorer

Theorem ixpsnbasval

Description: The value of an infinite Cartesian product of the base of a left module over a ring with a singleton. (Contributed by AV, 3-Dec-2018)

Ref Expression
Assertion ixpsnbasval ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → X 𝑥 ∈ { 𝑋 } ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) } )

Proof

Step Hyp Ref Expression
1 ixpsnval ⊢ ( 𝑋 ∈ 𝑊 → X 𝑥 ∈ { 𝑋 } ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) ) } )
2 1 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → X 𝑥 ∈ { 𝑋 } ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) ) } )
3 csbfv2g ⊢ ( 𝑋 ∈ 𝑊 → ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = ( Base ‘ ⦋ 𝑋 / 𝑥 ⦌ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) )
4 csbfv2g ⊢ ( 𝑋 ∈ 𝑊 → ⦋ 𝑋 / 𝑥 ⦌ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) = ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ ⦋ 𝑋 / 𝑥 ⦌ 𝑥 ) )
5 csbvarg ⊢ ( 𝑋 ∈ 𝑊 → ⦋ 𝑋 / 𝑥 ⦌ 𝑥 = 𝑋 )
6 5 fveq2d ⊢ ( 𝑋 ∈ 𝑊 → ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ ⦋ 𝑋 / 𝑥 ⦌ 𝑥 ) = ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑋 ) )
7 4 6 eqtrd ⊢ ( 𝑋 ∈ 𝑊 → ⦋ 𝑋 / 𝑥 ⦌ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) = ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑋 ) )
8 7 fveq2d ⊢ ( 𝑋 ∈ 𝑊 → ( Base ‘ ⦋ 𝑋 / 𝑥 ⦌ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑋 ) ) )
9 3 8 eqtrd ⊢ ( 𝑋 ∈ 𝑊 → ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑋 ) ) )
10 9 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑋 ) ) )
11 fvexd ⊢ ( 𝑅 ∈ 𝑉 → ( ringLMod ‘ 𝑅 ) ∈ V )
12 11 anim1ci ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( 𝑋 ∈ 𝑊 ∧ ( ringLMod ‘ 𝑅 ) ∈ V ) )
13 xpsng ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( ringLMod ‘ 𝑅 ) ∈ V ) → ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) = { ⟨ 𝑋 , ( ringLMod ‘ 𝑅 ) ⟩ } )
14 12 13 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) = { ⟨ 𝑋 , ( ringLMod ‘ 𝑅 ) ⟩ } )
15 14 fveq1d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑋 ) = ( { ⟨ 𝑋 , ( ringLMod ‘ 𝑅 ) ⟩ } ‘ 𝑋 ) )
16 fvsng ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( ringLMod ‘ 𝑅 ) ∈ V ) → ( { ⟨ 𝑋 , ( ringLMod ‘ 𝑅 ) ⟩ } ‘ 𝑋 ) = ( ringLMod ‘ 𝑅 ) )
17 12 16 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( { ⟨ 𝑋 , ( ringLMod ‘ 𝑅 ) ⟩ } ‘ 𝑋 ) = ( ringLMod ‘ 𝑅 ) )
18 15 17 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑋 ) = ( ringLMod ‘ 𝑅 ) )
19 18 fveq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑋 ) ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
20 10 19 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
21 rlmbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
22 20 21 eqtr4di ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = ( Base ‘ 𝑅 ) )
23 22 eleq2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) ↔ ( 𝑓 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) )
24 23 anbi2d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → ( ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) ) ↔ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) ) )
25 24 abbidv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑥 ⦌ ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) ) } = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) } )
26 2 25 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ) → X 𝑥 ∈ { 𝑋 } ( Base ‘ ( ( { 𝑋 } × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑥 ) ) = { 𝑓 ∣ ( 𝑓 Fn { 𝑋 } ∧ ( 𝑓 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) } )