dvalveclem

Description: Lemma for dvalvec . (Contributed by NM, 11-Oct-2013) (Proof shortened by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dvalvec.h	$⊢ H = LHyp (K)$
	dvalvec.v	$⊢ U = DVecA (K) (W)$
	dvalveclem.t	$⊢ T = LTrn (K) (W)$
	dvalveclem.a	$⊢ \underset{˙}{+} = +_{U}$
	dvalveclem.e	$⊢ E = TEndo (K) (W)$
	dvalveclem.d	$⊢ D = Scalar (U)$
	dvalveclem.b	$⊢ B = {Base}_{K}$
	dvalveclem.p	$⊢ \underset{˙}{⨣} = +_{D}$
	dvalveclem.m	$⊢ \underset{˙}{\times} = \cdot_{D}$
	dvalveclem.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
Assertion	dvalveclem	$⊢ (K \in HL \land W \in H) \to U \in LVec$

Proof

Step	Hyp	Ref	Expression
1		dvalvec.h	$⊢ H = LHyp (K)$
2		dvalvec.v	$⊢ U = DVecA (K) (W)$
3		dvalveclem.t	$⊢ T = LTrn (K) (W)$
4		dvalveclem.a	$⊢ \underset{˙}{+} = +_{U}$
5		dvalveclem.e	$⊢ E = TEndo (K) (W)$
6		dvalveclem.d	$⊢ D = Scalar (U)$
7		dvalveclem.b	$⊢ B = {Base}_{K}$
8		dvalveclem.p	$⊢ \underset{˙}{⨣} = +_{D}$
9		dvalveclem.m	$⊢ \underset{˙}{\times} = \cdot_{D}$
10		dvalveclem.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
11		eqid	$⊢ {Base}_{U} = {Base}_{U}$
12	1 3 2 11	dvavbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = T$
13	12	eqcomd	$⊢ (K \in HL \land W \in H) \to T = {Base}_{U}$
14	4	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{+} = +_{U}$
15	6	a1i	$⊢ (K \in HL \land W \in H) \to D = Scalar (U)$
16	10	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{\cdot} = \cdot_{U}$
17		eqid	$⊢ {Base}_{D} = {Base}_{D}$
18	1 5 2 6 17	dvabase	$⊢ (K \in HL \land W \in H) \to {Base}_{D} = E$
19	18	eqcomd	$⊢ (K \in HL \land W \in H) \to E = {Base}_{D}$
20	8	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⨣} = +_{D}$
21	9	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{\times} = \cdot_{D}$
22	1 3 5	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$
23	22 19	eleqtrd	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in {Base}_{D}$
24		eqid	$⊢ (f \in T ⟼ {I ↾}_{B}) = (f \in T ⟼ {I ↾}_{B})$
25	7 1 3 5 24	tendo1ne0	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \neq (f \in T ⟼ {I ↾}_{B})$
26		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
27	1 26 2 6	dvasca	$⊢ (K \in HL \land W \in H) \to D = EDRing (K) (W)$
28	27	fveq2d	$⊢ (K \in HL \land W \in H) \to 0_{D} = 0_{EDRing (K) (W)}$
29		eqid	$⊢ 0_{EDRing (K) (W)} = 0_{EDRing (K) (W)}$
30	7 1 3 26 24 29	erng0g	$⊢ (K \in HL \land W \in H) \to 0_{EDRing (K) (W)} = (f \in T ⟼ {I ↾}_{B})$
31	28 30	eqtrd	$⊢ (K \in HL \land W \in H) \to 0_{D} = (f \in T ⟼ {I ↾}_{B})$
32	25 31	neeqtrrd	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \neq 0_{D}$
33	22 22	jca	$⊢ (K \in HL \land W \in H) \to ({I ↾}_{T} \in E \land {I ↾}_{T} \in E)$
34	1 3 5 2 6 9	dvamulr	$⊢ ((K \in HL \land W \in H) \land ({I ↾}_{T} \in E \land {I ↾}_{T} \in E)) \to ({I ↾}_{T}) \underset{˙}{\times} ({I ↾}_{T}) = ({I ↾}_{T}) \circ ({I ↾}_{T})$
35	33 34	mpdan	$⊢ (K \in HL \land W \in H) \to ({I ↾}_{T}) \underset{˙}{\times} ({I ↾}_{T}) = ({I ↾}_{T}) \circ ({I ↾}_{T})$
36		f1oi	$⊢ ({I ↾}_{T}) : T \underset{1-1 onto}{⟶} T$
37		f1of	$⊢ ({I ↾}_{T}) : T \underset{1-1 onto}{⟶} T \to ({I ↾}_{T}) : T ⟶ T$
38		fcoi2	$⊢ ({I ↾}_{T}) : T ⟶ T \to ({I ↾}_{T}) \circ ({I ↾}_{T}) = {I ↾}_{T}$
39	36 37 38	mp2b	$⊢ ({I ↾}_{T}) \circ ({I ↾}_{T}) = {I ↾}_{T}$
40	35 39	eqtrdi	$⊢ (K \in HL \land W \in H) \to ({I ↾}_{T}) \underset{˙}{\times} ({I ↾}_{T}) = {I ↾}_{T}$
41	23 32 40	3jca	$⊢ (K \in HL \land W \in H) \to ({I ↾}_{T} \in {Base}_{D} \land {I ↾}_{T} \neq 0_{D} \land ({I ↾}_{T}) \underset{˙}{\times} ({I ↾}_{T}) = {I ↾}_{T})$
42	1 26	erngdv	$⊢ (K \in HL \land W \in H) \to EDRing (K) (W) \in DivRing$
43	27 42	eqeltrd	$⊢ (K \in HL \land W \in H) \to D \in DivRing$
44		eqid	$⊢ 0_{D} = 0_{D}$
45		eqid	$⊢ 1_{D} = 1_{D}$
46	17 9 44 45	drngid2	$⊢ D \in DivRing \to (({I ↾}_{T} \in {Base}_{D} \land {I ↾}_{T} \neq 0_{D} \land ({I ↾}_{T}) \underset{˙}{\times} ({I ↾}_{T}) = {I ↾}_{T}) \leftrightarrow 1_{D} = {I ↾}_{T})$
47	43 46	syl	$⊢ (K \in HL \land W \in H) \to (({I ↾}_{T} \in {Base}_{D} \land {I ↾}_{T} \neq 0_{D} \land ({I ↾}_{T}) \underset{˙}{\times} ({I ↾}_{T}) = {I ↾}_{T}) \leftrightarrow 1_{D} = {I ↾}_{T})$
48	41 47	mpbid	$⊢ (K \in HL \land W \in H) \to 1_{D} = {I ↾}_{T}$
49	48	eqcomd	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} = 1_{D}$
50		drngring	$⊢ D \in DivRing \to D \in Ring$
51	43 50	syl	$⊢ (K \in HL \land W \in H) \to D \in Ring$
52	1 2	dvaabl	$⊢ (K \in HL \land W \in H) \to U \in Abel$
53		ablgrp	$⊢ U \in Abel \to U \in Grp$
54	52 53	syl	$⊢ (K \in HL \land W \in H) \to U \in Grp$
55	1 3 5 2 10	dvavsca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T)) \to s \underset{˙}{\cdot} t = s (t)$
56	55	3impb	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in T) \to s \underset{˙}{\cdot} t = s (t)$
57	1 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in T) \to s (t) \in T$
58	56 57	eqeltrd	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in T) \to s \underset{˙}{\cdot} t \in T$
59	1 3 5	tendospdi1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s (t \circ f) = s (t) \circ s (f)$
60		simpr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s \in E$
61	1 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land t \in T \land f \in T) \to t \circ f \in T$
62	61	3adant3r1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to t \circ f \in T$
63	60 62	jca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to (s \in E \land t \circ f \in T)$
64	1 3 5 2 10	dvavsca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \circ f \in T)) \to s \underset{˙}{\cdot} (t \circ f) = s (t \circ f)$
65	63 64	syldan	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s \underset{˙}{\cdot} (t \circ f) = s (t \circ f)$
66	57	3adant3r3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s (t) \in T$
67	1 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in E \land f \in T) \to s (f) \in T$
68	67	3adant3r2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s (f) \in T$
69	66 68	jca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to (s (t) \in T \land s (f) \in T)$
70	1 3 2 4	dvavadd	$⊢ ((K \in HL \land W \in H) \land (s (t) \in T \land s (f) \in T)) \to s (t) \underset{˙}{+} s (f) = s (t) \circ s (f)$
71	69 70	syldan	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s (t) \underset{˙}{+} s (f) = s (t) \circ s (f)$
72	59 65 71	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s \underset{˙}{\cdot} (t \circ f) = s (t) \underset{˙}{+} s (f)$
73	1 3 2 4	dvavadd	$⊢ ((K \in HL \land W \in H) \land (t \in T \land f \in T)) \to t \underset{˙}{+} f = t \circ f$
74	73	3adantr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to t \underset{˙}{+} f = t \circ f$
75	74	oveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s \underset{˙}{\cdot} (t \underset{˙}{+} f) = s \underset{˙}{\cdot} (t \circ f)$
76	55	3adantr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s \underset{˙}{\cdot} t = s (t)$
77	1 3 5 2 10	dvavsca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land f \in T)) \to s \underset{˙}{\cdot} f = s (f)$
78	77	3adantr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s \underset{˙}{\cdot} f = s (f)$
79	76 78	oveq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to (s \underset{˙}{\cdot} t) \underset{˙}{+} (s \underset{˙}{\cdot} f) = s (t) \underset{˙}{+} s (f)$
80	72 75 79	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in T \land f \in T)) \to s \underset{˙}{\cdot} (t \underset{˙}{+} f) = (s \underset{˙}{\cdot} t) \underset{˙}{+} (s \underset{˙}{\cdot} f)$
81	1 3 5 2 6 8	dvaplusgv	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \underset{˙}{⨣} t) (f) = s (f) \circ t (f)$
82	1 3 5 2 6 8	dvafplusg	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⨣} = (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f)))$
83	82	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to \underset{˙}{⨣} = (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f)))$
84	83	oveqd	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \underset{˙}{⨣} t = s (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f))) t$
85		eqid	$⊢ (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f))) = (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f)))$
86	1 3 5 85	tendoplcl	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f))) t \in E$
87	84 86	eqeltrd	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \underset{˙}{⨣} t \in E$
88	87	3adant3r3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s \underset{˙}{⨣} t \in E$
89		simpr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to f \in T$
90	88 89	jca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \underset{˙}{⨣} t \in E \land f \in T)$
91	1 3 5 2 10	dvavsca	$⊢ ((K \in HL \land W \in H) \land (s \underset{˙}{⨣} t \in E \land f \in T)) \to (s \underset{˙}{⨣} t) \underset{˙}{\cdot} f = (s \underset{˙}{⨣} t) (f)$
92	90 91	syldan	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \underset{˙}{⨣} t) \underset{˙}{\cdot} f = (s \underset{˙}{⨣} t) (f)$
93	77	3adantr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s \underset{˙}{\cdot} f = s (f)$
94	1 3 5 2 10	dvavsca	$⊢ ((K \in HL \land W \in H) \land (t \in E \land f \in T)) \to t \underset{˙}{\cdot} f = t (f)$
95	94	3adantr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to t \underset{˙}{\cdot} f = t (f)$
96	93 95	oveq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \underset{˙}{\cdot} f) \underset{˙}{+} (t \underset{˙}{\cdot} f) = s (f) \underset{˙}{+} t (f)$
97	67	3adant3r2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s (f) \in T$
98	1 3 5	tendospcl	$⊢ ((K \in HL \land W \in H) \land t \in E \land f \in T) \to t (f) \in T$
99	98	3adant3r1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to t (f) \in T$
100	97 99	jca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s (f) \in T \land t (f) \in T)$
101	1 3 2 4	dvavadd	$⊢ ((K \in HL \land W \in H) \land (s (f) \in T \land t (f) \in T)) \to s (f) \underset{˙}{+} t (f) = s (f) \circ t (f)$
102	100 101	syldan	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s (f) \underset{˙}{+} t (f) = s (f) \circ t (f)$
103	96 102	eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \underset{˙}{\cdot} f) \underset{˙}{+} (t \underset{˙}{\cdot} f) = s (f) \circ t (f)$
104	81 92 103	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \underset{˙}{⨣} t) \underset{˙}{\cdot} f = (s \underset{˙}{\cdot} f) \underset{˙}{+} (t \underset{˙}{\cdot} f)$
105	1 3 5	tendospass	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \circ t) (f) = s (t (f))$
106	1 5	tendococl	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \circ t \in E$
107	106	3adant3r3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s \circ t \in E$
108	107 89	jca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \circ t \in E \land f \in T)$
109	1 3 5 2 10	dvavsca	$⊢ ((K \in HL \land W \in H) \land (s \circ t \in E \land f \in T)) \to (s \circ t) \underset{˙}{\cdot} f = (s \circ t) (f)$
110	108 109	syldan	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \circ t) \underset{˙}{\cdot} f = (s \circ t) (f)$
111		simpr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s \in E$
112	111 99	jca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \in E \land t (f) \in T)$
113	1 3 5 2 10	dvavsca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t (f) \in T)) \to s \underset{˙}{\cdot} t (f) = s (t (f))$
114	112 113	syldan	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s \underset{˙}{\cdot} t (f) = s (t (f))$
115	105 110 114	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \circ t) \underset{˙}{\cdot} f = s \underset{˙}{\cdot} t (f)$
116	1 3 5 2 6 9	dvamulr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E)) \to s \underset{˙}{\times} t = s \circ t$
117	116	3adantr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s \underset{˙}{\times} t = s \circ t$
118	117	oveq1d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \underset{˙}{\times} t) \underset{˙}{\cdot} f = (s \circ t) \underset{˙}{\cdot} f$
119	95	oveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to s \underset{˙}{\cdot} (t \underset{˙}{\cdot} f) = s \underset{˙}{\cdot} t (f)$
120	115 118 119	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in T)) \to (s \underset{˙}{\times} t) \underset{˙}{\cdot} f = s \underset{˙}{\cdot} (t \underset{˙}{\cdot} f)$
121	22	anim1i	$⊢ ((K \in HL \land W \in H) \land s \in T) \to ({I ↾}_{T} \in E \land s \in T)$
122	1 3 5 2 10	dvavsca	$⊢ ((K \in HL \land W \in H) \land ({I ↾}_{T} \in E \land s \in T)) \to ({I ↾}_{T}) \underset{˙}{\cdot} s = ({I ↾}_{T}) (s)$
123	121 122	syldan	$⊢ ((K \in HL \land W \in H) \land s \in T) \to ({I ↾}_{T}) \underset{˙}{\cdot} s = ({I ↾}_{T}) (s)$
124		fvresi	$⊢ s \in T \to ({I ↾}_{T}) (s) = s$
125	124	adantl	$⊢ ((K \in HL \land W \in H) \land s \in T) \to ({I ↾}_{T}) (s) = s$
126	123 125	eqtrd	$⊢ ((K \in HL \land W \in H) \land s \in T) \to ({I ↾}_{T}) \underset{˙}{\cdot} s = s$
127	13 14 15 16 19 20 21 49 51 54 58 80 104 120 126	islmodd	$⊢ (K \in HL \land W \in H) \to U \in LMod$
128	6	islvec	$⊢ U \in LVec \leftrightarrow (U \in LMod \land D \in DivRing)$
129	127 43 128	sylanbrc	$⊢ (K \in HL \land W \in H) \to U \in LVec$

Metamath Proof Explorer

Theorem dvalveclem

Proof