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		grpmnd	$⊢ W \in Grp \to W \in Mnd$
28	26 27	syl	$⊢ W \in CMod \to W \in Mnd$
29	28	ad2antrr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to W \in Mnd$
30		simpr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to y \in ℕ_{0}$
31		simplr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to B \in V$
32		eqid	$⊢ +_{W} = +_{W}$
33	1 2 32	mulgnn0p1	$⊢ (W \in Mnd \land y \in ℕ_{0} \land B \in V) \to (y + 1) \underset{˙}{∙} B = (y \underset{˙}{∙} B) +_{W} B$
34	29 30 31 33	syl3anc	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{∙} B = (y \underset{˙}{∙} B) +_{W} B$
35		simpll	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to W \in CMod$
36		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
37	22 36	clmzss	$⊢ W \in CMod \to ℤ \subseteq {Base}_{Scalar (W)}$
38	37	ad2antrr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to ℤ \subseteq {Base}_{Scalar (W)}$
39		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
40	39	adantl	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to y \in ℤ$
41	38 40	sseldd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to y \in {Base}_{Scalar (W)}$
42		1zzd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to 1 \in ℤ$
43	38 42	sseldd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to 1 \in {Base}_{Scalar (W)}$
44	1 22 3 36 32	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)$
45	35 41 43 31 44	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)$
46	1 3	clmvs1	$⊢ (W \in CMod \land B \in V) \to 1 \underset{˙}{\cdot} B = B$
47	46	adantr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to 1 \underset{˙}{\cdot} B = B$
48	47	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$
49	45 48	eqtrd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ_{0}) \to (y + 1) \underset{˙}{\cdot} B = (y \underset{˙}{\cdot} B) +_{W} B$
50	34 49	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)$
51	25 50	syl5ibr	$⊢ ((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)$
52	51	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))$
53		fveq2	$⊢ y \underset{˙}{∙} B = y \underset{˙}{\cdot} B \to {inv}_{g} (W) (y \underset{˙}{∙} B) = {inv}_{g} (W) (y \underset{˙}{\cdot} B)$
54	26	ad2antrr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to W \in Grp$
55		nnz	$⊢ y \in ℕ \to y \in ℤ$
56	55	adantl	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to y \in ℤ$
57		simplr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to B \in V$
58		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
59	1 2 58	mulgneg	$⊢ (W \in Grp \land y \in ℤ \land B \in V) \to (- y) \underset{˙}{∙} B = {inv}_{g} (W) (y \underset{˙}{∙} B)$
60	54 56 57 59	syl3anc	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to (- y) \underset{˙}{∙} B = {inv}_{g} (W) (y \underset{˙}{∙} B)$
61		simpll	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to W \in CMod$
62	37	ad2antrr	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to ℤ \subseteq {Base}_{Scalar (W)}$
63	62 56	sseldd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to y \in {Base}_{Scalar (W)}$
64	1 22 3 58 36 61 57 63	clmvsneg	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to {inv}_{g} (W) (y \underset{˙}{\cdot} B) = (- y) \underset{˙}{\cdot} B$
65	64	eqcomd	$⊢ ((W \in CMod \land B \in V) \land y \in ℕ) \to (- y) \underset{˙}{\cdot} B = {inv}_{g} (W) (y \underset{˙}{\cdot} B)$
66	60 65	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))$
67	53 66	syl5ibr	$⊢ ((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)$
68	67	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))$
69	6 9 12 15 18 24 52 68	zindd	$⊢ (W \in CMod \land B \in V) \to (A \in ℤ \to A \underset{˙}{∙} B = A \underset{˙}{\cdot} B)$
70	69	3impia	$⊢ (W \in CMod \land B \in V \land A \in ℤ) \to A \underset{˙}{∙} B = A \underset{˙}{\cdot} B$
71	70	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