dvhlveclem

Description: Lemma for dvhlvec . TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does ph -> method shorten proof? (Contributed by NM, 22-Oct-2013) (Proof shortened by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	dvhgrp.b	$⊢ B = {Base}_{K}$
	dvhgrp.h	$⊢ H = LHyp (K)$
	dvhgrp.t	$⊢ T = LTrn (K) (W)$
	dvhgrp.e	$⊢ E = TEndo (K) (W)$
	dvhgrp.u	$⊢ U = DVecH (K) (W)$
	dvhgrp.d	$⊢ D = Scalar (U)$
	dvhgrp.p	$⊢ \underset{˙}{⨣} = +_{D}$
	dvhgrp.a	$⊢ \underset{˙}{+} = +_{U}$
	dvhgrp.o	$⊢ \underset{˙}{0} = 0_{D}$
	dvhgrp.i	$⊢ I = {inv}_{g} (D)$
	dvhlvec.m	$⊢ \underset{˙}{\times} = \cdot_{D}$
	dvhlvec.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
Assertion	dvhlveclem	$⊢ (K \in HL \land W \in H) \to U \in LVec$

Proof

Step	Hyp	Ref	Expression
1		dvhgrp.b	$⊢ B = {Base}_{K}$
2		dvhgrp.h	$⊢ H = LHyp (K)$
3		dvhgrp.t	$⊢ T = LTrn (K) (W)$
4		dvhgrp.e	$⊢ E = TEndo (K) (W)$
5		dvhgrp.u	$⊢ U = DVecH (K) (W)$
6		dvhgrp.d	$⊢ D = Scalar (U)$
7		dvhgrp.p	$⊢ \underset{˙}{⨣} = +_{D}$
8		dvhgrp.a	$⊢ \underset{˙}{+} = +_{U}$
9		dvhgrp.o	$⊢ \underset{˙}{0} = 0_{D}$
10		dvhgrp.i	$⊢ I = {inv}_{g} (D)$
11		dvhlvec.m	$⊢ \underset{˙}{\times} = \cdot_{D}$
12		dvhlvec.s	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
13		eqid	$⊢ {Base}_{U} = {Base}_{U}$
14	2 3 4 5 13	dvhvbase	$⊢ (K \in HL \land W \in H) \to {Base}_{U} = T \times E$
15	14	eqcomd	$⊢ (K \in HL \land W \in H) \to T \times E = {Base}_{U}$
16	8	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{+} = +_{U}$
17	6	a1i	$⊢ (K \in HL \land W \in H) \to D = Scalar (U)$
18	12	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{\cdot} = \cdot_{U}$
19		eqid	$⊢ {Base}_{D} = {Base}_{D}$
20	2 4 5 6 19	dvhbase	$⊢ (K \in HL \land W \in H) \to {Base}_{D} = E$
21	20	eqcomd	$⊢ (K \in HL \land W \in H) \to E = {Base}_{D}$
22	7	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⨣} = +_{D}$
23	11	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{\times} = \cdot_{D}$
24		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
25	2 24 5 6	dvhsca	$⊢ (K \in HL \land W \in H) \to D = EDRing (K) (W)$
26	25	fveq2d	$⊢ (K \in HL \land W \in H) \to 1_{D} = 1_{EDRing (K) (W)}$
27		eqid	$⊢ 1_{EDRing (K) (W)} = 1_{EDRing (K) (W)}$
28	2 3 24 27	erng1r	$⊢ (K \in HL \land W \in H) \to 1_{EDRing (K) (W)} = {I ↾}_{T}$
29	26 28	eqtr2d	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} = 1_{D}$
30	2 24	erngdv	$⊢ (K \in HL \land W \in H) \to EDRing (K) (W) \in DivRing$
31	25 30	eqeltrd	$⊢ (K \in HL \land W \in H) \to D \in DivRing$
32		drngring	$⊢ D \in DivRing \to D \in Ring$
33	31 32	syl	$⊢ (K \in HL \land W \in H) \to D \in Ring$
34	1 2 3 4 5 6 7 8 9 10	dvhgrp	$⊢ (K \in HL \land W \in H) \to U \in Grp$
35	2 3 4 5 12	dvhvscacl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E))) \to s \underset{˙}{\cdot} t \in (T \times E)$
36	35	3impb	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in (T \times E)) \to s \underset{˙}{\cdot} t \in (T \times E)$
37		simpl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to (K \in HL \land W \in H)$
38		simpr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \in E$
39		simpr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to t \in (T \times E)$
40		xp1st	$⊢ t \in (T \times E) \to 1^{st} (t) \in T$
41	39 40	syl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (t) \in T$
42		simpr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to f \in (T \times E)$
43		xp1st	$⊢ f \in (T \times E) \to 1^{st} (f) \in T$
44	42 43	syl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (f) \in T$
45	2 3 4	tendospdi1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land 1^{st} (t) \in T \land 1^{st} (f) \in T)) \to s (1^{st} (t) \circ 1^{st} (f)) = s (1^{st} (t)) \circ s (1^{st} (f))$
46	37 38 41 44 45	syl13anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s (1^{st} (t) \circ 1^{st} (f)) = s (1^{st} (t)) \circ s (1^{st} (f))$
47	2 3 4 5 6 8 7	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (t \in (T \times E) \land f \in (T \times E))) \to t \underset{˙}{+} f = ⟨1^{st} (t) \circ 1^{st} (f), 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)⟩$
48	47	3adantr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to t \underset{˙}{+} f = ⟨1^{st} (t) \circ 1^{st} (f), 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)⟩$
49	48	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (t \underset{˙}{+} f) = 1^{st} (⟨1^{st} (t) \circ 1^{st} (f), 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)⟩)$
50		fvex	$⊢ 1^{st} (t) \in V$
51		fvex	$⊢ 1^{st} (f) \in V$
52	50 51	coex	$⊢ 1^{st} (t) \circ 1^{st} (f) \in V$
53		ovex	$⊢ 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f) \in V$
54	52 53	op1st	$⊢ 1^{st} (⟨1^{st} (t) \circ 1^{st} (f), 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)⟩) = 1^{st} (t) \circ 1^{st} (f)$
55	49 54	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (t \underset{˙}{+} f) = 1^{st} (t) \circ 1^{st} (f)$
56	55	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s (1^{st} (t \underset{˙}{+} f)) = s (1^{st} (t) \circ 1^{st} (f))$
57	2 3 4 5 12	dvhvsca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E))) \to s \underset{˙}{\cdot} t = ⟨s (1^{st} (t)), s \circ 2^{nd} (t)⟩$
58	57	3adantr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\cdot} t = ⟨s (1^{st} (t)), s \circ 2^{nd} (t)⟩$
59	58	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (s \underset{˙}{\cdot} t) = 1^{st} (⟨s (1^{st} (t)), s \circ 2^{nd} (t)⟩)$
60		fvex	$⊢ s (1^{st} (t)) \in V$
61		vex	$⊢ s \in V$
62		fvex	$⊢ 2^{nd} (t) \in V$
63	61 62	coex	$⊢ s \circ 2^{nd} (t) \in V$
64	60 63	op1st	$⊢ 1^{st} (⟨s (1^{st} (t)), s \circ 2^{nd} (t)⟩) = s (1^{st} (t))$
65	59 64	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (s \underset{˙}{\cdot} t) = s (1^{st} (t))$
66	2 3 4 5 12	dvhvsca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land f \in (T \times E))) \to s \underset{˙}{\cdot} f = ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩$
67	66	3adantr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\cdot} f = ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩$
68	67	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (s \underset{˙}{\cdot} f) = 1^{st} (⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
69		fvex	$⊢ s (1^{st} (f)) \in V$
70		fvex	$⊢ 2^{nd} (f) \in V$
71	61 70	coex	$⊢ s \circ 2^{nd} (f) \in V$
72	69 71	op1st	$⊢ 1^{st} (⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩) = s (1^{st} (f))$
73	68 72	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (s \underset{˙}{\cdot} f) = s (1^{st} (f))$
74	65 73	coeq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 1^{st} (s \underset{˙}{\cdot} t) \circ 1^{st} (s \underset{˙}{\cdot} f) = s (1^{st} (t)) \circ s (1^{st} (f))$
75	46 56 74	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s (1^{st} (t \underset{˙}{+} f)) = 1^{st} (s \underset{˙}{\cdot} t) \circ 1^{st} (s \underset{˙}{\cdot} f)$
76	33	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to D \in Ring$
77	21	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to E = {Base}_{D}$
78	38 77	eleqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \in {Base}_{D}$
79		xp2nd	$⊢ t \in (T \times E) \to 2^{nd} (t) \in E$
80	39 79	syl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (t) \in E$
81	80 77	eleqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (t) \in {Base}_{D}$
82		xp2nd	$⊢ f \in (T \times E) \to 2^{nd} (f) \in E$
83	42 82	syl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (f) \in E$
84	83 77	eleqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (f) \in {Base}_{D}$
85	19 7 11	ringdi	$⊢ (D \in Ring \land (s \in {Base}_{D} \land 2^{nd} (t) \in {Base}_{D} \land 2^{nd} (f) \in {Base}_{D})) \to s \underset{˙}{\times} (2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)) = (s \underset{˙}{\times} 2^{nd} (t)) \underset{˙}{⨣} (s \underset{˙}{\times} 2^{nd} (f))$
86	76 78 81 84 85	syl13anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\times} (2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)) = (s \underset{˙}{\times} 2^{nd} (t)) \underset{˙}{⨣} (s \underset{˙}{\times} 2^{nd} (f))$
87	19 7	ringacl	$⊢ (D \in Ring \land 2^{nd} (t) \in {Base}_{D} \land 2^{nd} (f) \in {Base}_{D}) \to 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f) \in {Base}_{D}$
88	76 81 84 87	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f) \in {Base}_{D}$
89	88 77	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f) \in E$
90	2 3 4 5 6 11	dvhmulr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f) \in E)) \to s \underset{˙}{\times} (2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)) = s \circ (2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f))$
91	37 38 89 90	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\times} (2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)) = s \circ (2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f))$
92	2 3 4 5 6 11	dvhmulr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land 2^{nd} (t) \in E)) \to s \underset{˙}{\times} 2^{nd} (t) = s \circ 2^{nd} (t)$
93	37 38 80 92	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\times} 2^{nd} (t) = s \circ 2^{nd} (t)$
94	2 3 4 5 6 11	dvhmulr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land 2^{nd} (f) \in E)) \to s \underset{˙}{\times} 2^{nd} (f) = s \circ 2^{nd} (f)$
95	37 38 83 94	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\times} 2^{nd} (f) = s \circ 2^{nd} (f)$
96	93 95	oveq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to (s \underset{˙}{\times} 2^{nd} (t)) \underset{˙}{⨣} (s \underset{˙}{\times} 2^{nd} (f)) = (s \circ 2^{nd} (t)) \underset{˙}{⨣} (s \circ 2^{nd} (f))$
97	86 91 96	3eqtr3d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \circ (2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)) = (s \circ 2^{nd} (t)) \underset{˙}{⨣} (s \circ 2^{nd} (f))$
98	48	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (t \underset{˙}{+} f) = 2^{nd} (⟨1^{st} (t) \circ 1^{st} (f), 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)⟩)$
99	52 53	op2nd	$⊢ 2^{nd} (⟨1^{st} (t) \circ 1^{st} (f), 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)⟩) = 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)$
100	98 99	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (t \underset{˙}{+} f) = 2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f)$
101	100	coeq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \circ 2^{nd} (t \underset{˙}{+} f) = s \circ (2^{nd} (t) \underset{˙}{⨣} 2^{nd} (f))$
102	58	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (s \underset{˙}{\cdot} t) = 2^{nd} (⟨s (1^{st} (t)), s \circ 2^{nd} (t)⟩)$
103	60 63	op2nd	$⊢ 2^{nd} (⟨s (1^{st} (t)), s \circ 2^{nd} (t)⟩) = s \circ 2^{nd} (t)$
104	102 103	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (s \underset{˙}{\cdot} t) = s \circ 2^{nd} (t)$
105	67	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (s \underset{˙}{\cdot} f) = 2^{nd} (⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
106	69 71	op2nd	$⊢ 2^{nd} (⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩) = s \circ 2^{nd} (f)$
107	105 106	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (s \underset{˙}{\cdot} f) = s \circ 2^{nd} (f)$
108	104 107	oveq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to 2^{nd} (s \underset{˙}{\cdot} t) \underset{˙}{⨣} 2^{nd} (s \underset{˙}{\cdot} f) = (s \circ 2^{nd} (t)) \underset{˙}{⨣} (s \circ 2^{nd} (f))$
109	97 101 108	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \circ 2^{nd} (t \underset{˙}{+} f) = 2^{nd} (s \underset{˙}{\cdot} t) \underset{˙}{⨣} 2^{nd} (s \underset{˙}{\cdot} f)$
110	75 109	opeq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to ⟨s (1^{st} (t \underset{˙}{+} f)), s \circ 2^{nd} (t \underset{˙}{+} f)⟩ = ⟨1^{st} (s \underset{˙}{\cdot} t) \circ 1^{st} (s \underset{˙}{\cdot} f), 2^{nd} (s \underset{˙}{\cdot} t) \underset{˙}{⨣} 2^{nd} (s \underset{˙}{\cdot} f)⟩$
111	2 3 4 5 6 7 8	dvhvaddcl	$⊢ ((K \in HL \land W \in H) \land (t \in (T \times E) \land f \in (T \times E))) \to t \underset{˙}{+} f \in (T \times E)$
112	111	3adantr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to t \underset{˙}{+} f \in (T \times E)$
113	2 3 4 5 12	dvhvsca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \underset{˙}{+} f \in (T \times E))) \to s \underset{˙}{\cdot} (t \underset{˙}{+} f) = ⟨s (1^{st} (t \underset{˙}{+} f)), s \circ 2^{nd} (t \underset{˙}{+} f)⟩$
114	37 38 112 113	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\cdot} (t \underset{˙}{+} f) = ⟨s (1^{st} (t \underset{˙}{+} f)), s \circ 2^{nd} (t \underset{˙}{+} f)⟩$
115	35	3adantr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\cdot} t \in (T \times E)$
116	2 3 4 5 12	dvhvscacl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land f \in (T \times E))) \to s \underset{˙}{\cdot} f \in (T \times E)$
117	116	3adantr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\cdot} f \in (T \times E)$
118	2 3 4 5 6 8 7	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (s \underset{˙}{\cdot} t \in (T \times E) \land s \underset{˙}{\cdot} f \in (T \times E))) \to (s \underset{˙}{\cdot} t) \underset{˙}{+} (s \underset{˙}{\cdot} f) = ⟨1^{st} (s \underset{˙}{\cdot} t) \circ 1^{st} (s \underset{˙}{\cdot} f), 2^{nd} (s \underset{˙}{\cdot} t) \underset{˙}{⨣} 2^{nd} (s \underset{˙}{\cdot} f)⟩$
119	37 115 117 118	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to (s \underset{˙}{\cdot} t) \underset{˙}{+} (s \underset{˙}{\cdot} f) = ⟨1^{st} (s \underset{˙}{\cdot} t) \circ 1^{st} (s \underset{˙}{\cdot} f), 2^{nd} (s \underset{˙}{\cdot} t) \underset{˙}{⨣} 2^{nd} (s \underset{˙}{\cdot} f)⟩$
120	110 114 119	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in (T \times E) \land f \in (T \times E))) \to s \underset{˙}{\cdot} (t \underset{˙}{+} f) = (s \underset{˙}{\cdot} t) \underset{˙}{+} (s \underset{˙}{\cdot} f)$
121		simpl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (K \in HL \land W \in H)$
122		simpr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \in E$
123		simpr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to t \in E$
124		simpr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to f \in (T \times E)$
125	124 43	syl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 1^{st} (f) \in T$
126		eqid	$⊢ +_{EDRing (K) (W)} = +_{EDRing (K) (W)}$
127	2 3 4 24 126	erngplus2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land 1^{st} (f) \in T)) \to (s +_{EDRing (K) (W)} t) (1^{st} (f)) = s (1^{st} (f)) \circ t (1^{st} (f))$
128	121 122 123 125 127	syl13anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s +_{EDRing (K) (W)} t) (1^{st} (f)) = s (1^{st} (f)) \circ t (1^{st} (f))$
129	25	fveq2d	$⊢ (K \in HL \land W \in H) \to +_{D} = +_{EDRing (K) (W)}$
130	7 129	syl5eq	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⨣} = +_{EDRing (K) (W)}$
131	130	oveqd	$⊢ (K \in HL \land W \in H) \to s \underset{˙}{⨣} t = s +_{EDRing (K) (W)} t$
132	131	fveq1d	$⊢ (K \in HL \land W \in H) \to (s \underset{˙}{⨣} t) (1^{st} (f)) = (s +_{EDRing (K) (W)} t) (1^{st} (f))$
133	132	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) (1^{st} (f)) = (s +_{EDRing (K) (W)} t) (1^{st} (f))$
134	66	3adantr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \underset{˙}{\cdot} f = ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩$
135	134	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 1^{st} (s \underset{˙}{\cdot} f) = 1^{st} (⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
136	135 72	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 1^{st} (s \underset{˙}{\cdot} f) = s (1^{st} (f))$
137	2 3 4 5 12	dvhvsca	$⊢ ((K \in HL \land W \in H) \land (t \in E \land f \in (T \times E))) \to t \underset{˙}{\cdot} f = ⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩$
138	137	3adantr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to t \underset{˙}{\cdot} f = ⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩$
139	138	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 1^{st} (t \underset{˙}{\cdot} f) = 1^{st} (⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩)$
140		fvex	$⊢ t (1^{st} (f)) \in V$
141		vex	$⊢ t \in V$
142	141 70	coex	$⊢ t \circ 2^{nd} (f) \in V$
143	140 142	op1st	$⊢ 1^{st} (⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩) = t (1^{st} (f))$
144	139 143	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 1^{st} (t \underset{˙}{\cdot} f) = t (1^{st} (f))$
145	136 144	coeq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 1^{st} (s \underset{˙}{\cdot} f) \circ 1^{st} (t \underset{˙}{\cdot} f) = s (1^{st} (f)) \circ t (1^{st} (f))$
146	128 133 145	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) (1^{st} (f)) = 1^{st} (s \underset{˙}{\cdot} f) \circ 1^{st} (t \underset{˙}{\cdot} f)$
147	33	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to D \in Ring$
148	21	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to E = {Base}_{D}$
149	122 148	eleqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \in {Base}_{D}$
150	123 148	eleqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to t \in {Base}_{D}$
151	124 82	syl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 2^{nd} (f) \in E$
152	151 148	eleqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 2^{nd} (f) \in {Base}_{D}$
153	19 7 11	ringdir	$⊢ (D \in Ring \land (s \in {Base}_{D} \land t \in {Base}_{D} \land 2^{nd} (f) \in {Base}_{D})) \to (s \underset{˙}{⨣} t) \underset{˙}{\times} 2^{nd} (f) = (s \underset{˙}{\times} 2^{nd} (f)) \underset{˙}{⨣} (t \underset{˙}{\times} 2^{nd} (f))$
154	147 149 150 152 153	syl13anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) \underset{˙}{\times} 2^{nd} (f) = (s \underset{˙}{\times} 2^{nd} (f)) \underset{˙}{⨣} (t \underset{˙}{\times} 2^{nd} (f))$
155	19 7	ringacl	$⊢ (D \in Ring \land s \in {Base}_{D} \land t \in {Base}_{D}) \to s \underset{˙}{⨣} t \in {Base}_{D}$
156	147 149 150 155	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \underset{˙}{⨣} t \in {Base}_{D}$
157	156 148	eleqtrrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \underset{˙}{⨣} t \in E$
158	2 3 4 5 6 11	dvhmulr	$⊢ ((K \in HL \land W \in H) \land (s \underset{˙}{⨣} t \in E \land 2^{nd} (f) \in E)) \to (s \underset{˙}{⨣} t) \underset{˙}{\times} 2^{nd} (f) = (s \underset{˙}{⨣} t) \circ 2^{nd} (f)$
159	121 157 151 158	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) \underset{˙}{\times} 2^{nd} (f) = (s \underset{˙}{⨣} t) \circ 2^{nd} (f)$
160	121 122 151 94	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \underset{˙}{\times} 2^{nd} (f) = s \circ 2^{nd} (f)$
161	2 3 4 5 6 11	dvhmulr	$⊢ ((K \in HL \land W \in H) \land (t \in E \land 2^{nd} (f) \in E)) \to t \underset{˙}{\times} 2^{nd} (f) = t \circ 2^{nd} (f)$
162	121 123 151 161	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to t \underset{˙}{\times} 2^{nd} (f) = t \circ 2^{nd} (f)$
163	160 162	oveq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{\times} 2^{nd} (f)) \underset{˙}{⨣} (t \underset{˙}{\times} 2^{nd} (f)) = (s \circ 2^{nd} (f)) \underset{˙}{⨣} (t \circ 2^{nd} (f))$
164	154 159 163	3eqtr3d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) \circ 2^{nd} (f) = (s \circ 2^{nd} (f)) \underset{˙}{⨣} (t \circ 2^{nd} (f))$
165	134	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 2^{nd} (s \underset{˙}{\cdot} f) = 2^{nd} (⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)$
166	165 106	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 2^{nd} (s \underset{˙}{\cdot} f) = s \circ 2^{nd} (f)$
167	138	fveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 2^{nd} (t \underset{˙}{\cdot} f) = 2^{nd} (⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩)$
168	140 142	op2nd	$⊢ 2^{nd} (⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩) = t \circ 2^{nd} (f)$
169	167 168	eqtrdi	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 2^{nd} (t \underset{˙}{\cdot} f) = t \circ 2^{nd} (f)$
170	166 169	oveq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to 2^{nd} (s \underset{˙}{\cdot} f) \underset{˙}{⨣} 2^{nd} (t \underset{˙}{\cdot} f) = (s \circ 2^{nd} (f)) \underset{˙}{⨣} (t \circ 2^{nd} (f))$
171	164 170	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) \circ 2^{nd} (f) = 2^{nd} (s \underset{˙}{\cdot} f) \underset{˙}{⨣} 2^{nd} (t \underset{˙}{\cdot} f)$
172	146 171	opeq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to ⟨(s \underset{˙}{⨣} t) (1^{st} (f)), (s \underset{˙}{⨣} t) \circ 2^{nd} (f)⟩ = ⟨1^{st} (s \underset{˙}{\cdot} f) \circ 1^{st} (t \underset{˙}{\cdot} f), 2^{nd} (s \underset{˙}{\cdot} f) \underset{˙}{⨣} 2^{nd} (t \underset{˙}{\cdot} f)⟩$
173	2 3 4 5 12	dvhvsca	$⊢ ((K \in HL \land W \in H) \land (s \underset{˙}{⨣} t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) \underset{˙}{\cdot} f = ⟨(s \underset{˙}{⨣} t) (1^{st} (f)), (s \underset{˙}{⨣} t) \circ 2^{nd} (f)⟩$
174	121 157 124 173	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) \underset{˙}{\cdot} f = ⟨(s \underset{˙}{⨣} t) (1^{st} (f)), (s \underset{˙}{⨣} t) \circ 2^{nd} (f)⟩$
175	116	3adantr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \underset{˙}{\cdot} f \in (T \times E)$
176	2 3 4 5 12	dvhvscacl	$⊢ ((K \in HL \land W \in H) \land (t \in E \land f \in (T \times E))) \to t \underset{˙}{\cdot} f \in (T \times E)$
177	176	3adantr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to t \underset{˙}{\cdot} f \in (T \times E)$
178	2 3 4 5 6 8 7	dvhvadd	$⊢ ((K \in HL \land W \in H) \land (s \underset{˙}{\cdot} f \in (T \times E) \land t \underset{˙}{\cdot} f \in (T \times E))) \to (s \underset{˙}{\cdot} f) \underset{˙}{+} (t \underset{˙}{\cdot} f) = ⟨1^{st} (s \underset{˙}{\cdot} f) \circ 1^{st} (t \underset{˙}{\cdot} f), 2^{nd} (s \underset{˙}{\cdot} f) \underset{˙}{⨣} 2^{nd} (t \underset{˙}{\cdot} f)⟩$
179	121 175 177 178	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{\cdot} f) \underset{˙}{+} (t \underset{˙}{\cdot} f) = ⟨1^{st} (s \underset{˙}{\cdot} f) \circ 1^{st} (t \underset{˙}{\cdot} f), 2^{nd} (s \underset{˙}{\cdot} f) \underset{˙}{⨣} 2^{nd} (t \underset{˙}{\cdot} f)⟩$
180	172 174 179	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{⨣} t) \underset{˙}{\cdot} f = (s \underset{˙}{\cdot} f) \underset{˙}{+} (t \underset{˙}{\cdot} f)$
181	2 3 4	tendocoval	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E) \land 1^{st} (f) \in T) \to (s \circ t) (1^{st} (f)) = s (t (1^{st} (f)))$
182	121 122 123 125 181	syl121anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \circ t) (1^{st} (f)) = s (t (1^{st} (f)))$
183		coass	$⊢ (s \circ t) \circ 2^{nd} (f) = s \circ (t \circ 2^{nd} (f))$
184	183	a1i	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \circ t) \circ 2^{nd} (f) = s \circ (t \circ 2^{nd} (f))$
185	182 184	opeq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to ⟨(s \circ t) (1^{st} (f)), (s \circ t) \circ 2^{nd} (f)⟩ = ⟨s (t (1^{st} (f))), s \circ (t \circ 2^{nd} (f))⟩$
186	2 4	tendococl	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \circ t \in E$
187	121 122 123 186	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \circ t \in E$
188	2 3 4 5 12	dvhvsca	$⊢ ((K \in HL \land W \in H) \land (s \circ t \in E \land f \in (T \times E))) \to (s \circ t) \underset{˙}{\cdot} f = ⟨(s \circ t) (1^{st} (f)), (s \circ t) \circ 2^{nd} (f)⟩$
189	121 187 124 188	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \circ t) \underset{˙}{\cdot} f = ⟨(s \circ t) (1^{st} (f)), (s \circ t) \circ 2^{nd} (f)⟩$
190	2 3 4	tendocl	$⊢ ((K \in HL \land W \in H) \land t \in E \land 1^{st} (f) \in T) \to t (1^{st} (f)) \in T$
191	121 123 125 190	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to t (1^{st} (f)) \in T$
192	2 4	tendococl	$⊢ ((K \in HL \land W \in H) \land t \in E \land 2^{nd} (f) \in E) \to t \circ 2^{nd} (f) \in E$
193	121 123 151 192	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to t \circ 2^{nd} (f) \in E$
194	2 3 4 5 12	dvhopvsca	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t (1^{st} (f)) \in T \land t \circ 2^{nd} (f) \in E)) \to s \underset{˙}{\cdot} ⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩ = ⟨s (t (1^{st} (f))), s \circ (t \circ 2^{nd} (f))⟩$
195	121 122 191 193 194	syl13anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \underset{˙}{\cdot} ⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩ = ⟨s (t (1^{st} (f))), s \circ (t \circ 2^{nd} (f))⟩$
196	185 189 195	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \circ t) \underset{˙}{\cdot} f = s \underset{˙}{\cdot} ⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩$
197	2 3 4 5 6 11	dvhmulr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E)) \to s \underset{˙}{\times} t = s \circ t$
198	197	3adantr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \underset{˙}{\times} t = s \circ t$
199	198	oveq1d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{\times} t) \underset{˙}{\cdot} f = (s \circ t) \underset{˙}{\cdot} f$
200	138	oveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to s \underset{˙}{\cdot} (t \underset{˙}{\cdot} f) = s \underset{˙}{\cdot} ⟨t (1^{st} (f)), t \circ 2^{nd} (f)⟩$
201	196 199 200	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land f \in (T \times E))) \to (s \underset{˙}{\times} t) \underset{˙}{\cdot} f = s \underset{˙}{\cdot} (t \underset{˙}{\cdot} f)$
202		xp1st	$⊢ s \in (T \times E) \to 1^{st} (s) \in T$
203	202	adantl	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to 1^{st} (s) \in T$
204		fvresi	$⊢ 1^{st} (s) \in T \to ({I ↾}_{T}) (1^{st} (s)) = 1^{st} (s)$
205	203 204	syl	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to ({I ↾}_{T}) (1^{st} (s)) = 1^{st} (s)$
206		xp2nd	$⊢ s \in (T \times E) \to 2^{nd} (s) \in E$
207	2 3 4	tendof	$⊢ ((K \in HL \land W \in H) \land 2^{nd} (s) \in E) \to 2^{nd} (s) : T ⟶ T$
208	206 207	sylan2	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to 2^{nd} (s) : T ⟶ T$
209		fcoi2	$⊢ 2^{nd} (s) : T ⟶ T \to ({I ↾}_{T}) \circ 2^{nd} (s) = 2^{nd} (s)$
210	208 209	syl	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to ({I ↾}_{T}) \circ 2^{nd} (s) = 2^{nd} (s)$
211	205 210	opeq12d	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to ⟨({I ↾}_{T}) (1^{st} (s)), ({I ↾}_{T}) \circ 2^{nd} (s)⟩ = ⟨1^{st} (s), 2^{nd} (s)⟩$
212	2 3 4	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$
213	212	anim1i	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to ({I ↾}_{T} \in E \land s \in (T \times E))$
214	2 3 4 5 12	dvhvsca	$⊢ ((K \in HL \land W \in H) \land ({I ↾}_{T} \in E \land s \in (T \times E))) \to ({I ↾}_{T}) \underset{˙}{\cdot} s = ⟨({I ↾}_{T}) (1^{st} (s)), ({I ↾}_{T}) \circ 2^{nd} (s)⟩$
215	213 214	syldan	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to ({I ↾}_{T}) \underset{˙}{\cdot} s = ⟨({I ↾}_{T}) (1^{st} (s)), ({I ↾}_{T}) \circ 2^{nd} (s)⟩$
216		1st2nd2	$⊢ s \in (T \times E) \to s = ⟨1^{st} (s), 2^{nd} (s)⟩$
217	216	adantl	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to s = ⟨1^{st} (s), 2^{nd} (s)⟩$
218	211 215 217	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land s \in (T \times E)) \to ({I ↾}_{T}) \underset{˙}{\cdot} s = s$
219	15 16 17 18 21 22 23 29 33 34 36 120 180 201 218	islmodd	$⊢ (K \in HL \land W \in H) \to U \in LMod$
220	6	islvec	$⊢ U \in LVec \leftrightarrow (U \in LMod \land D \in DivRing)$
221	219 31 220	sylanbrc	$⊢ (K \in HL \land W \in H) \to U \in LVec$

Metamath Proof Explorer

Theorem dvhlveclem

Proof