frlmvscadiccat

Description: Scalar multiplication distributes over concatenation. (Contributed by SN, 6-Sep-2023)

	Ref	Expression
Hypotheses	frlmfzoccat.w	$⊢ W = K freeLMod (0 ..^L)$
	frlmfzoccat.x	$⊢ X = K freeLMod (0 ..^M)$
	frlmfzoccat.y	$⊢ Y = K freeLMod (0 ..^N)$
	frlmfzoccat.b	$⊢ B = {Base}_{W}$
	frlmfzoccat.c	$⊢ C = {Base}_{X}$
	frlmfzoccat.d	$⊢ D = {Base}_{Y}$
	frlmfzoccat.k	$⊢ φ \to K \in Z$
	frlmfzoccat.l	$⊢ φ \to M + N = L$
	frlmfzoccat.m	$⊢ φ \to M \in ℕ_{0}$
	frlmfzoccat.n	$⊢ φ \to N \in ℕ_{0}$
	frlmfzoccat.u	$⊢ φ \to U \in C$
	frlmfzoccat.v	$⊢ φ \to V \in D$
	frlmvscadiccat.o	$⊢ O = \cdot_{W}$
	frlmvscadiccat.p	$⊢ \underset{˙}{∙} = \cdot_{X}$
	frlmvscadiccat.q	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	frlmvscadiccat.s	$⊢ S = {Base}_{K}$
	frlmvscadiccat.a	$⊢ φ \to A \in S$
Assertion	frlmvscadiccat	$⊢ φ \to A O (U ++ V) = (A \underset{˙}{∙} U) ++ (A \underset{˙}{\cdot} V)$

Proof

Step	Hyp	Ref	Expression
1		frlmfzoccat.w	$⊢ W = K freeLMod (0 ..^L)$
2		frlmfzoccat.x	$⊢ X = K freeLMod (0 ..^M)$
3		frlmfzoccat.y	$⊢ Y = K freeLMod (0 ..^N)$
4		frlmfzoccat.b	$⊢ B = {Base}_{W}$
5		frlmfzoccat.c	$⊢ C = {Base}_{X}$
6		frlmfzoccat.d	$⊢ D = {Base}_{Y}$
7		frlmfzoccat.k	$⊢ φ \to K \in Z$
8		frlmfzoccat.l	$⊢ φ \to M + N = L$
9		frlmfzoccat.m	$⊢ φ \to M \in ℕ_{0}$
10		frlmfzoccat.n	$⊢ φ \to N \in ℕ_{0}$
11		frlmfzoccat.u	$⊢ φ \to U \in C$
12		frlmfzoccat.v	$⊢ φ \to V \in D$
13		frlmvscadiccat.o	$⊢ O = \cdot_{W}$
14		frlmvscadiccat.p	$⊢ \underset{˙}{∙} = \cdot_{X}$
15		frlmvscadiccat.q	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
16		frlmvscadiccat.s	$⊢ S = {Base}_{K}$
17		frlmvscadiccat.a	$⊢ φ \to A \in S$
18		fconstg	$⊢ A \in S \to ((0 ..^L) \times \{A\}) : (0 ..^L) ⟶ \{A\}$
19	17 18	syl	$⊢ φ \to ((0 ..^L) \times \{A\}) : (0 ..^L) ⟶ \{A\}$
20	19	ffnd	$⊢ φ \to ((0 ..^L) \times \{A\}) Fn (0 ..^L)$
21		fconstg	$⊢ A \in S \to ((0 ..^M) \times \{A\}) : (0 ..^M) ⟶ \{A\}$
22		iswrdi	$⊢ ((0 ..^M) \times \{A\}) : (0 ..^M) ⟶ \{A\} \to (0 ..^M) \times \{A\} \in Word \{A\}$
23	17 21 22	3syl	$⊢ φ \to (0 ..^M) \times \{A\} \in Word \{A\}$
24		fconstg	$⊢ A \in S \to ((0 ..^N) \times \{A\}) : (0 ..^N) ⟶ \{A\}$
25		iswrdi	$⊢ ((0 ..^N) \times \{A\}) : (0 ..^N) ⟶ \{A\} \to (0 ..^N) \times \{A\} \in Word \{A\}$
26	17 24 25	3syl	$⊢ φ \to (0 ..^N) \times \{A\} \in Word \{A\}$
27		ccatvalfn	$⊢ ((0 ..^M) \times \{A\} \in Word \{A\} \land (0 ..^N) \times \{A\} \in Word \{A\}) \to (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) Fn (0 ..^\|(0 ..^M) \times \{A\}\| + \|(0 ..^N) \times \{A\}\|)$
28	23 26 27	syl2anc	$⊢ φ \to (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) Fn (0 ..^\|(0 ..^M) \times \{A\}\| + \|(0 ..^N) \times \{A\}\|)$
29		fzofi	$⊢ (0 ..^M) \in Fin$
30		snfi	$⊢ \{A\} \in Fin$
31		hashxp	$⊢ ((0 ..^M) \in Fin \land \{A\} \in Fin) \to \|(0 ..^M) \times \{A\}\| = \|(0 ..^M)\| \|\{A\}\|$
32	29 30 31	mp2an	$⊢ \|(0 ..^M) \times \{A\}\| = \|(0 ..^M)\| \|\{A\}\|$
33		hashsng	$⊢ A \in S \to \|\{A\}\| = 1$
34	17 33	syl	$⊢ φ \to \|\{A\}\| = 1$
35	34	oveq2d	$⊢ φ \to \|(0 ..^M)\| \|\{A\}\| = \|(0 ..^M)\| \cdot 1$
36		hashcl	$⊢ (0 ..^M) \in Fin \to \|(0 ..^M)\| \in ℕ_{0}$
37	29 36	mp1i	$⊢ φ \to \|(0 ..^M)\| \in ℕ_{0}$
38	37	nn0cnd	$⊢ φ \to \|(0 ..^M)\| \in ℂ$
39	38	mulid1d	$⊢ φ \to \|(0 ..^M)\| \cdot 1 = \|(0 ..^M)\|$
40		hashfzo0	$⊢ M \in ℕ_{0} \to \|(0 ..^M)\| = M$
41	9 40	syl	$⊢ φ \to \|(0 ..^M)\| = M$
42	35 39 41	3eqtrd	$⊢ φ \to \|(0 ..^M)\| \|\{A\}\| = M$
43	32 42	syl5eq	$⊢ φ \to \|(0 ..^M) \times \{A\}\| = M$
44		fzofi	$⊢ (0 ..^N) \in Fin$
45		hashxp	$⊢ ((0 ..^N) \in Fin \land \{A\} \in Fin) \to \|(0 ..^N) \times \{A\}\| = \|(0 ..^N)\| \|\{A\}\|$
46	44 30 45	mp2an	$⊢ \|(0 ..^N) \times \{A\}\| = \|(0 ..^N)\| \|\{A\}\|$
47	34	oveq2d	$⊢ φ \to \|(0 ..^N)\| \|\{A\}\| = \|(0 ..^N)\| \cdot 1$
48		hashcl	$⊢ (0 ..^N) \in Fin \to \|(0 ..^N)\| \in ℕ_{0}$
49	44 48	mp1i	$⊢ φ \to \|(0 ..^N)\| \in ℕ_{0}$
50	49	nn0cnd	$⊢ φ \to \|(0 ..^N)\| \in ℂ$
51	50	mulid1d	$⊢ φ \to \|(0 ..^N)\| \cdot 1 = \|(0 ..^N)\|$
52		hashfzo0	$⊢ N \in ℕ_{0} \to \|(0 ..^N)\| = N$
53	10 52	syl	$⊢ φ \to \|(0 ..^N)\| = N$
54	47 51 53	3eqtrd	$⊢ φ \to \|(0 ..^N)\| \|\{A\}\| = N$
55	46 54	syl5eq	$⊢ φ \to \|(0 ..^N) \times \{A\}\| = N$
56	43 55	oveq12d	$⊢ φ \to \|(0 ..^M) \times \{A\}\| + \|(0 ..^N) \times \{A\}\| = M + N$
57	56 8	eqtrd	$⊢ φ \to \|(0 ..^M) \times \{A\}\| + \|(0 ..^N) \times \{A\}\| = L$
58	57	oveq2d	$⊢ φ \to (0 ..^\|(0 ..^M) \times \{A\}\| + \|(0 ..^N) \times \{A\}\|) = (0 ..^L)$
59	58	fneq2d	$⊢ φ \to ((((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) Fn (0 ..^\|(0 ..^M) \times \{A\}\| + \|(0 ..^N) \times \{A\}\|) \leftrightarrow (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) Fn (0 ..^L))$
60	28 59	mpbid	$⊢ φ \to (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) Fn (0 ..^L)$
61	43	adantr	$⊢ (φ \land x \in (0 ..^L)) \to \|(0 ..^M) \times \{A\}\| = M$
62	61	breq2d	$⊢ (φ \land x \in (0 ..^L)) \to (x < \|(0 ..^M) \times \{A\}\| \leftrightarrow x < M)$
63	62	ifbid	$⊢ (φ \land x \in (0 ..^L)) \to if (x < \|(0 ..^M) \times \{A\}\|, ((0 ..^M) \times \{A\}) (x), ((0 ..^N) \times \{A\}) (x - \|(0 ..^M) \times \{A\}\|)) = if (x < M, ((0 ..^M) \times \{A\}) (x), ((0 ..^N) \times \{A\}) (x - \|(0 ..^M) \times \{A\}\|))$
64	17	adantr	$⊢ (φ \land x \in (0 ..^L)) \to A \in S$
65		elfzouz	$⊢ x \in (0 ..^L) \to x \in ℤ_{\geq 0}$
66	65	ad2antlr	$⊢ ((φ \land x \in (0 ..^L)) \land x < M) \to x \in ℤ_{\geq 0}$
67	9	ad2antrr	$⊢ ((φ \land x \in (0 ..^L)) \land x < M) \to M \in ℕ_{0}$
68	67	nn0zd	$⊢ ((φ \land x \in (0 ..^L)) \land x < M) \to M \in ℤ$
69		simpr	$⊢ ((φ \land x \in (0 ..^L)) \land x < M) \to x < M$
70		elfzo2	$⊢ x \in (0 ..^M) \leftrightarrow (x \in ℤ_{\geq 0} \land M \in ℤ \land x < M)$
71	66 68 69 70	syl3anbrc	$⊢ ((φ \land x \in (0 ..^L)) \land x < M) \to x \in (0 ..^M)$
72		fvconst2g	$⊢ (A \in S \land x \in (0 ..^M)) \to ((0 ..^M) \times \{A\}) (x) = A$
73	64 71 72	syl2an2r	$⊢ ((φ \land x \in (0 ..^L)) \land x < M) \to ((0 ..^M) \times \{A\}) (x) = A$
74	43	ad2antrr	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to \|(0 ..^M) \times \{A\}\| = M$
75	74	oveq2d	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to x - \|(0 ..^M) \times \{A\}\| = x - M$
76	9	ad2antrr	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to M \in ℕ_{0}$
77		elfzonn0	$⊢ x \in (0 ..^L) \to x \in ℕ_{0}$
78	77	ad2antlr	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to x \in ℕ_{0}$
79	9	adantr	$⊢ (φ \land x \in (0 ..^L)) \to M \in ℕ_{0}$
80	79	nn0red	$⊢ (φ \land x \in (0 ..^L)) \to M \in ℝ$
81		elfzoelz	$⊢ x \in (0 ..^L) \to x \in ℤ$
82	81	adantl	$⊢ (φ \land x \in (0 ..^L)) \to x \in ℤ$
83	82	zred	$⊢ (φ \land x \in (0 ..^L)) \to x \in ℝ$
84	80 83	lenltd	$⊢ (φ \land x \in (0 ..^L)) \to (M \leq x \leftrightarrow \neg x < M)$
85	84	biimpar	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to M \leq x$
86		nn0sub2	$⊢ (M \in ℕ_{0} \land x \in ℕ_{0} \land M \leq x) \to x - M \in ℕ_{0}$
87	76 78 85 86	syl3anc	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to x - M \in ℕ_{0}$
88		elnn0uz	$⊢ x - M \in ℕ_{0} \leftrightarrow x - M \in ℤ_{\geq 0}$
89	87 88	sylib	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to x - M \in ℤ_{\geq 0}$
90	10	ad2antrr	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to N \in ℕ_{0}$
91	90	nn0zd	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to N \in ℤ$
92		elfzolt2	$⊢ x \in (0 ..^L) \to x < L$
93	92	adantl	$⊢ (φ \land x \in (0 ..^L)) \to x < L$
94	80	recnd	$⊢ (φ \land x \in (0 ..^L)) \to M \in ℂ$
95	83	recnd	$⊢ (φ \land x \in (0 ..^L)) \to x \in ℂ$
96	94 95	pncan3d	$⊢ (φ \land x \in (0 ..^L)) \to M + x - M = x$
97	8	adantr	$⊢ (φ \land x \in (0 ..^L)) \to M + N = L$
98	93 96 97	3brtr4d	$⊢ (φ \land x \in (0 ..^L)) \to M + x - M < M + N$
99	83 80	resubcld	$⊢ (φ \land x \in (0 ..^L)) \to x - M \in ℝ$
100	10	adantr	$⊢ (φ \land x \in (0 ..^L)) \to N \in ℕ_{0}$
101	100	nn0red	$⊢ (φ \land x \in (0 ..^L)) \to N \in ℝ$
102	99 101 80	ltadd2d	$⊢ (φ \land x \in (0 ..^L)) \to (x - M < N \leftrightarrow M + x - M < M + N)$
103	98 102	mpbird	$⊢ (φ \land x \in (0 ..^L)) \to x - M < N$
104	103	adantr	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to x - M < N$
105		elfzo2	$⊢ x - M \in (0 ..^N) \leftrightarrow (x - M \in ℤ_{\geq 0} \land N \in ℤ \land x - M < N)$
106	89 91 104 105	syl3anbrc	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to x - M \in (0 ..^N)$
107	75 106	eqeltrd	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to x - \|(0 ..^M) \times \{A\}\| \in (0 ..^N)$
108		fvconst2g	$⊢ (A \in S \land x - \|(0 ..^M) \times \{A\}\| \in (0 ..^N)) \to ((0 ..^N) \times \{A\}) (x - \|(0 ..^M) \times \{A\}\|) = A$
109	64 107 108	syl2an2r	$⊢ ((φ \land x \in (0 ..^L)) \land \neg x < M) \to ((0 ..^N) \times \{A\}) (x - \|(0 ..^M) \times \{A\}\|) = A$
110	73 109	ifeqda	$⊢ (φ \land x \in (0 ..^L)) \to if (x < M, ((0 ..^M) \times \{A\}) (x), ((0 ..^N) \times \{A\}) (x - \|(0 ..^M) \times \{A\}\|)) = A$
111	63 110	eqtr2d	$⊢ (φ \land x \in (0 ..^L)) \to A = if (x < \|(0 ..^M) \times \{A\}\|, ((0 ..^M) \times \{A\}) (x), ((0 ..^N) \times \{A\}) (x - \|(0 ..^M) \times \{A\}\|))$
112		fvconst2g	$⊢ (A \in S \land x \in (0 ..^L)) \to ((0 ..^L) \times \{A\}) (x) = A$
113	17 112	sylan	$⊢ (φ \land x \in (0 ..^L)) \to ((0 ..^L) \times \{A\}) (x) = A$
114	64 21 22	3syl	$⊢ (φ \land x \in (0 ..^L)) \to (0 ..^M) \times \{A\} \in Word \{A\}$
115	64 24 25	3syl	$⊢ (φ \land x \in (0 ..^L)) \to (0 ..^N) \times \{A\} \in Word \{A\}$
116		ccatsymb	$⊢ ((0 ..^M) \times \{A\} \in Word \{A\} \land (0 ..^N) \times \{A\} \in Word \{A\} \land x \in ℤ) \to (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) (x) = if (x < \|(0 ..^M) \times \{A\}\|, ((0 ..^M) \times \{A\}) (x), ((0 ..^N) \times \{A\}) (x - \|(0 ..^M) \times \{A\}\|))$
117	114 115 82 116	syl3anc	$⊢ (φ \land x \in (0 ..^L)) \to (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) (x) = if (x < \|(0 ..^M) \times \{A\}\|, ((0 ..^M) \times \{A\}) (x), ((0 ..^N) \times \{A\}) (x - \|(0 ..^M) \times \{A\}\|))$
118	111 113 117	3eqtr4d	$⊢ (φ \land x \in (0 ..^L)) \to ((0 ..^L) \times \{A\}) (x) = (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) (x)$
119	20 60 118	eqfnfvd	$⊢ φ \to (0 ..^L) \times \{A\} = ((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})$
120	119	oveq1d	$⊢ φ \to ((0 ..^L) \times \{A\}) {\cdot_{K}}_{f} (U ++ V) = (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) {\cdot_{K}}_{f} (U ++ V)$
121	2 5 16	frlmfzowrd	$⊢ U \in C \to U \in Word S$
122	11 121	syl	$⊢ φ \to U \in Word S$
123	3 6 16	frlmfzowrd	$⊢ V \in D \to V \in Word S$
124	12 123	syl	$⊢ φ \to V \in Word S$
125	32 35	syl5eq	$⊢ φ \to \|(0 ..^M) \times \{A\}\| = \|(0 ..^M)\| \cdot 1$
126		ovexd	$⊢ φ \to (0 ..^M) \in V$
127	2 16 5	frlmbasf	$⊢ ((0 ..^M) \in V \land U \in C) \to U : (0 ..^M) ⟶ S$
128	126 11 127	syl2anc	$⊢ φ \to U : (0 ..^M) ⟶ S$
129	128	ffnd	$⊢ φ \to U Fn (0 ..^M)$
130		hashfn	$⊢ U Fn (0 ..^M) \to \|U\| = \|(0 ..^M)\|$
131	129 130	syl	$⊢ φ \to \|U\| = \|(0 ..^M)\|$
132	39 125 131	3eqtr4d	$⊢ φ \to \|(0 ..^M) \times \{A\}\| = \|U\|$
133	47 51	eqtrd	$⊢ φ \to \|(0 ..^N)\| \|\{A\}\| = \|(0 ..^N)\|$
134	46 133	syl5eq	$⊢ φ \to \|(0 ..^N) \times \{A\}\| = \|(0 ..^N)\|$
135		ovexd	$⊢ φ \to (0 ..^N) \in V$
136	3 16 6	frlmbasf	$⊢ ((0 ..^N) \in V \land V \in D) \to V : (0 ..^N) ⟶ S$
137	135 12 136	syl2anc	$⊢ φ \to V : (0 ..^N) ⟶ S$
138	137	ffnd	$⊢ φ \to V Fn (0 ..^N)$
139		hashfn	$⊢ V Fn (0 ..^N) \to \|V\| = \|(0 ..^N)\|$
140	138 139	syl	$⊢ φ \to \|V\| = \|(0 ..^N)\|$
141	134 140	eqtr4d	$⊢ φ \to \|(0 ..^N) \times \{A\}\| = \|V\|$
142	23 26 122 124 132 141	ofccat	$⊢ φ \to (((0 ..^M) \times \{A\}) ++ ((0 ..^N) \times \{A\})) {\cdot_{K}}_{f} (U ++ V) = (((0 ..^M) \times \{A\}) {\cdot_{K}}_{f} U) ++ (((0 ..^N) \times \{A\}) {\cdot_{K}}_{f} V)$
143	120 142	eqtrd	$⊢ φ \to ((0 ..^L) \times \{A\}) {\cdot_{K}}_{f} (U ++ V) = (((0 ..^M) \times \{A\}) {\cdot_{K}}_{f} U) ++ (((0 ..^N) \times \{A\}) {\cdot_{K}}_{f} V)$
144		ovexd	$⊢ φ \to (0 ..^L) \in V$
145	1 2 3 4 5 6 7 8 9 10 11 12	frlmfzoccat	$⊢ φ \to U ++ V \in B$
146		eqid	$⊢ \cdot_{K} = \cdot_{K}$
147	1 4 16 144 17 145 13 146	frlmvscafval	$⊢ φ \to A O (U ++ V) = ((0 ..^L) \times \{A\}) {\cdot_{K}}_{f} (U ++ V)$
148	2 5 16 126 17 11 14 146	frlmvscafval	$⊢ φ \to A \underset{˙}{∙} U = ((0 ..^M) \times \{A\}) {\cdot_{K}}_{f} U$
149	3 6 16 135 17 12 15 146	frlmvscafval	$⊢ φ \to A \underset{˙}{\cdot} V = ((0 ..^N) \times \{A\}) {\cdot_{K}}_{f} V$
150	148 149	oveq12d	$⊢ φ \to (A \underset{˙}{∙} U) ++ (A \underset{˙}{\cdot} V) = (((0 ..^M) \times \{A\}) {\cdot_{K}}_{f} U) ++ (((0 ..^N) \times \{A\}) {\cdot_{K}}_{f} V)$
151	143 147 150	3eqtr4d	$⊢ φ \to A O (U ++ V) = (A \underset{˙}{∙} U) ++ (A \underset{˙}{\cdot} V)$

Metamath Proof Explorer

Theorem frlmvscadiccat

Proof