Theorem ljoinappend ≪ | index | src | ≫

theorem ljoinappend (L1 L2: nat): $ ljoin (L1 ++ L2) = ljoin L1 ++ ljoin L2 $;

Step	Hyp	Ref	Expression
1		id	_1 = L1 -> _1 = L1
2	1	appendeq1d	_1 = L1 -> _1 ++ L2 = L1 ++ L2
3	2	ljoineqd	_1 = L1 -> ljoin (_1 ++ L2) = ljoin (L1 ++ L2)
4	1	ljoineqd	_1 = L1 -> ljoin _1 = ljoin L1
5	4	appendeq1d	_1 = L1 -> ljoin _1 ++ ljoin L2 = ljoin L1 ++ ljoin L2
6	3, 5	eqeqd	_1 = L1 -> (ljoin (_1 ++ L2) = ljoin _1 ++ ljoin L2 <-> ljoin (L1 ++ L2) = ljoin L1 ++ ljoin L2)
7		id	_1 = 0 -> _1 = 0
8	7	appendeq1d	_1 = 0 -> _1 ++ L2 = 0 ++ L2
9	8	ljoineqd	_1 = 0 -> ljoin (_1 ++ L2) = ljoin (0 ++ L2)
10	7	ljoineqd	_1 = 0 -> ljoin _1 = ljoin 0
11	10	appendeq1d	_1 = 0 -> ljoin _1 ++ ljoin L2 = ljoin 0 ++ ljoin L2
12	9, 11	eqeqd	_1 = 0 -> (ljoin (_1 ++ L2) = ljoin _1 ++ ljoin L2 <-> ljoin (0 ++ L2) = ljoin 0 ++ ljoin L2)
13		id	_1 = a2 -> _1 = a2
14	13	appendeq1d	_1 = a2 -> _1 ++ L2 = a2 ++ L2
15	14	ljoineqd	_1 = a2 -> ljoin (_1 ++ L2) = ljoin (a2 ++ L2)
16	13	ljoineqd	_1 = a2 -> ljoin _1 = ljoin a2
17	16	appendeq1d	_1 = a2 -> ljoin _1 ++ ljoin L2 = ljoin a2 ++ ljoin L2
18	15, 17	eqeqd	_1 = a2 -> (ljoin (_1 ++ L2) = ljoin _1 ++ ljoin L2 <-> ljoin (a2 ++ L2) = ljoin a2 ++ ljoin L2)
19		id	_1 = a1 : a2 -> _1 = a1 : a2
20	19	appendeq1d	_1 = a1 : a2 -> _1 ++ L2 = a1 : a2 ++ L2
21	20	ljoineqd	_1 = a1 : a2 -> ljoin (_1 ++ L2) = ljoin (a1 : a2 ++ L2)
22	19	ljoineqd	_1 = a1 : a2 -> ljoin _1 = ljoin (a1 : a2)
23	22	appendeq1d	_1 = a1 : a2 -> ljoin _1 ++ ljoin L2 = ljoin (a1 : a2) ++ ljoin L2
24	21, 23	eqeqd	_1 = a1 : a2 -> (ljoin (_1 ++ L2) = ljoin _1 ++ ljoin L2 <-> ljoin (a1 : a2 ++ L2) = ljoin (a1 : a2) ++ ljoin L2)
25		eqtr4	ljoin (0 ++ L2) = ljoin L2 -> ljoin 0 ++ ljoin L2 = ljoin L2 -> ljoin (0 ++ L2) = ljoin 0 ++ ljoin L2
26		ljoineq	0 ++ L2 = L2 -> ljoin (0 ++ L2) = ljoin L2
27		append0	0 ++ L2 = L2
28	26, 27	ax_mp	ljoin (0 ++ L2) = ljoin L2
29	25, 28	ax_mp	ljoin 0 ++ ljoin L2 = ljoin L2 -> ljoin (0 ++ L2) = ljoin 0 ++ ljoin L2
30		eqtr	ljoin 0 ++ ljoin L2 = 0 ++ ljoin L2 -> 0 ++ ljoin L2 = ljoin L2 -> ljoin 0 ++ ljoin L2 = ljoin L2
31		appendeq1	ljoin 0 = 0 -> ljoin 0 ++ ljoin L2 = 0 ++ ljoin L2
32		ljoin0	ljoin 0 = 0
33	31, 32	ax_mp	ljoin 0 ++ ljoin L2 = 0 ++ ljoin L2
34	30, 33	ax_mp	0 ++ ljoin L2 = ljoin L2 -> ljoin 0 ++ ljoin L2 = ljoin L2
35		append0	0 ++ ljoin L2 = ljoin L2
36	34, 35	ax_mp	ljoin 0 ++ ljoin L2 = ljoin L2
37	29, 36	ax_mp	ljoin (0 ++ L2) = ljoin 0 ++ ljoin L2
38		ljoineq	a1 : a2 ++ L2 = a1 : (a2 ++ L2) -> ljoin (a1 : a2 ++ L2) = ljoin (a1 : (a2 ++ L2))
39		appendS	a1 : a2 ++ L2 = a1 : (a2 ++ L2)
40	38, 39	ax_mp	ljoin (a1 : a2 ++ L2) = ljoin (a1 : (a2 ++ L2))
41		ljoinS	ljoin (a1 : (a2 ++ L2)) = a1 ++ ljoin (a2 ++ L2)
42		appendeq1	ljoin (a1 : a2) = a1 ++ ljoin a2 -> ljoin (a1 : a2) ++ ljoin L2 = (a1 ++ ljoin a2) ++ ljoin L2
43		ljoinS	ljoin (a1 : a2) = a1 ++ ljoin a2
44	42, 43	ax_mp	ljoin (a1 : a2) ++ ljoin L2 = (a1 ++ ljoin a2) ++ ljoin L2
45		appendass	(a1 ++ ljoin a2) ++ ljoin L2 = a1 ++ ljoin a2 ++ ljoin L2
46		appendeq2	ljoin (a2 ++ L2) = ljoin a2 ++ ljoin L2 -> a1 ++ ljoin (a2 ++ L2) = a1 ++ ljoin a2 ++ ljoin L2
47	45, 46	syl6eqr	ljoin (a2 ++ L2) = ljoin a2 ++ ljoin L2 -> a1 ++ ljoin (a2 ++ L2) = (a1 ++ ljoin a2) ++ ljoin L2
48	44, 47	syl6eqr	ljoin (a2 ++ L2) = ljoin a2 ++ ljoin L2 -> a1 ++ ljoin (a2 ++ L2) = ljoin (a1 : a2) ++ ljoin L2
49	41, 48	syl5eq	ljoin (a2 ++ L2) = ljoin a2 ++ ljoin L2 -> ljoin (a1 : (a2 ++ L2)) = ljoin (a1 : a2) ++ ljoin L2
50	40, 49	syl5eq	ljoin (a2 ++ L2) = ljoin a2 ++ ljoin L2 -> ljoin (a1 : a2 ++ L2) = ljoin (a1 : a2) ++ ljoin L2
51	6, 12, 18, 24, 37, 50	listind	ljoin (L1 ++ L2) = ljoin L1 ++ ljoin L2

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)