erngdvlem3-rN

Description: Lemma for eringring . (Contributed by NM, 6-Aug-2013) (New usage is discouraged.)

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

Proof

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

Metamath Proof Explorer

Theorem erngdvlem3-rN

Proof