ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imasival Unicode version
Theorem imasival 13570
Description: Value of an image structure. The is a lemma for the theorems imasbas 13571, imasplusg 13572, and imasmulr 13573 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 |- ( ph -> U = ( F "s R ) )
imasval.v |- ( ph -> V = ( Base ` R ) )
imasval.p |- .+ = ( +g ` R )
imasval.m |- .X. = ( .r ` R )
imasval.q |- .x. = ( .s ` R )
imasval.a |- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
imasval.t |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
imasval.f |- ( ph -> F : V -onto-> B )
imasval.r |- ( ph -> R e. Z )
Assertion
Ref Expression
imasival |- ( ph -> U = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
Distinct variable groups:   F, p, q   R, p, q   V, p, q   ph, p, q
Allowed substitution hints:   B( q, p)   .+ ( q, p)   .+b ( q, p)   .xb ( q, p)   .x. ( q, p)   .X. ( q, p)   U( q, p)   Z( q, p)
Proof of Theorem imasival
Dummy variables f r v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasval.u . 2 |- ( ph -> U = ( F "s R ) )
2 df-iimas 13567 . . . 4 |- "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } )
32a1i 9 . . 3 |- ( ph -> "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } ) )
4 basfn 13355 . . . . . 6 |- Base Fn _V
5 vex 2818 . . . . . 6 |- r e. _V
6 funfvex 5692 . . . . . . 7 |- ( ( Fun Base /\ r e. dom Base ) -> ( Base ` r ) e. _V )
76funfni 5463 . . . . . 6 |- ( ( Base Fn _V /\ r e. _V ) -> ( Base ` r ) e. _V )
84, 5, 7mp2an 426 . . . . 5 |- ( Base ` r ) e. _V
98a1i 9 . . . 4 |- ( ( ph /\ ( f = F /\ r = R ) ) -> ( Base ` r ) e. _V )
10 simplrl 537 . . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> f = F )
1110rneqd 4991 . . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran f = ran F )
12 imasval.f . . . . . . . . 9 |- ( ph -> F : V -onto-> B )
13 forn 5598 . . . . . . . . 9 |- ( F : V -onto-> B -> ran F = B )
1412, 13syl 14 . . . . . . . 8 |- ( ph -> ran F = B )
1514ad2antrr 488 . . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran F = B )
1611, 15eqtrd 2267 . . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran f = B )
1716opeq2d 3895 . . . . 5 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( Base ` ndx ) , ran f >. = <. ( Base ` ndx ) , B >. )
18 simplrr 538 . . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> r = R )
1918fveq2d 5679 . . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` r ) = ( Base ` R ) )
20 simpr 110 . . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> v = ( Base ` r ) )
21 imasval.v . . . . . . . . . 10 |- ( ph -> V = ( Base ` R ) )
2221ad2antrr 488 . . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> V = ( Base ` R ) )
2319, 20, 223eqtr4d 2277 . . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> v = V )
2410fveq1d 5677 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` p ) = ( F ` p ) )
2510fveq1d 5677 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` q ) = ( F ` q ) )
2624, 25opeq12d 3896 . . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( f ` p ) , ( f ` q ) >. = <. ( F ` p ) , ( F ` q ) >. )
2718fveq2d 5679 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( +g ` r ) = ( +g ` R ) )
28 imasval.p . . . . . . . . . . . . . 14 |- .+ = ( +g ` R )
2927, 28eqtr4di 2285 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( +g ` r ) = .+ )
3029oveqd 6075 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( +g ` r ) q ) = ( p .+ q ) )
3110, 30fveq12d 5682 . . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( +g ` r ) q ) ) = ( F ` ( p .+ q ) ) )
3226, 31opeq12d 3896 . . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. )
3332sneqd 3707 . . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
3423, 33iuneq12d 4020 . . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
3523, 34iuneq12d 4020 . . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
36 imasval.a . . . . . . . 8 |- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
3736ad2antrr 488 . . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
3835, 37eqtr4d 2270 . . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = .+b )
3938opeq2d 3895 . . . . 5 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. = <. ( +g ` ndx ) , .+b >. )
4018fveq2d 5679 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .r ` r ) = ( .r ` R ) )
41 imasval.m . . . . . . . . . . . . . 14 |- .X. = ( .r ` R )
4240, 41eqtr4di 2285 . . . . . . . . . . . . 13 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .r ` r ) = .X. )
4342oveqd 6075 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .r ` r ) q ) = ( p .X. q ) )
4410, 43fveq12d 5682 . . . . . . . . . . 11 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( .r ` r ) q ) ) = ( F ` ( p .X. q ) ) )
4526, 44opeq12d 3896 . . . . . . . . . 10 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. )
4645sneqd 3707 . . . . . . . . 9 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
4723, 46iuneq12d 4020 . . . . . . . 8 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
4823, 47iuneq12d 4020 . . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
49 imasval.t . . . . . . . 8 |- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
5049ad2antrr 488 . . . . . . 7 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
5148, 50eqtr4d 2270 . . . . . 6 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = .xb )
5251opeq2d 3895 . . . . 5 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. = <. ( .r ` ndx ) , .xb >. )
5317, 39, 52tpeq123d 3788 . . . 4 |- ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
549, 53csbied 3188 . . 3 |- ( ( ph /\ ( f = F /\ r = R ) ) -> [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
55 fof 5595 . . . . 5 |- ( F : V -onto-> B -> F : V --> B )
5612, 55syl 14 . . . 4 |- ( ph -> F : V --> B )
57 imasval.r . . . . . . 7 |- ( ph -> R e. Z )
5857elexd 2829 . . . . . 6 |- ( ph -> R e. _V )
59 funfvex 5692 . . . . . . 7 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
6059funfni 5463 . . . . . 6 |- ( ( Base Fn _V /\ R e. _V ) -> ( Base ` R ) e. _V )
614, 58, 60sylancr 414 . . . . 5 |- ( ph -> ( Base ` R ) e. _V )
6221, 61eqeltrd 2311 . . . 4 |- ( ph -> V e. _V )
6356, 62fexd 5921 . . 3 |- ( ph -> F e. _V )
64 basendxnn 13352 . . . . 5 |- ( Base ` ndx ) e. NN
65 focdmex 6317 . . . . . 6 |- ( V e. _V -> ( F : V -onto-> B -> B e. _V ) )
6662, 12, 65sylc 62 . . . . 5 |- ( ph -> B e. _V )
67 opexg 4349 . . . . 5 |- ( ( ( Base ` ndx ) e. NN /\ B e. _V ) -> <. ( Base ` ndx ) , B >. e. _V )
6864, 66, 67sylancr 414 . . . 4 |- ( ph -> <. ( Base ` ndx ) , B >. e. _V )
69 plusgndxnn 13408 . . . . 5 |- ( +g ` ndx ) e. NN
7063ad2antrr 488 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> F e. _V )
71 vex 2818 . . . . . . . . . . . . . . 15 |- p e. _V
7271a1i 9 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> p e. _V )
73 fvexg 5694 . . . . . . . . . . . . . 14 |- ( ( F e. _V /\ p e. _V ) -> ( F ` p ) e. _V )
7470, 72, 73syl2anc 411 . . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> ( F ` p ) e. _V )
75 vex 2818 . . . . . . . . . . . . . . 15 |- q e. _V
7675a1i 9 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> q e. _V )
77 fvexg 5694 . . . . . . . . . . . . . 14 |- ( ( F e. _V /\ q e. _V ) -> ( F ` q ) e. _V )
7870, 76, 77syl2anc 411 . . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> ( F ` q ) e. _V )
79 opexg 4349 . . . . . . . . . . . . 13 |- ( ( ( F ` p ) e. _V /\ ( F ` q ) e. _V ) -> <. ( F ` p ) , ( F ` q ) >. e. _V )
8074, 78, 79syl2anc 411 . . . . . . . . . . . 12 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> <. ( F ` p ) , ( F ` q ) >. e. _V )
81 plusgslid 13409 . . . . . . . . . . . . . . . . . 18 |- ( +g = Slot ( +g ` ndx ) /\ ( +g ` ndx ) e. NN )
8281slotex 13323 . . . . . . . . . . . . . . . . 17 |- ( R e. Z -> ( +g ` R ) e. _V )
8357, 82syl 14 . . . . . . . . . . . . . . . 16 |- ( ph -> ( +g ` R ) e. _V )
8428, 83eqeltrid 2321 . . . . . . . . . . . . . . 15 |- ( ph -> .+ e. _V )
8584ad2antrr 488 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> .+ e. _V )
86 ovexg 6092 . . . . . . . . . . . . . 14 |- ( ( p e. _V /\ .+ e. _V /\ q e. _V ) -> ( p .+ q ) e. _V )
8772, 85, 76, 86syl3anc 1274 . . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> ( p .+ q ) e. _V )
88 fvexg 5694 . . . . . . . . . . . . 13 |- ( ( F e. _V /\ ( p .+ q ) e. _V ) -> ( F ` ( p .+ q ) ) e. _V )
8970, 87, 88syl2anc 411 . . . . . . . . . . . 12 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> ( F ` ( p .+ q ) ) e. _V )
90 opexg 4349 . . . . . . . . . . . 12 |- ( ( <. ( F ` p ) , ( F ` q ) >. e. _V /\ ( F ` ( p .+ q ) ) e. _V ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. e. _V )
9180, 89, 90syl2anc 411 . . . . . . . . . . 11 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. e. _V )
92 snexg 4302 . . . . . . . . . . 11 |- ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. e. _V -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V )
9391, 92syl 14 . . . . . . . . . 10 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V )
9493ralrimiva 2617 . . . . . . . . 9 |- ( ( ph /\ p e. V ) -> A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V )
95 iunexg 6321 . . . . . . . . 9 |- ( ( V e. _V /\ A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V )
9662, 94, 95syl2an2r 599 . . . . . . . 8 |- ( ( ph /\ p e. V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V )
9796ralrimiva 2617 . . . . . . 7 |- ( ph -> A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V )
98 iunexg 6321 . . . . . . 7 |- ( ( V e. _V /\ A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V ) -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V )
9962, 97, 98syl2anc 411 . . . . . 6 |- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } e. _V )
10036, 99eqeltrd 2311 . . . . 5 |- ( ph -> .+b e. _V )
101 opexg 4349 . . . . 5 |- ( ( ( +g ` ndx ) e. NN /\ .+b e. _V ) -> <. ( +g ` ndx ) , .+b >. e. _V )
10269, 100, 101sylancr 414 . . . 4 |- ( ph -> <. ( +g ` ndx ) , .+b >. e. _V )
103 mulrslid 13429 . . . . . 6 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
104103simpri 113 . . . . 5 |- ( .r ` ndx ) e. NN
105103slotex 13323 . . . . . . . . . . . . . . . . 17 |- ( R e. Z -> ( .r ` R ) e. _V )
10657, 105syl 14 . . . . . . . . . . . . . . . 16 |- ( ph -> ( .r ` R ) e. _V )
10741, 106eqeltrid 2321 . . . . . . . . . . . . . . 15 |- ( ph -> .X. e. _V )
108107ad2antrr 488 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> .X. e. _V )
109 ovexg 6092 . . . . . . . . . . . . . 14 |- ( ( p e. _V /\ .X. e. _V /\ q e. _V ) -> ( p .X. q ) e. _V )
11072, 108, 76, 109syl3anc 1274 . . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> ( p .X. q ) e. _V )
111 fvexg 5694 . . . . . . . . . . . . 13 |- ( ( F e. _V /\ ( p .X. q ) e. _V ) -> ( F ` ( p .X. q ) ) e. _V )
11270, 110, 111syl2anc 411 . . . . . . . . . . . 12 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> ( F ` ( p .X. q ) ) e. _V )
113 opexg 4349 . . . . . . . . . . . 12 |- ( ( <. ( F ` p ) , ( F ` q ) >. e. _V /\ ( F ` ( p .X. q ) ) e. _V ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. e. _V )
11480, 112, 113syl2anc 411 . . . . . . . . . . 11 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. e. _V )
115 snexg 4302 . . . . . . . . . . 11 |- ( <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. e. _V -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V )
116114, 115syl 14 . . . . . . . . . 10 |- ( ( ( ph /\ p e. V ) /\ q e. V ) -> { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V )
117116ralrimiva 2617 . . . . . . . . 9 |- ( ( ph /\ p e. V ) -> A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V )
118 iunexg 6321 . . . . . . . . 9 |- ( ( V e. _V /\ A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V )
11962, 117, 118syl2an2r 599 . . . . . . . 8 |- ( ( ph /\ p e. V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V )
120119ralrimiva 2617 . . . . . . 7 |- ( ph -> A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V )
121 iunexg 6321 . . . . . . 7 |- ( ( V e. _V /\ A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V ) -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V )
12262, 120, 121syl2anc 411 . . . . . 6 |- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } e. _V )
12349, 122eqeltrd 2311 . . . . 5 |- ( ph -> .xb e. _V )
124 opexg 4349 . . . . 5 |- ( ( ( .r ` ndx ) e. NN /\ .xb e. _V ) -> <. ( .r ` ndx ) , .xb >. e. _V )
125104, 123, 124sylancr 414 . . . 4 |- ( ph -> <. ( .r ` ndx ) , .xb >. e. _V )
126 tpexg 4570 . . . 4 |- ( ( <. ( Base ` ndx ) , B >. e. _V /\ <. ( +g ` ndx ) , .+b >. e. _V /\ <. ( .r ` ndx ) , .xb >. e. _V ) -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } e. _V )
12768, 102, 125, 126syl3anc 1274 . . 3 |- ( ph -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } e. _V )
1283, 54, 63, 58, 127ovmpod 6189 . 2 |- ( ph -> ( F "s R ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
1291, 128eqtrd 2267 1 |- ( ph -> U = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   e. wcel 2205   A.wral 2522   _Vcvv 2815   [_csb 3141   {csn 3694   {ctp 3696   <.cop 3697   U_ciun 3996   ran crn 4755   Fn wfn 5352   -->wf 5353   -onto->wfo 5355   ` cfv 5357  (class class class)co 6058   e. cmpo 6060   NNcn 9254   ndxcnx 13293  Slot cslot 13295   Basecbs 13296   +g cplusg 13374   .rcmulr 13375   .scvsca 13378   "s cimas 13565
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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-coll 4230  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240
This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3046  df-csb 3142  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-tp 3702  df-op 3703  df-uni 3920  df-int 3955  df-iun 3998  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-f1 5362  df-fo 5363  df-f1o 5364  df-fv 5365  df-ov 6061  df-oprab 6062  df-mpo 6063  df-inn 9255  df-2 9313  df-3 9314  df-ndx 13299  df-slot 13300  df-base 13302  df-plusg 13387  df-mulr 13388  df-iimas 13567
This theorem is referenced by:  imasbas  13571  imasplusg  13572  imasmulr  13573
  Copyright terms: Public domain W3C validator