Theorem ljoinArray ≪ | index | src | ≫ 

theorem ljoinArray (A: set) (L m n: nat):
  $ L e. Array (Array A n) m -> ljoin L e. Array A (n * m) $;
StepHypRefExpression
1 elArray 
L e. Array (Array A n) m <-> L e. List (Array A n) /\ len L = m
2 elArray 
ljoin L e. Array A (n * m) <-> ljoin L e. List A /\ len (ljoin L) = n * m
3 ljoinT 
L e. List (List A) <-> ljoin L e. List A
4 ssel 
List (Array A n) C_ List (List A) -> L e. List (Array A n) -> L e. List (List A)
5 Listss 
Array A n C_ List A -> List (Array A n) C_ List (List A)
6 ArrayssList 
Array A n C_ List A
7 5, 6 ax_mp 
List (Array A n) C_ List (List A)
8 4, 7 ax_mp 
L e. List (Array A n) -> L e. List (List A)
9 8 anwl 
L e. List (Array A n) /\ len L = m -> L e. List (List A)
10 3, 9 sylib 
L e. List (Array A n) /\ len L = m -> ljoin L e. List A
11 id 
_1 = L -> _1 = L
12 11 eleq1d 
_1 = L -> (_1 e. List (Array A n) <-> L e. List (Array A n))
13 11 ljoineqd 
_1 = L -> ljoin _1 = ljoin L
14 13 leneqd 
_1 = L -> len (ljoin _1) = len (ljoin L)
15 11 leneqd 
_1 = L -> len _1 = len L
16 15 muleq2d 
_1 = L -> n * len _1 = n * len L
17 14, 16 eqeqd 
_1 = L -> (len (ljoin _1) = n * len _1 <-> len (ljoin L) = n * len L)
18 12, 17 imeqd 
_1 = L -> (_1 e. List (Array A n) -> len (ljoin _1) = n * len _1 <-> L e. List (Array A n) -> len (ljoin L) = n * len L)
19 id 
_1 = 0 -> _1 = 0
20 19 eleq1d 
_1 = 0 -> (_1 e. List (Array A n) <-> 0 e. List (Array A n))
21 19 ljoineqd 
_1 = 0 -> ljoin _1 = ljoin 0
22 21 leneqd 
_1 = 0 -> len (ljoin _1) = len (ljoin 0)
23 19 leneqd 
_1 = 0 -> len _1 = len 0
24 23 muleq2d 
_1 = 0 -> n * len _1 = n * len 0
25 22, 24 eqeqd 
_1 = 0 -> (len (ljoin _1) = n * len _1 <-> len (ljoin 0) = n * len 0)
26 20, 25 imeqd 
_1 = 0 -> (_1 e. List (Array A n) -> len (ljoin _1) = n * len _1 <-> 0 e. List (Array A n) -> len (ljoin 0) = n * len 0)
27 id 
_1 = a2 -> _1 = a2
28 27 eleq1d 
_1 = a2 -> (_1 e. List (Array A n) <-> a2 e. List (Array A n))
29 27 ljoineqd 
_1 = a2 -> ljoin _1 = ljoin a2
30 29 leneqd 
_1 = a2 -> len (ljoin _1) = len (ljoin a2)
31 27 leneqd 
_1 = a2 -> len _1 = len a2
32 31 muleq2d 
_1 = a2 -> n * len _1 = n * len a2
33 30, 32 eqeqd 
_1 = a2 -> (len (ljoin _1) = n * len _1 <-> len (ljoin a2) = n * len a2)
34 28, 33 imeqd 
_1 = a2 -> (_1 e. List (Array A n) -> len (ljoin _1) = n * len _1 <-> a2 e. List (Array A n) -> len (ljoin a2) = n * len a2)
35 id 
_1 = a1 : a2 -> _1 = a1 : a2
36 35 eleq1d 
_1 = a1 : a2 -> (_1 e. List (Array A n) <-> a1 : a2 e. List (Array A n))
37 35 ljoineqd 
_1 = a1 : a2 -> ljoin _1 = ljoin (a1 : a2)
38 37 leneqd 
_1 = a1 : a2 -> len (ljoin _1) = len (ljoin (a1 : a2))
39 35 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
40 39 muleq2d 
_1 = a1 : a2 -> n * len _1 = n * len (a1 : a2)
41 38, 40 eqeqd 
_1 = a1 : a2 -> (len (ljoin _1) = n * len _1 <-> len (ljoin (a1 : a2)) = n * len (a1 : a2))
42 36, 41 imeqd 
_1 = a1 : a2 -> (_1 e. List (Array A n) -> len (ljoin _1) = n * len _1 <-> a1 : a2 e. List (Array A n) -> len (ljoin (a1 : a2)) = n * len (a1 : a2))
43 eqtr 
len (ljoin 0) = len 0 -> len 0 = n * len 0 -> len (ljoin 0) = n * len 0
44 leneq 
ljoin 0 = 0 -> len (ljoin 0) = len 0
45 ljoin0 
ljoin 0 = 0
46 44, 45 ax_mp 
len (ljoin 0) = len 0
47 43, 46 ax_mp 
len 0 = n * len 0 -> len (ljoin 0) = n * len 0
48 eqtr4 
len 0 = 0 -> n * len 0 = 0 -> len 0 = n * len 0
49 len0 
len 0 = 0
50 48, 49 ax_mp 
n * len 0 = 0 -> len 0 = n * len 0
51 eqtr 
n * len 0 = n * 0 -> n * 0 = 0 -> n * len 0 = 0
52 muleq2 
len 0 = 0 -> n * len 0 = n * 0
53 52, 49 ax_mp 
n * len 0 = n * 0
54 51, 53 ax_mp 
n * 0 = 0 -> n * len 0 = 0
55 mul02 
n * 0 = 0
56 54, 55 ax_mp 
n * len 0 = 0
57 50, 56 ax_mp 
len 0 = n * len 0
58 47, 57 ax_mp 
len (ljoin 0) = n * len 0
59 58 a1i 
0 e. List (Array A n) -> len (ljoin 0) = n * len 0
60 elListS 
a1 : a2 e. List (Array A n) <-> a1 e. Array A n /\ a2 e. List (Array A n)
61 anr 
a1 e. Array A n /\ a2 e. List (Array A n) -> a2 e. List (Array A n)
62 eqeq 
len (ljoin (a1 : a2)) = len a1 + len (ljoin a2) ->
  n * len (a1 : a2) = n * len a2 + n ->
  (len (ljoin (a1 : a2)) = n * len (a1 : a2) <-> len a1 + len (ljoin a2) = n * len a2 + n)
63 eqtr 
len (ljoin (a1 : a2)) = len (a1 ++ ljoin a2) -> len (a1 ++ ljoin a2) = len a1 + len (ljoin a2) -> len (ljoin (a1 : a2)) = len a1 + len (ljoin a2)
64 leneq 
ljoin (a1 : a2) = a1 ++ ljoin a2 -> len (ljoin (a1 : a2)) = len (a1 ++ ljoin a2)
65 ljoinS 
ljoin (a1 : a2) = a1 ++ ljoin a2
66 64, 65 ax_mp 
len (ljoin (a1 : a2)) = len (a1 ++ ljoin a2)
67 63, 66 ax_mp 
len (a1 ++ ljoin a2) = len a1 + len (ljoin a2) -> len (ljoin (a1 : a2)) = len a1 + len (ljoin a2)
68 appendlen 
len (a1 ++ ljoin a2) = len a1 + len (ljoin a2)
69 67, 68 ax_mp 
len (ljoin (a1 : a2)) = len a1 + len (ljoin a2)
70 62, 69 ax_mp 
n * len (a1 : a2) = n * len a2 + n -> (len (ljoin (a1 : a2)) = n * len (a1 : a2) <-> len a1 + len (ljoin a2) = n * len a2 + n)
71 eqtr 
n * len (a1 : a2) = n * suc (len a2) -> n * suc (len a2) = n * len a2 + n -> n * len (a1 : a2) = n * len a2 + n
72 muleq2 
len (a1 : a2) = suc (len a2) -> n * len (a1 : a2) = n * suc (len a2)
73 lenS 
len (a1 : a2) = suc (len a2)
74 72, 73 ax_mp 
n * len (a1 : a2) = n * suc (len a2)
75 71, 74 ax_mp 
n * suc (len a2) = n * len a2 + n -> n * len (a1 : a2) = n * len a2 + n
76 mulS2 
n * suc (len a2) = n * len a2 + n
77 75, 76 ax_mp 
n * len (a1 : a2) = n * len a2 + n
78 70, 77 ax_mp 
len (ljoin (a1 : a2)) = n * len (a1 : a2) <-> len a1 + len (ljoin a2) = n * len a2 + n
79 addeq1 
len (ljoin a2) = n * len a2 -> len (ljoin a2) + n = n * len a2 + n
80 79 eqeq2d 
len (ljoin a2) = n * len a2 -> (len a1 + len (ljoin a2) = len (ljoin a2) + n <-> len a1 + len (ljoin a2) = n * len a2 + n)
81 addcom 
len a1 + len (ljoin a2) = len (ljoin a2) + len a1
82 elArray 
a1 e. Array A n <-> a1 e. List A /\ len a1 = n
83 anr 
a1 e. List A /\ len a1 = n -> len a1 = n
84 82, 83 sylbi 
a1 e. Array A n -> len a1 = n
85 84 anwl 
a1 e. Array A n /\ a2 e. List (Array A n) -> len a1 = n
86 85 addeq2d 
a1 e. Array A n /\ a2 e. List (Array A n) -> len (ljoin a2) + len a1 = len (ljoin a2) + n
87 81, 86 syl5eq 
a1 e. Array A n /\ a2 e. List (Array A n) -> len a1 + len (ljoin a2) = len (ljoin a2) + n
88 80, 87 syl5ibcom 
a1 e. Array A n /\ a2 e. List (Array A n) -> len (ljoin a2) = n * len a2 -> len a1 + len (ljoin a2) = n * len a2 + n
89 78, 88 syl6ibr 
a1 e. Array A n /\ a2 e. List (Array A n) -> len (ljoin a2) = n * len a2 -> len (ljoin (a1 : a2)) = n * len (a1 : a2)
90 61, 89 eimd 
a1 e. Array A n /\ a2 e. List (Array A n) -> (a2 e. List (Array A n) -> len (ljoin a2) = n * len a2) -> len (ljoin (a1 : a2)) = n * len (a1 : a2)
91 90 com12 
(a2 e. List (Array A n) -> len (ljoin a2) = n * len a2) -> a1 e. Array A n /\ a2 e. List (Array A n) -> len (ljoin (a1 : a2)) = n * len (a1 : a2)
92 60, 91 syl5bi 
(a2 e. List (Array A n) -> len (ljoin a2) = n * len a2) -> a1 : a2 e. List (Array A n) -> len (ljoin (a1 : a2)) = n * len (a1 : a2)
93 18, 26, 34, 42, 59, 92 listind 
L e. List (Array A n) -> len (ljoin L) = n * len L
94 93 anwl 
L e. List (Array A n) /\ len L = m -> len (ljoin L) = n * len L
95 anr 
L e. List (Array A n) /\ len L = m -> len L = m
96 95 muleq2d 
L e. List (Array A n) /\ len L = m -> n * len L = n * m
97 94, 96 eqtrd 
L e. List (Array A n) /\ len L = m -> len (ljoin L) = n * m
98 10, 97 iand 
L e. List (Array A n) /\ len L = m -> ljoin L e. List A /\ len (ljoin L) = n * m
99 2, 98 sylibr 
L e. List (Array A n) /\ len L = m -> ljoin L e. Array A (n * m)
100 1, 99 sylbi 
L e. Array (Array A n) m -> ljoin L e. Array A (n * m)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)