Metamath Proof Explorer


Theorem prdsleval

Description: Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses prdsbasmpt.y Y = S 𝑠 R
prdsbasmpt.b B = Base Y
prdsbasmpt.s φ S V
prdsbasmpt.i φ I W
prdsbasmpt.r φ R Fn I
prdsplusgval.f φ F B
prdsplusgval.g φ G B
prdsleval.l ˙ = Y
Assertion prdsleval φ F ˙ G x I F x R x G x

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y Y = S 𝑠 R
2 prdsbasmpt.b B = Base Y
3 prdsbasmpt.s φ S V
4 prdsbasmpt.i φ I W
5 prdsbasmpt.r φ R Fn I
6 prdsplusgval.f φ F B
7 prdsplusgval.g φ G B
8 prdsleval.l ˙ = Y
9 df-br F ˙ G F G ˙
10 fnex R Fn I I W R V
11 5 4 10 syl2anc φ R V
12 5 fndmd φ dom R = I
13 1 3 11 2 12 8 prdsle φ ˙ = f g | f g B x I f x R x g x
14 vex f V
15 vex g V
16 14 15 prss f B g B f g B
17 16 anbi1i f B g B x I f x R x g x f g B x I f x R x g x
18 17 opabbii f g | f B g B x I f x R x g x = f g | f g B x I f x R x g x
19 13 18 eqtr4di φ ˙ = f g | f B g B x I f x R x g x
20 19 eleq2d φ F G ˙ F G f g | f B g B x I f x R x g x
21 9 20 syl5bb φ F ˙ G F G f g | f B g B x I f x R x g x
22 fveq1 f = F f x = F x
23 fveq1 g = G g x = G x
24 22 23 breqan12d f = F g = G f x R x g x F x R x G x
25 24 ralbidv f = F g = G x I f x R x g x x I F x R x G x
26 25 opelopab2a F B G B F G f g | f B g B x I f x R x g x x I F x R x G x
27 6 7 26 syl2anc φ F G f g | f B g B x I f x R x g x x I F x R x G x
28 21 27 bitrd φ F ˙ G x I F x R x G x