erngdvlem4-rN

Description: Lemma for erngdv . (Contributed by NM, 11-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)$
	edlemk6.j-r	$⊢ \underset{˙}{\lor} = join (K)$
	edlemk6.m-r	$⊢ \underset{˙}{\land} = meet (K)$
	edlemk6.r-r	$⊢ R = trL (K) (W)$
	edlemk6.p-r	$⊢ Q = oc (K) (W)$
	edlemk6.z-r	$⊢ Z = (Q \underset{˙}{\lor} R (b)) \underset{˙}{\land} (h (Q) \underset{˙}{\lor} R (b \circ {s (h)}^{-1}))$
	edlemk6.y-r	$⊢ Y = (Q \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
	edlemk6.x-r	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (s (h)) \land R (b) \neq R (g)) \to z (Q) = Y))$
	edlemk6.u-r	$⊢ U = (g \in T ⟼ if (s (h) = h, g, X))$
Assertion	erngdvlem4-rN	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to D \in DivRing$

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		edlemk6.j-r	$⊢ \underset{˙}{\lor} = join (K)$
11		edlemk6.m-r	$⊢ \underset{˙}{\land} = meet (K)$
12		edlemk6.r-r	$⊢ R = trL (K) (W)$
13		edlemk6.p-r	$⊢ Q = oc (K) (W)$
14		edlemk6.z-r	$⊢ Z = (Q \underset{˙}{\lor} R (b)) \underset{˙}{\land} (h (Q) \underset{˙}{\lor} R (b \circ {s (h)}^{-1}))$
15		edlemk6.y-r	$⊢ Y = (Q \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
16		edlemk6.x-r	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (s (h)) \land R (b) \neq R (g)) \to z (Q) = Y))$
17		edlemk6.u-r	$⊢ U = (g \in T ⟼ if (s (h) = h, g, X))$
18		eqid	$⊢ {Base}_{D} = {Base}_{D}$
19	1 4 5 2 18	erngbase-rN	$⊢ (K \in HL \land W \in H) \to {Base}_{D} = E$
20	19	eqcomd	$⊢ (K \in HL \land W \in H) \to E = {Base}_{D}$
21	20	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to E = {Base}_{D}$
22		eqid	$⊢ \cdot_{D} = \cdot_{D}$
23	1 4 5 2 22	erngfmul-rN	$⊢ (K \in HL \land W \in H) \to \cdot_{D} = (a \in E, b \in E ⟼ b \circ a)$
24	9 23	eqtr4id	$⊢ (K \in HL \land W \in H) \to M = \cdot_{D}$
25	24	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to M = \cdot_{D}$
26	3 1 4 5 7	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
27	26 19	eleqtrrd	$⊢ (K \in HL \land W \in H) \to O \in {Base}_{D}$
28		eqid	$⊢ +_{D} = +_{D}$
29	1 4 5 2 28	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)))$
30	6 29	eqtr4id	$⊢ (K \in HL \land W \in H) \to P = +_{D}$
31	30	oveqd	$⊢ (K \in HL \land W \in H) \to O P O = O +_{D} O$
32	3 1 4 5 7 6	tendo0pl	$⊢ ((K \in HL \land W \in H) \land O \in E) \to O P O = O$
33	26 32	mpdan	$⊢ (K \in HL \land W \in H) \to O P O = O$
34	31 33	eqtr3d	$⊢ (K \in HL \land W \in H) \to O +_{D} O = O$
35	1 2 3 4 5 6 7 8	erngdvlem1-rN	$⊢ (K \in HL \land W \in H) \to D \in Grp$
36		eqid	$⊢ 0_{D} = 0_{D}$
37	18 28 36	isgrpid2	$⊢ D \in Grp \to ((O \in {Base}_{D} \land O +_{D} O = O) \leftrightarrow 0_{D} = O)$
38	35 37	syl	$⊢ (K \in HL \land W \in H) \to ((O \in {Base}_{D} \land O +_{D} O = O) \leftrightarrow 0_{D} = O)$
39	27 34 38	mpbi2and	$⊢ (K \in HL \land W \in H) \to 0_{D} = O$
40	39	eqcomd	$⊢ (K \in HL \land W \in H) \to O = 0_{D}$
41	40	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to O = 0_{D}$
42	1 4 5	tendoidcl	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in E$
43	42 19	eleqtrrd	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \in {Base}_{D}$
44	19	eleq2d	$⊢ (K \in HL \land W \in H) \to (u \in {Base}_{D} \leftrightarrow u \in E)$
45		simpl	$⊢ ((K \in HL \land W \in H) \land u \in E) \to (K \in HL \land W \in H)$
46	42	adantr	$⊢ ((K \in HL \land W \in H) \land u \in E) \to {I ↾}_{T} \in E$
47		simpr	$⊢ ((K \in HL \land W \in H) \land u \in E) \to u \in E$
48	1 4 5 2 22	erngmul-rN	$⊢ ((K \in HL \land W \in H) \land ({I ↾}_{T} \in E \land u \in E)) \to ({I ↾}_{T}) \cdot_{D} u = u \circ ({I ↾}_{T})$
49	45 46 47 48	syl12anc	$⊢ ((K \in HL \land W \in H) \land u \in E) \to ({I ↾}_{T}) \cdot_{D} u = u \circ ({I ↾}_{T})$
50	1 4 5	tendo1mulr	$⊢ ((K \in HL \land W \in H) \land u \in E) \to u \circ ({I ↾}_{T}) = u$
51	49 50	eqtrd	$⊢ ((K \in HL \land W \in H) \land u \in E) \to ({I ↾}_{T}) \cdot_{D} u = u$
52	1 4 5 2 22	erngmul-rN	$⊢ ((K \in HL \land W \in H) \land (u \in E \land {I ↾}_{T} \in E)) \to u \cdot_{D} ({I ↾}_{T}) = ({I ↾}_{T}) \circ u$
53	45 47 46 52	syl12anc	$⊢ ((K \in HL \land W \in H) \land u \in E) \to u \cdot_{D} ({I ↾}_{T}) = ({I ↾}_{T}) \circ u$
54	1 4 5	tendo1mul	$⊢ ((K \in HL \land W \in H) \land u \in E) \to ({I ↾}_{T}) \circ u = u$
55	53 54	eqtrd	$⊢ ((K \in HL \land W \in H) \land u \in E) \to u \cdot_{D} ({I ↾}_{T}) = u$
56	51 55	jca	$⊢ ((K \in HL \land W \in H) \land u \in E) \to (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u)$
57	56	ex	$⊢ (K \in HL \land W \in H) \to (u \in E \to (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u))$
58	44 57	sylbid	$⊢ (K \in HL \land W \in H) \to (u \in {Base}_{D} \to (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u))$
59	58	ralrimiv	$⊢ (K \in HL \land W \in H) \to \forall u \in {Base}_{D} (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u)$
60	1 2 3 4 5 6 7 8 9	erngdvlem3-rN	$⊢ (K \in HL \land W \in H) \to D \in Ring$
61		eqid	$⊢ 1_{D} = 1_{D}$
62	18 22 61	isringid	$⊢ D \in Ring \to (({I ↾}_{T} \in {Base}_{D} \land \forall u \in {Base}_{D} (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u)) \leftrightarrow 1_{D} = {I ↾}_{T})$
63	60 62	syl	$⊢ (K \in HL \land W \in H) \to (({I ↾}_{T} \in {Base}_{D} \land \forall u \in {Base}_{D} (({I ↾}_{T}) \cdot_{D} u = u \land u \cdot_{D} ({I ↾}_{T}) = u)) \leftrightarrow 1_{D} = {I ↾}_{T})$
64	43 59 63	mpbi2and	$⊢ (K \in HL \land W \in H) \to 1_{D} = {I ↾}_{T}$
65	64	eqcomd	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} = 1_{D}$
66	65	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to {I ↾}_{T} = 1_{D}$
67	60	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to D \in Ring$
68		simp1l	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to (K \in HL \land W \in H)$
69	24	oveqd	$⊢ (K \in HL \land W \in H) \to s M t = s \cdot_{D} t$
70	68 69	syl	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to s M t = s \cdot_{D} t$
71		simp2l	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to s \in E$
72		simp3l	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to t \in E$
73	1 4 5 2 22	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$
74	68 71 72 73	syl12anc	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to s \cdot_{D} t = t \circ s$
75	70 74	eqtrd	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to s M t = t \circ s$
76		simp3	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to (t \in E \land t \neq O)$
77		simp2	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to (s \in E \land s \neq O)$
78	3 1 4 5 7	tendoconid	$⊢ ((K \in HL \land W \in H) \land (t \in E \land t \neq O) \land (s \in E \land s \neq O)) \to t \circ s \neq O$
79	68 76 77 78	syl3anc	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to t \circ s \neq O$
80	75 79	eqnetrd	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O) \land (t \in E \land t \neq O)) \to s M t \neq O$
81	3 1 4 5 7	tendo1ne0	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \neq O$
82	81	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to {I ↾}_{T} \neq O$
83		simpll	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to (K \in HL \land W \in H)$
84		simplrl	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to h \in T$
85		simpr	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to (s \in E \land s \neq O)$
86	3 10 11 1 4 12 13 14 15 16 17 5 7	cdleml6	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq O)) \to (U \in E \land U (s (h)) = h)$
87	86	simpld	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq O)) \to U \in E$
88	83 84 85 87	syl3anc	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to U \in E$
89	24	oveqd	$⊢ (K \in HL \land W \in H) \to s M U = s \cdot_{D} U$
90	89	ad2antrr	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to s M U = s \cdot_{D} U$
91		simprl	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to s \in E$
92	1 4 5 2 22	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$
93	83 91 88 92	syl12anc	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to s \cdot_{D} U = U \circ s$
94	3 10 11 1 4 12 13 14 15 16 17 5 7	cdleml8	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq O)) \to U \circ s = {I ↾}_{T}$
95	94	3expa	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to U \circ s = {I ↾}_{T}$
96	93 95	eqtrd	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to s \cdot_{D} U = {I ↾}_{T}$
97	90 96	eqtrd	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq O)) \to s M U = {I ↾}_{T}$
98	21 25 41 66 67 80 82 88 97	isdrngrd	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to D \in DivRing$

Metamath Proof Explorer

Theorem erngdvlem4-rN

Proof