erngdvlem3

	Ref	Expression
Hypotheses	ernggrp.h	$⊢ H = LHyp (K)$
	ernggrp.d	$⊢ D = EDRing (K) (W)$
	erngdv.b	$⊢ B = {Base}_{K}$
	erngdv.t	$⊢ T = LTrn (K) (W)$
	erngdv.e	$⊢ E = TEndo (K) (W)$
	erngdv.p	$⊢ P = (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f)))$
	erngdv.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
	erngdv.i	$⊢ I = (a \in E ⟼ (f \in T ⟼ {a (f)}^{-1}))$
	erngrnglem.m	$⊢ \underset{˙}{+} = (a \in E, b \in E ⟼ a \circ b)$
Assertion	erngdvlem3	$⊢ (K \in HL \land W \in H) \to D \in Ring$

Proof

Step	Hyp	Ref	Expression
1		ernggrp.h	$⊢ H = LHyp (K)$
2		ernggrp.d	$⊢ D = EDRing (K) (W)$
3		erngdv.b	$⊢ B = {Base}_{K}$
4		erngdv.t	$⊢ T = LTrn (K) (W)$
5		erngdv.e	$⊢ E = TEndo (K) (W)$
6		erngdv.p	$⊢ P = (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f)))$
7		erngdv.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
8		erngdv.i	$⊢ I = (a \in E ⟼ (f \in T ⟼ {a (f)}^{-1}))$
9		erngrnglem.m	$⊢ \underset{˙}{+} = (a \in E, b \in E ⟼ a \circ b)$
10		eqid	$⊢ {Base}_{D} = {Base}_{D}$
11	1 4 5 2 10	erngbase	$⊢ (K \in HL \land W \in H) \to {Base}_{D} = E$
12	11	eqcomd	$⊢ (K \in HL \land W \in H) \to E = {Base}_{D}$
13		eqid	$⊢ +_{D} = +_{D}$
14	1 4 5 2 13	erngfplus	$⊢ (K \in HL \land W \in H) \to +_{D} = (a \in E, b \in E ⟼ (f \in T ⟼ a (f) \circ b (f)))$
15	6 14	eqtr4id	$⊢ (K \in HL \land W \in H) \to P = +_{D}$
16		eqid	$⊢ \cdot_{D} = \cdot_{D}$
17	1 4 5 2 16	erngfmul	$⊢ (K \in HL \land W \in H) \to \cdot_{D} = (a \in E, b \in E ⟼ a \circ b)$
18	9 17	eqtr4id	$⊢ (K \in HL \land W \in H) \to \underset{˙}{+} = \cdot_{D}$
19	1 2 3 4 5 6 7 8	erngdvlem1	$⊢ (K \in HL \land W \in H) \to D \in Grp$
20	18	oveqd	$⊢ (K \in HL \land W \in H) \to s \underset{˙}{+} t = s \cdot_{D} t$
21	20	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \underset{˙}{+} t = s \cdot_{D} t$
22	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E)) \to s \cdot_{D} t = s \circ t$
23	22	3impb	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \cdot_{D} t = s \circ t$
24	21 23	eqtrd	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \underset{˙}{+} t = s \circ t$
25	1 5	tendococl	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \circ t \in E$
26	24 25	eqeltrd	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s \underset{˙}{+} t \in E$
27		coass	$⊢ (s \circ t) \circ u = s \circ (t \circ u)$
28	18	oveqd	$⊢ (K \in HL \land W \in H) \to (s \underset{˙}{+} t) \underset{˙}{+} u = (s \underset{˙}{+} t) \cdot_{D} u$
29	28	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s \underset{˙}{+} t) \underset{˙}{+} u = (s \underset{˙}{+} t) \cdot_{D} u$
30		simpl	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (K \in HL \land W \in H)$
31	26	3adant3r3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} t \in E$
32		simpr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to u \in E$
33	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land (s \underset{˙}{+} t \in E \land u \in E)) \to (s \underset{˙}{+} t) \cdot_{D} u = (s \underset{˙}{+} t) \circ u$
34	30 31 32 33	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s \underset{˙}{+} t) \cdot_{D} u = (s \underset{˙}{+} t) \circ u$
35	18	oveqdr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} t = s \cdot_{D} t$
36	22	3adantr3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \cdot_{D} t = s \circ t$
37	35 36	eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} t = s \circ t$
38	37	coeq1d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s \underset{˙}{+} t) \circ u = (s \circ t) \circ u$
39	29 34 38	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s \underset{˙}{+} t) \underset{˙}{+} u = (s \circ t) \circ u$
40	18	oveqd	$⊢ (K \in HL \land W \in H) \to s \underset{˙}{+} (t \underset{˙}{+} u) = s \cdot_{D} (t \underset{˙}{+} u)$
41	40	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} (t \underset{˙}{+} u) = s \cdot_{D} (t \underset{˙}{+} u)$
42		simpr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \in E$
43	18	oveqdr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to t \underset{˙}{+} u = t \cdot_{D} u$
44	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land (t \in E \land u \in E)) \to t \cdot_{D} u = t \circ u$
45	44	3adantr1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to t \cdot_{D} u = t \circ u$
46	43 45	eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to t \underset{˙}{+} u = t \circ u$
47	1 5	tendococl	$⊢ ((K \in HL \land W \in H) \land t \in E \land u \in E) \to t \circ u \in E$
48	47	3adant3r1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to t \circ u \in E$
49	46 48	eqeltrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to t \underset{˙}{+} u \in E$
50	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \underset{˙}{+} u \in E)) \to s \cdot_{D} (t \underset{˙}{+} u) = s \circ (t \underset{˙}{+} u)$
51	30 42 49 50	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \cdot_{D} (t \underset{˙}{+} u) = s \circ (t \underset{˙}{+} u)$
52	46	coeq2d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \circ (t \underset{˙}{+} u) = s \circ (t \circ u)$
53	41 51 52	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} (t \underset{˙}{+} u) = s \circ (t \circ u)$
54	27 39 53	3eqtr4a	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s \underset{˙}{+} t) \underset{˙}{+} u = s \underset{˙}{+} (t \underset{˙}{+} u)$
55	1 4 5 6	tendodi1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \circ (t P u) = (s \circ t) P (s \circ u)$
56	18	oveqd	$⊢ (K \in HL \land W \in H) \to s \underset{˙}{+} (t P u) = s \cdot_{D} (t P u)$
57	56	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} (t P u) = s \cdot_{D} (t P u)$
58	1 4 5 6	tendoplcl	$⊢ ((K \in HL \land W \in H) \land t \in E \land u \in E) \to t P u \in E$
59	58	3adant3r1	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to t P u \in E$
60	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t P u \in E)) \to s \cdot_{D} (t P u) = s \circ (t P u)$
61	30 42 59 60	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \cdot_{D} (t P u) = s \circ (t P u)$
62	57 61	eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} (t P u) = s \circ (t P u)$
63	18	oveqdr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} u = s \cdot_{D} u$
64	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land (s \in E \land u \in E)) \to s \cdot_{D} u = s \circ u$
65	64	3adantr2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \cdot_{D} u = s \circ u$
66	63 65	eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} u = s \circ u$
67	37 66	oveq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s \underset{˙}{+} t) P (s \underset{˙}{+} u) = (s \circ t) P (s \circ u)$
68	55 62 67	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s \underset{˙}{+} (t P u) = (s \underset{˙}{+} t) P (s \underset{˙}{+} u)$
69	1 4 5 6	tendodi2	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s P t) \circ u = (s \circ u) P (t \circ u)$
70	18	oveqd	$⊢ (K \in HL \land W \in H) \to (s P t) \underset{˙}{+} u = (s P t) \cdot_{D} u$
71	70	adantr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s P t) \underset{˙}{+} u = (s P t) \cdot_{D} u$
72	1 4 5 6	tendoplcl	$⊢ ((K \in HL \land W \in H) \land s \in E \land t \in E) \to s P t \in E$
73	72	3adant3r3	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to s P t \in E$
74	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land (s P t \in E \land u \in E)) \to (s P t) \cdot_{D} u = (s P t) \circ u$
75	30 73 32 74	syl12anc	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s P t) \cdot_{D} u = (s P t) \circ u$
76	71 75	eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s P t) \underset{˙}{+} u = (s P t) \circ u$
77	66 46	oveq12d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s \underset{˙}{+} u) P (t \underset{˙}{+} u) = (s \circ u) P (t \circ u)$
78	69 76 77	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E \land u \in E)) \to (s P t) \underset{˙}{+} u = (s \underset{˙}{+} u) P (t \underset{˙}{+} u)$
79	1 4 5	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$
80	18	oveqd	$⊢ (K \in HL \land W \in H) \to ({I ↾}_{T}) \underset{˙}{+} s = ({I ↾}_{T}) \cdot_{D} s$
81	80	adantr	$⊢ ((K \in HL \land W \in H) \land s \in E) \to ({I ↾}_{T}) \underset{˙}{+} s = ({I ↾}_{T}) \cdot_{D} s$
82		simpl	$⊢ ((K \in HL \land W \in H) \land s \in E) \to (K \in HL \land W \in H)$
83	79	adantr	$⊢ ((K \in HL \land W \in H) \land s \in E) \to {I ↾}_{T} \in E$
84		simpr	$⊢ ((K \in HL \land W \in H) \land s \in E) \to s \in E$
85	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land ({I ↾}_{T} \in E \land s \in E)) \to ({I ↾}_{T}) \cdot_{D} s = ({I ↾}_{T}) \circ s$
86	82 83 84 85	syl12anc	$⊢ ((K \in HL \land W \in H) \land s \in E) \to ({I ↾}_{T}) \cdot_{D} s = ({I ↾}_{T}) \circ s$
87	1 4 5	tendo1mul	$⊢ ((K \in HL \land W \in H) \land s \in E) \to ({I ↾}_{T}) \circ s = s$
88	81 86 87	3eqtrd	$⊢ ((K \in HL \land W \in H) \land s \in E) \to ({I ↾}_{T}) \underset{˙}{+} s = s$
89	18	oveqd	$⊢ (K \in HL \land W \in H) \to s \underset{˙}{+} ({I ↾}_{T}) = s \cdot_{D} ({I ↾}_{T})$
90	89	adantr	$⊢ ((K \in HL \land W \in H) \land s \in E) \to s \underset{˙}{+} ({I ↾}_{T}) = s \cdot_{D} ({I ↾}_{T})$
91	1 4 5 2 16	erngmul	$⊢ ((K \in HL \land W \in H) \land (s \in E \land {I ↾}_{T} \in E)) \to s \cdot_{D} ({I ↾}_{T}) = s \circ ({I ↾}_{T})$
92	82 84 83 91	syl12anc	$⊢ ((K \in HL \land W \in H) \land s \in E) \to s \cdot_{D} ({I ↾}_{T}) = s \circ ({I ↾}_{T})$
93	1 4 5	tendo1mulr	$⊢ ((K \in HL \land W \in H) \land s \in E) \to s \circ ({I ↾}_{T}) = s$
94	90 92 93	3eqtrd	$⊢ ((K \in HL \land W \in H) \land s \in E) \to s \underset{˙}{+} ({I ↾}_{T}) = s$
95	12 15 18 19 26 54 68 78 79 88 94	isringd	$⊢ (K \in HL \land W \in H) \to D \in Ring$

Metamath Proof Explorer

Theorem erngdvlem3

Proof