Metamath Proof Explorer


Theorem relexpmulnn

Description: With exponents limited to the counting numbers, the composition of powers of a relation is the relation raised to the product of exponents. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion relexpmulnn R V I = J K J K R r J r K = R r I

Proof

Step Hyp Ref Expression
1 oveq2 x = 1 R r J r x = R r J r 1
2 oveq2 x = 1 J x = J 1
3 2 oveq2d x = 1 R r J x = R r J 1
4 1 3 eqeq12d x = 1 R r J r x = R r J x R r J r 1 = R r J 1
5 4 imbi2d x = 1 J R V I = J K R r J r x = R r J x J R V I = J K R r J r 1 = R r J 1
6 oveq2 x = y R r J r x = R r J r y
7 oveq2 x = y J x = J y
8 7 oveq2d x = y R r J x = R r J y
9 6 8 eqeq12d x = y R r J r x = R r J x R r J r y = R r J y
10 9 imbi2d x = y J R V I = J K R r J r x = R r J x J R V I = J K R r J r y = R r J y
11 oveq2 x = y + 1 R r J r x = R r J r y + 1
12 oveq2 x = y + 1 J x = J y + 1
13 12 oveq2d x = y + 1 R r J x = R r J y + 1
14 11 13 eqeq12d x = y + 1 R r J r x = R r J x R r J r y + 1 = R r J y + 1
15 14 imbi2d x = y + 1 J R V I = J K R r J r x = R r J x J R V I = J K R r J r y + 1 = R r J y + 1
16 oveq2 x = K R r J r x = R r J r K
17 oveq2 x = K J x = J K
18 17 oveq2d x = K R r J x = R r J K
19 16 18 eqeq12d x = K R r J r x = R r J x R r J r K = R r J K
20 19 imbi2d x = K J R V I = J K R r J r x = R r J x J R V I = J K R r J r K = R r J K
21 ovexd J R V I = J K R r J V
22 21 relexp1d J R V I = J K R r J r 1 = R r J
23 simp1 J R V I = J K J
24 nnre J J
25 ax-1rid J J 1 = J
26 23 24 25 3syl J R V I = J K J 1 = J
27 26 eqcomd J R V I = J K J = J 1
28 27 oveq2d J R V I = J K R r J = R r J 1
29 22 28 eqtrd J R V I = J K R r J r 1 = R r J 1
30 ovex R r J V
31 simp1 y J R V I = J K R r J r y = R r J y y
32 relexpsucnnr R r J V y R r J r y + 1 = R r J r y R r J
33 30 31 32 sylancr y J R V I = J K R r J r y = R r J y R r J r y + 1 = R r J r y R r J
34 simp3 y J R V I = J K R r J r y = R r J y R r J r y = R r J y
35 34 coeq1d y J R V I = J K R r J r y = R r J y R r J r y R r J = R r J y R r J
36 simp21 y J R V I = J K R r J r y = R r J y J
37 36 31 nnmulcld y J R V I = J K R r J r y = R r J y J y
38 simp22 y J R V I = J K R r J r y = R r J y R V
39 relexpaddnn J y J R V R r J y R r J = R r J y + J
40 37 36 38 39 syl3anc y J R V I = J K R r J r y = R r J y R r J y R r J = R r J y + J
41 35 40 eqtrd y J R V I = J K R r J r y = R r J y R r J r y R r J = R r J y + J
42 36 nncnd y J R V I = J K R r J r y = R r J y J
43 31 nncnd y J R V I = J K R r J r y = R r J y y
44 1cnd y J R V I = J K R r J r y = R r J y 1
45 42 43 44 adddid y J R V I = J K R r J r y = R r J y J y + 1 = J y + J 1
46 42 mulid1d y J R V I = J K R r J r y = R r J y J 1 = J
47 46 oveq2d y J R V I = J K R r J r y = R r J y J y + J 1 = J y + J
48 45 47 eqtr2d y J R V I = J K R r J r y = R r J y J y + J = J y + 1
49 48 oveq2d y J R V I = J K R r J r y = R r J y R r J y + J = R r J y + 1
50 41 49 eqtrd y J R V I = J K R r J r y = R r J y R r J r y R r J = R r J y + 1
51 33 50 eqtrd y J R V I = J K R r J r y = R r J y R r J r y + 1 = R r J y + 1
52 51 3exp y J R V I = J K R r J r y = R r J y R r J r y + 1 = R r J y + 1
53 52 a2d y J R V I = J K R r J r y = R r J y J R V I = J K R r J r y + 1 = R r J y + 1
54 5 10 15 20 29 53 nnind K J R V I = J K R r J r K = R r J K
55 54 3expd K J R V I = J K R r J r K = R r J K
56 55 impcom J K R V I = J K R r J r K = R r J K
57 56 impd J K R V I = J K R r J r K = R r J K
58 57 impcom R V I = J K J K R r J r K = R r J K
59 simplr R V I = J K J K I = J K
60 59 eqcomd R V I = J K J K J K = I
61 60 oveq2d R V I = J K J K R r J K = R r I
62 58 61 eqtrd R V I = J K J K R r J r K = R r I