clmmulg

Description: The group multiple function matches the scalar multiplication function. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	clmmulg.1	$⊢ V = {Base}_{W}$
	clmmulg.2	$⊢ \underset{˙}{∙} = \cdot_{W}$
	clmmulg.3	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	clmmulg	$⊢ (W \in CMod \land A \in ℤ \land B \in V) \to A \underset{˙}{∙} B = A \underset{˙}{\cdot} B$

Proof

Step	Hyp	Ref	Expression
1		clmmulg.1	$⊢ V = {Base}_{W}$
2		clmmulg.2	$⊢ \underset{˙}{∙} = \cdot_{W}$
3		clmmulg.3	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		oveq1	$⊢ x = 0 \to x \underset{˙}{∙} B = 0 \underset{˙}{∙} B$
5		oveq1	$⊢ x = 0 \to x \underset{˙}{\cdot} B = 0 \underset{˙}{\cdot} B$
6	4 5	eqeq12d	$⊢ x = 0 \to (x \underset{˙}{∙} B = x \underset{˙}{\cdot} B \leftrightarrow 0 \underset{˙}{∙} B = 0 \underset{˙}{\cdot} B)$
7		oveq1	$⊢ x = y \to x \underset{˙}{∙} B = y \underset{˙}{∙} B$
8		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} B = y \underset{˙}{\cdot} B$
9	7 8	eqeq12d	$⊢ x = y \to (x \underset{˙}{∙} B = x \underset{˙}{\cdot} B \leftrightarrow y \underset{˙}{∙} B = y \underset{˙}{\cdot} B)$
10		oveq1	$⊢ x = y + 1 \to x \underset{˙}{∙} B = (y + 1) \underset{˙}{∙} B$
11		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\cdot} B = (y + 1) \underset{˙}{\cdot} B$
12	10 11	eqeq12d	$⊢ x = y + 1 \to (x \underset{˙}{∙} B = x \underset{˙}{\cdot} B \leftrightarrow (y + 1) \underset{˙}{∙} B = (y + 1) \underset{˙}{\cdot} B)$
13		oveq1	$⊢ x = - y \to x \underset{˙}{∙} B = (- y) \underset{˙}{∙} B$
14		oveq1	$⊢ x = - y \to x \underset{˙}{\cdot} B = (- y) \underset{˙}{\cdot} B$
15	13 14	eqeq12d	$⊢ x = - y \to (x \underset{˙}{∙} B = x \underset{˙}{\cdot} B \leftrightarrow (- y) \underset{˙}{∙} B = (- y) \underset{˙}{\cdot} B)$
16		oveq1	$⊢ x = A \to x \underset{˙}{∙} B = A \underset{˙}{∙} B$
17		oveq1	$⊢ x = A \to x \underset{˙}{\cdot} B = A \underset{˙}{\cdot} B$
18	16 17	eqeq12d	$⊢ x = A \to (x \underset{˙}{∙} B = x \underset{˙}{\cdot} B \leftrightarrow A \underset{˙}{∙} B = A \underset{˙}{\cdot} B)$
19		eqid	$⊢ 0_{W} = 0_{W}$
20	1 19 2	mulg0	$⊢ B \in V \to 0 \underset{˙}{∙} B = 0_{W}$
21	20	adantl	$⊢ (W \in CMod \land B \in V) \to 0 \underset{˙}{∙} B = 0_{W}$
22		eqid	$⊢ Scalar (W) = Scalar (W)$
23	1 22 3 19	clm0vs	$⊢ (W \in CMod \land B \in V) \to 0 \underset{˙}{\cdot} B = 0_{W}$
24	21 23	eqtr4d	$⊢ (W \in CMod \land B \in V) \to 0 \underset{˙}{∙} B = 0 \underset{˙}{\cdot} B$
25		oveq1	$⊢ y \underset{˙}{∙} B = y \underset{˙}{\cdot} B \to (y \underset{˙}{∙} B) +_{W} B = (y \underset{˙}{\cdot} B) +_{W} B$
26		clmgrp	$⊢ W \in CMod \to W \in Grp$
27	26	grpmndd	$⊢ W \in CMod \to W \in Mnd$
28	27	ad2antrr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to W \in Mnd$
29		simpr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to y \in ℕ_{0}$
30		simplr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to B \in V$
31		eqid	$⊢ +_{W} = +_{W}$
32	1 2 31	mulgnn0p1	$⊢ (W \in Mnd \land y \in ℕ_{0} \land B \in V) \to (y + 1) \underset{˙}{∙} B = (y \underset{˙}{∙} B) +_{W} B$
33	28 29 30 32	syl3anc	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{∙} B = (y \underset{˙}{∙} B) +_{W} B$
34		simpll	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to W \in CMod$
35		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
36	22 35	clmzss	$⊢ W \in CMod \to ℤ \subseteq {Base}_{Scalar (W)}$
37	36	ad2antrr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to ℤ \subseteq {Base}_{Scalar (W)}$
38		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
39	38	adantl	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to y \in ℤ$
40	37 39	sseldd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to y \in {Base}_{Scalar (W)}$
41		1zzd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to 1 \in ℤ$
42	37 41	sseldd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to 1 \in {Base}_{Scalar (W)}$
43	1 22 3 35 31	clmvsdir	$⊢ (W \in CMod \land (y \in {Base}_{Scalar (W)} \land 1 \in {Base}_{Scalar (W)} \land B \in V)) \to (y + 1) \underset{˙}{\cdot} B = (y \underset{˙}{\cdot} B) +_{W} (1 \underset{˙}{\cdot} B)$
44	34 40 42 30 43	syl13anc	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{\cdot} B = (y \underset{˙}{\cdot} B) +_{W} (1 \underset{˙}{\cdot} B)$
45	1 3	clmvs1	$⊢ (W \in CMod \land B \in V) \to 1 \underset{˙}{\cdot} B = B$
46	45	adantr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to 1 \underset{˙}{\cdot} B = B$
47	46	oveq2d	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to (y \underset{˙}{\cdot} B) +_{W} (1 \underset{˙}{\cdot} B) = (y \underset{˙}{\cdot} B) +_{W} B$
48	44 47	eqtrd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{\cdot} B = (y \underset{˙}{\cdot} B) +_{W} B$
49	33 48	eqeq12d	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to ((y + 1) \underset{˙}{∙} B = (y + 1) \underset{˙}{\cdot} B \leftrightarrow (y \underset{˙}{∙} B) +_{W} B = (y \underset{˙}{\cdot} B) +_{W} B)$
50	25 49	imbitrrid	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to (y \underset{˙}{∙} B = y \underset{˙}{\cdot} B \to (y + 1) \underset{˙}{∙} B = (y + 1) \underset{˙}{\cdot} B)$
51	50	ex	$⊢ (W \in CMod \land B \in V) \to (y \in ℕ_{0} \to (y \underset{˙}{∙} B = y \underset{˙}{\cdot} B \to (y + 1) \underset{˙}{∙} B = (y + 1) \underset{˙}{\cdot} B))$
52		fveq2	$⊢ y \underset{˙}{∙} B = y \underset{˙}{\cdot} B \to {inv}_{g} (W) (y \underset{˙}{∙} B) = {inv}_{g} (W) (y \underset{˙}{\cdot} B)$
53	26	ad2antrr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to W \in Grp$
54		nnz	$⊢ y \in ℕ \to y \in ℤ$
55	54	adantl	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to y \in ℤ$
56		simplr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to B \in V$
57		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
58	1 2 57	mulgneg	$⊢ (W \in Grp \land y \in ℤ \land B \in V) \to (- y) \underset{˙}{∙} B = {inv}_{g} (W) (y \underset{˙}{∙} B)$
59	53 55 56 58	syl3anc	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to (- y) \underset{˙}{∙} B = {inv}_{g} (W) (y \underset{˙}{∙} B)$
60		simpll	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to W \in CMod$
61	36	ad2antrr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to ℤ \subseteq {Base}_{Scalar (W)}$
62	61 55	sseldd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to y \in {Base}_{Scalar (W)}$
63	1 22 3 57 35 60 56 62	clmvsneg	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to {inv}_{g} (W) (y \underset{˙}{\cdot} B) = (- y) \underset{˙}{\cdot} B$
64	63	eqcomd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to (- y) \underset{˙}{\cdot} B = {inv}_{g} (W) (y \underset{˙}{\cdot} B)$
65	59 64	eqeq12d	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to ((- y) \underset{˙}{∙} B = (- y) \underset{˙}{\cdot} B \leftrightarrow {inv}_{g} (W) (y \underset{˙}{∙} B) = {inv}_{g} (W) (y \underset{˙}{\cdot} B))$
66	52 65	imbitrrid	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to (y \underset{˙}{∙} B = y \underset{˙}{\cdot} B \to (- y) \underset{˙}{∙} B = (- y) \underset{˙}{\cdot} B)$
67	66	ex	$⊢ (W \in CMod \land B \in V) \to (y \in ℕ \to (y \underset{˙}{∙} B = y \underset{˙}{\cdot} B \to (- y) \underset{˙}{∙} B = (- y) \underset{˙}{\cdot} B))$
68	6 9 12 15 18 24 51 67	zindd	$⊢ (W \in CMod \land B \in V) \to (A \in ℤ \to A \underset{˙}{∙} B = A \underset{˙}{\cdot} B)$
69	68	3impia	$⊢ (W \in CMod \land B \in V \land A \in ℤ) \to A \underset{˙}{∙} B = A \underset{˙}{\cdot} B$
70	69	3com23	$⊢ (W \in CMod \land A \in ℤ \land B \in V) \to A \underset{˙}{∙} B = A \underset{˙}{\cdot} B$

Metamath Proof Explorer

Theorem clmmulg

Proof