ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imasival GIF version

Theorem imasival 12748
Description: Value of an image structure. The is a lemma for the theorems imasbas 12749, imasplusg 12750, and imasmulr 12751 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.)
Hypotheses
Ref Expression
imasval.u (πœ‘ β†’ π‘ˆ = (𝐹 β€œs 𝑅))
imasval.v (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘…))
imasval.p + = (+gβ€˜π‘…)
imasval.m Γ— = (.rβ€˜π‘…)
imasval.q Β· = ( ·𝑠 β€˜π‘…)
imasval.a (πœ‘ β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
imasval.t (πœ‘ β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
imasval.f (πœ‘ β†’ 𝐹:𝑉–onto→𝐡)
imasval.r (πœ‘ β†’ 𝑅 ∈ 𝑍)
Assertion
Ref Expression
imasival (πœ‘ β†’ π‘ˆ = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩})
Distinct variable groups:   𝐹,𝑝,π‘ž   𝑅,𝑝,π‘ž   𝑉,𝑝,π‘ž   πœ‘,𝑝,π‘ž
Allowed substitution hints:   𝐡(π‘ž,𝑝)   + (π‘ž,𝑝)   ✚ (π‘ž,𝑝)   βˆ™ (π‘ž,𝑝)   Β· (π‘ž,𝑝)   Γ— (π‘ž,𝑝)   π‘ˆ(π‘ž,𝑝)   𝑍(π‘ž,𝑝)

Proof of Theorem imasival
Dummy variables 𝑓 π‘Ÿ 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasval.u . 2 (πœ‘ β†’ π‘ˆ = (𝐹 β€œs 𝑅))
2 df-iimas 12744 . . . 4 β€œs = (𝑓 ∈ V, π‘Ÿ ∈ V ↦ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œ{⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩})
32a1i 9 . . 3 (πœ‘ β†’ β€œs = (𝑓 ∈ V, π‘Ÿ ∈ V ↦ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œ{⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩}))
4 basfn 12537 . . . . . 6 Base Fn V
5 vex 2754 . . . . . 6 π‘Ÿ ∈ V
6 funfvex 5546 . . . . . . 7 ((Fun Base ∧ π‘Ÿ ∈ dom Base) β†’ (Baseβ€˜π‘Ÿ) ∈ V)
76funfni 5330 . . . . . 6 ((Base Fn V ∧ π‘Ÿ ∈ V) β†’ (Baseβ€˜π‘Ÿ) ∈ V)
84, 5, 7mp2an 426 . . . . 5 (Baseβ€˜π‘Ÿ) ∈ V
98a1i 9 . . . 4 ((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) β†’ (Baseβ€˜π‘Ÿ) ∈ V)
10 simplrl 535 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑓 = 𝐹)
1110rneqd 4870 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝑓 = ran 𝐹)
12 imasval.f . . . . . . . . 9 (πœ‘ β†’ 𝐹:𝑉–onto→𝐡)
13 forn 5455 . . . . . . . . 9 (𝐹:𝑉–onto→𝐡 β†’ ran 𝐹 = 𝐡)
1412, 13syl 14 . . . . . . . 8 (πœ‘ β†’ ran 𝐹 = 𝐡)
1514ad2antrr 488 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝐹 = 𝐡)
1611, 15eqtrd 2221 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ran 𝑓 = 𝐡)
1716opeq2d 3799 . . . . 5 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(Baseβ€˜ndx), ran π‘“βŸ© = ⟨(Baseβ€˜ndx), 𝐡⟩)
18 simplrr 536 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ π‘Ÿ = 𝑅)
1918fveq2d 5533 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (Baseβ€˜π‘Ÿ) = (Baseβ€˜π‘…))
20 simpr 110 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = (Baseβ€˜π‘Ÿ))
21 imasval.v . . . . . . . . . 10 (πœ‘ β†’ 𝑉 = (Baseβ€˜π‘…))
2221ad2antrr 488 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑉 = (Baseβ€˜π‘…))
2319, 20, 223eqtr4d 2231 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ 𝑣 = 𝑉)
2410fveq1d 5531 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜π‘) = (πΉβ€˜π‘))
2510fveq1d 5531 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜π‘ž) = (πΉβ€˜π‘ž))
2624, 25opeq12d 3800 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩ = ⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩)
2718fveq2d 5533 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (+gβ€˜π‘Ÿ) = (+gβ€˜π‘…))
28 imasval.p . . . . . . . . . . . . . 14 + = (+gβ€˜π‘…)
2927, 28eqtr4di 2239 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (+gβ€˜π‘Ÿ) = + )
3029oveqd 5907 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝(+gβ€˜π‘Ÿ)π‘ž) = (𝑝 + π‘ž))
3110, 30fveq12d 5536 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž)) = (πΉβ€˜(𝑝 + π‘ž)))
3226, 31opeq12d 3800 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩ = ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩)
3332sneqd 3619 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3423, 33iuneq12d 3924 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3523, 34iuneq12d 3924 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
36 imasval.a . . . . . . . 8 (πœ‘ β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3736ad2antrr 488 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ✚ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩})
3835, 37eqtr4d 2224 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩} = ✚ )
3938opeq2d 3799 . . . . 5 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩ = ⟨(+gβ€˜ndx), ✚ ⟩)
4018fveq2d 5533 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = (.rβ€˜π‘…))
41 imasval.m . . . . . . . . . . . . . 14 Γ— = (.rβ€˜π‘…)
4240, 41eqtr4di 2239 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (.rβ€˜π‘Ÿ) = Γ— )
4342oveqd 5907 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (𝑝(.rβ€˜π‘Ÿ)π‘ž) = (𝑝 Γ— π‘ž))
4410, 43fveq12d 5536 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž)) = (πΉβ€˜(𝑝 Γ— π‘ž)))
4526, 44opeq12d 3800 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩ = ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩)
4645sneqd 3619 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4723, 46iuneq12d 3924 . . . . . . . 8 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
4823, 47iuneq12d 3924 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
49 imasval.t . . . . . . . 8 (πœ‘ β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
5049ad2antrr 488 . . . . . . 7 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆ™ = βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩})
5148, 50eqtr4d 2224 . . . . . 6 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩} = βˆ™ )
5251opeq2d 3799 . . . . 5 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩ = ⟨(.rβ€˜ndx), βˆ™ ⟩)
5317, 39, 52tpeq123d 3698 . . . 4 (((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) ∧ 𝑣 = (Baseβ€˜π‘Ÿ)) β†’ {⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩})
549, 53csbied 3117 . . 3 ((πœ‘ ∧ (𝑓 = 𝐹 ∧ π‘Ÿ = 𝑅)) β†’ ⦋(Baseβ€˜π‘Ÿ) / π‘£β¦Œ{⟨(Baseβ€˜ndx), ran π‘“βŸ©, ⟨(+gβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(+gβ€˜π‘Ÿ)π‘ž))⟩}⟩, ⟨(.rβ€˜ndx), βˆͺ 𝑝 ∈ 𝑣 βˆͺ π‘ž ∈ 𝑣 {⟨⟨(π‘“β€˜π‘), (π‘“β€˜π‘ž)⟩, (π‘“β€˜(𝑝(.rβ€˜π‘Ÿ)π‘ž))⟩}⟩} = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩})
55 fof 5452 . . . . 5 (𝐹:𝑉–onto→𝐡 β†’ 𝐹:π‘‰βŸΆπ΅)
5612, 55syl 14 . . . 4 (πœ‘ β†’ 𝐹:π‘‰βŸΆπ΅)
57 imasval.r . . . . . . 7 (πœ‘ β†’ 𝑅 ∈ 𝑍)
5857elexd 2764 . . . . . 6 (πœ‘ β†’ 𝑅 ∈ V)
59 funfvex 5546 . . . . . . 7 ((Fun Base ∧ 𝑅 ∈ dom Base) β†’ (Baseβ€˜π‘…) ∈ V)
6059funfni 5330 . . . . . 6 ((Base Fn V ∧ 𝑅 ∈ V) β†’ (Baseβ€˜π‘…) ∈ V)
614, 58, 60sylancr 414 . . . . 5 (πœ‘ β†’ (Baseβ€˜π‘…) ∈ V)
6221, 61eqeltrd 2265 . . . 4 (πœ‘ β†’ 𝑉 ∈ V)
6356, 62fexd 5761 . . 3 (πœ‘ β†’ 𝐹 ∈ V)
64 basendxnn 12535 . . . . 5 (Baseβ€˜ndx) ∈ β„•
65 focdmex 6133 . . . . . 6 (𝑉 ∈ V β†’ (𝐹:𝑉–onto→𝐡 β†’ 𝐡 ∈ V))
6662, 12, 65sylc 62 . . . . 5 (πœ‘ β†’ 𝐡 ∈ V)
67 opexg 4242 . . . . 5 (((Baseβ€˜ndx) ∈ β„• ∧ 𝐡 ∈ V) β†’ ⟨(Baseβ€˜ndx), 𝐡⟩ ∈ V)
6864, 66, 67sylancr 414 . . . 4 (πœ‘ β†’ ⟨(Baseβ€˜ndx), 𝐡⟩ ∈ V)
69 plusgndxnn 12588 . . . . 5 (+gβ€˜ndx) ∈ β„•
7063ad2antrr 488 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ 𝐹 ∈ V)
71 vex 2754 . . . . . . . . . . . . . . 15 𝑝 ∈ V
7271a1i 9 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ 𝑝 ∈ V)
73 fvexg 5548 . . . . . . . . . . . . . 14 ((𝐹 ∈ V ∧ 𝑝 ∈ V) β†’ (πΉβ€˜π‘) ∈ V)
7470, 72, 73syl2anc 411 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ (πΉβ€˜π‘) ∈ V)
75 vex 2754 . . . . . . . . . . . . . . 15 π‘ž ∈ V
7675a1i 9 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ π‘ž ∈ V)
77 fvexg 5548 . . . . . . . . . . . . . 14 ((𝐹 ∈ V ∧ π‘ž ∈ V) β†’ (πΉβ€˜π‘ž) ∈ V)
7870, 76, 77syl2anc 411 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ (πΉβ€˜π‘ž) ∈ V)
79 opexg 4242 . . . . . . . . . . . . 13 (((πΉβ€˜π‘) ∈ V ∧ (πΉβ€˜π‘ž) ∈ V) β†’ ⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩ ∈ V)
8074, 78, 79syl2anc 411 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ ⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩ ∈ V)
81 plusgslid 12589 . . . . . . . . . . . . . . . . . 18 (+g = Slot (+gβ€˜ndx) ∧ (+gβ€˜ndx) ∈ β„•)
8281slotex 12506 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ 𝑍 β†’ (+gβ€˜π‘…) ∈ V)
8357, 82syl 14 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (+gβ€˜π‘…) ∈ V)
8428, 83eqeltrid 2275 . . . . . . . . . . . . . . 15 (πœ‘ β†’ + ∈ V)
8584ad2antrr 488 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ + ∈ V)
86 ovexg 5924 . . . . . . . . . . . . . 14 ((𝑝 ∈ V ∧ + ∈ V ∧ π‘ž ∈ V) β†’ (𝑝 + π‘ž) ∈ V)
8772, 85, 76, 86syl3anc 1248 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ (𝑝 + π‘ž) ∈ V)
88 fvexg 5548 . . . . . . . . . . . . 13 ((𝐹 ∈ V ∧ (𝑝 + π‘ž) ∈ V) β†’ (πΉβ€˜(𝑝 + π‘ž)) ∈ V)
8970, 87, 88syl2anc 411 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ (πΉβ€˜(𝑝 + π‘ž)) ∈ V)
90 opexg 4242 . . . . . . . . . . . 12 ((⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩ ∈ V ∧ (πΉβ€˜(𝑝 + π‘ž)) ∈ V) β†’ ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩ ∈ V)
9180, 89, 90syl2anc 411 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩ ∈ V)
92 snexg 4198 . . . . . . . . . . 11 (⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩ ∈ V β†’ {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V)
9391, 92syl 14 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V)
9493ralrimiva 2562 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ 𝑉) β†’ βˆ€π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V)
95 iunexg 6137 . . . . . . . . 9 ((𝑉 ∈ V ∧ βˆ€π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V) β†’ βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V)
9662, 94, 95syl2an2r 595 . . . . . . . 8 ((πœ‘ ∧ 𝑝 ∈ 𝑉) β†’ βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V)
9796ralrimiva 2562 . . . . . . 7 (πœ‘ β†’ βˆ€π‘ ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V)
98 iunexg 6137 . . . . . . 7 ((𝑉 ∈ V ∧ βˆ€π‘ ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V) β†’ βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V)
9962, 97, 98syl2anc 411 . . . . . 6 (πœ‘ β†’ βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 + π‘ž))⟩} ∈ V)
10036, 99eqeltrd 2265 . . . . 5 (πœ‘ β†’ ✚ ∈ V)
101 opexg 4242 . . . . 5 (((+gβ€˜ndx) ∈ β„• ∧ ✚ ∈ V) β†’ ⟨(+gβ€˜ndx), ✚ ⟩ ∈ V)
10269, 100, 101sylancr 414 . . . 4 (πœ‘ β†’ ⟨(+gβ€˜ndx), ✚ ⟩ ∈ V)
103 mulrslid 12608 . . . . . 6 (.r = Slot (.rβ€˜ndx) ∧ (.rβ€˜ndx) ∈ β„•)
104103simpri 113 . . . . 5 (.rβ€˜ndx) ∈ β„•
105103slotex 12506 . . . . . . . . . . . . . . . . 17 (𝑅 ∈ 𝑍 β†’ (.rβ€˜π‘…) ∈ V)
10657, 105syl 14 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (.rβ€˜π‘…) ∈ V)
10741, 106eqeltrid 2275 . . . . . . . . . . . . . . 15 (πœ‘ β†’ Γ— ∈ V)
108107ad2antrr 488 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ Γ— ∈ V)
109 ovexg 5924 . . . . . . . . . . . . . 14 ((𝑝 ∈ V ∧ Γ— ∈ V ∧ π‘ž ∈ V) β†’ (𝑝 Γ— π‘ž) ∈ V)
11072, 108, 76, 109syl3anc 1248 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ (𝑝 Γ— π‘ž) ∈ V)
111 fvexg 5548 . . . . . . . . . . . . 13 ((𝐹 ∈ V ∧ (𝑝 Γ— π‘ž) ∈ V) β†’ (πΉβ€˜(𝑝 Γ— π‘ž)) ∈ V)
11270, 110, 111syl2anc 411 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ (πΉβ€˜(𝑝 Γ— π‘ž)) ∈ V)
113 opexg 4242 . . . . . . . . . . . 12 ((⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩ ∈ V ∧ (πΉβ€˜(𝑝 Γ— π‘ž)) ∈ V) β†’ ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩ ∈ V)
11480, 112, 113syl2anc 411 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ ⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩ ∈ V)
115 snexg 4198 . . . . . . . . . . 11 (⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩ ∈ V β†’ {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V)
116114, 115syl 14 . . . . . . . . . 10 (((πœ‘ ∧ 𝑝 ∈ 𝑉) ∧ π‘ž ∈ 𝑉) β†’ {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V)
117116ralrimiva 2562 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ 𝑉) β†’ βˆ€π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V)
118 iunexg 6137 . . . . . . . . 9 ((𝑉 ∈ V ∧ βˆ€π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V) β†’ βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V)
11962, 117, 118syl2an2r 595 . . . . . . . 8 ((πœ‘ ∧ 𝑝 ∈ 𝑉) β†’ βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V)
120119ralrimiva 2562 . . . . . . 7 (πœ‘ β†’ βˆ€π‘ ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V)
121 iunexg 6137 . . . . . . 7 ((𝑉 ∈ V ∧ βˆ€π‘ ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V) β†’ βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V)
12262, 120, 121syl2anc 411 . . . . . 6 (πœ‘ β†’ βˆͺ 𝑝 ∈ 𝑉 βˆͺ π‘ž ∈ 𝑉 {⟨⟨(πΉβ€˜π‘), (πΉβ€˜π‘ž)⟩, (πΉβ€˜(𝑝 Γ— π‘ž))⟩} ∈ V)
12349, 122eqeltrd 2265 . . . . 5 (πœ‘ β†’ βˆ™ ∈ V)
124 opexg 4242 . . . . 5 (((.rβ€˜ndx) ∈ β„• ∧ βˆ™ ∈ V) β†’ ⟨(.rβ€˜ndx), βˆ™ ⟩ ∈ V)
125104, 123, 124sylancr 414 . . . 4 (πœ‘ β†’ ⟨(.rβ€˜ndx), βˆ™ ⟩ ∈ V)
126 tpexg 4458 . . . 4 ((⟨(Baseβ€˜ndx), 𝐡⟩ ∈ V ∧ ⟨(+gβ€˜ndx), ✚ ⟩ ∈ V ∧ ⟨(.rβ€˜ndx), βˆ™ ⟩ ∈ V) β†’ {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} ∈ V)
12768, 102, 125, 126syl3anc 1248 . . 3 (πœ‘ β†’ {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩} ∈ V)
1283, 54, 63, 58, 127ovmpod 6018 . 2 (πœ‘ β†’ (𝐹 β€œs 𝑅) = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩})
1291, 128eqtrd 2221 1 (πœ‘ β†’ π‘ˆ = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(+gβ€˜ndx), ✚ ⟩, ⟨(.rβ€˜ndx), βˆ™ ⟩})
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   = wceq 1363   ∈ wcel 2159  βˆ€wral 2467  Vcvv 2751  β¦‹csb 3071  {csn 3606  {ctp 3608  βŸ¨cop 3609  βˆͺ ciun 3900  ran crn 4641   Fn wfn 5225  βŸΆwf 5226  β€“ontoβ†’wfo 5228  β€˜cfv 5230  (class class class)co 5890   ∈ cmpo 5892  β„•cn 8936  ndxcnx 12476  Slot cslot 12478  Basecbs 12479  +gcplusg 12554  .rcmulr 12555   ·𝑠 cvsca 12558   β€œs cimas 12741
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-coll 4132  ax-sep 4135  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-setind 4550  ax-cnex 7919  ax-resscn 7920  ax-1re 7922  ax-addrcl 7925
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-ral 2472  df-rex 2473  df-reu 2474  df-rab 2476  df-v 2753  df-sbc 2977  df-csb 3072  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-pw 3591  df-sn 3612  df-pr 3613  df-tp 3614  df-op 3615  df-uni 3824  df-int 3859  df-iun 3902  df-br 4018  df-opab 4079  df-mpt 4080  df-id 4307  df-xp 4646  df-rel 4647  df-cnv 4648  df-co 4649  df-dm 4650  df-rn 4651  df-res 4652  df-ima 4653  df-iota 5192  df-fun 5232  df-fn 5233  df-f 5234  df-f1 5235  df-fo 5236  df-f1o 5237  df-fv 5238  df-ov 5893  df-oprab 5894  df-mpo 5895  df-inn 8937  df-2 8995  df-3 8996  df-ndx 12482  df-slot 12483  df-base 12485  df-plusg 12567  df-mulr 12568  df-iimas 12744
This theorem is referenced by:  imasbas  12749  imasplusg  12750  imasmulr  12751
  Copyright terms: Public domain W3C validator