erngdvlem4

	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)$
	edlemk6.j	$⊢ \underset{˙}{\lor} = join (K)$
	edlemk6.m	$⊢ \underset{˙}{\land} = meet (K)$
	edlemk6.r	$⊢ R = trL (K) (W)$
	edlemk6.p	$⊢ Q = oc (K) (W)$
	edlemk6.z	$⊢ Z = (Q \underset{˙}{\lor} R (b)) \underset{˙}{\land} (h (Q) \underset{˙}{\lor} R (b \circ {s (h)}^{-1}))$
	edlemk6.y	$⊢ Y = (Q \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
	edlemk6.x	$⊢ 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	$⊢ U = (g \in T ⟼ if (s (h) = h, g, X))$
Assertion	erngdvlem4	$⊢ ((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	$⊢ 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		edlemk6.j	$⊢ \underset{˙}{\lor} = join (K)$
11		edlemk6.m	$⊢ \underset{˙}{\land} = meet (K)$
12		edlemk6.r	$⊢ R = trL (K) (W)$
13		edlemk6.p	$⊢ Q = oc (K) (W)$
14		edlemk6.z	$⊢ Z = (Q \underset{˙}{\lor} R (b)) \underset{˙}{\land} (h (Q) \underset{˙}{\lor} R (b \circ {s (h)}^{-1}))$
15		edlemk6.y	$⊢ Y = (Q \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
16		edlemk6.x	$⊢ 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	$⊢ U = (g \in T ⟼ if (s (h) = h, g, X))$
18		eqid	$⊢ {Base}_{D} = {Base}_{D}$
19	1 4 5 2 18	erngbase	$⊢ (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	$⊢ (K \in HL \land W \in H) \to \cdot_{D} = (a \in E, b \in E ⟼ a \circ b)$
24	9 23	eqtr4id	$⊢ (K \in HL \land W \in H) \to \underset{˙}{+} = \cdot_{D}$
25	24	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to \underset{˙}{+} = \cdot_{D}$
26	3 1 4 5 7	tendo0cl	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} \in E$
27	26 19	eleqtrrd	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} \in {Base}_{D}$
28		eqid	$⊢ +_{D} = +_{D}$
29	1 4 5 2 28	erngfplus	$⊢ (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 \underset{˙}{0} P \underset{˙}{0} = \underset{˙}{0} +_{D} \underset{˙}{0}$
32	3 1 4 5 7 6	tendo0pl	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{0} \in E) \to \underset{˙}{0} P \underset{˙}{0} = \underset{˙}{0}$
33	26 32	mpdan	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} P \underset{˙}{0} = \underset{˙}{0}$
34	31 33	eqtr3d	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} +_{D} \underset{˙}{0} = \underset{˙}{0}$
35	1 2 3 4 5 6 7 8	erngdvlem1	$⊢ (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 ((\underset{˙}{0} \in {Base}_{D} \land \underset{˙}{0} +_{D} \underset{˙}{0} = \underset{˙}{0}) \leftrightarrow 0_{D} = \underset{˙}{0})$
38	35 37	syl	$⊢ (K \in HL \land W \in H) \to ((\underset{˙}{0} \in {Base}_{D} \land \underset{˙}{0} +_{D} \underset{˙}{0} = \underset{˙}{0}) \leftrightarrow 0_{D} = \underset{˙}{0})$
39	27 34 38	mpbi2and	$⊢ (K \in HL \land W \in H) \to 0_{D} = \underset{˙}{0}$
40	39	eqcomd	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} = 0_{D}$
41	40	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to \underset{˙}{0} = 0_{D}$
42	1 2 3 4 5 6 7 8 9	erngdvlem3	$⊢ (K \in HL \land W \in H) \to D \in Ring$
43	1 4 5 2 42	erng1lem	$⊢ (K \in HL \land W \in H) \to 1_{D} = {I ↾}_{T}$
44	43	eqcomd	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} = 1_{D}$
45	44	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to {I ↾}_{T} = 1_{D}$
46	42	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to D \in Ring$
47		simp1l	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to (K \in HL \land W \in H)$
48	24	oveqd	$⊢ (K \in HL \land W \in H) \to s \underset{˙}{+} t = s \cdot_{D} t$
49	47 48	syl	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to s \underset{˙}{+} t = s \cdot_{D} t$
50		simp2l	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to s \in E$
51		simp3l	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to t \in E$
52	1 4 5 2 22	erngmul	$⊢ ((K \in HL \land W \in H) \land (s \in E \land t \in E)) \to s \cdot_{D} t = s \circ t$
53	47 50 51 52	syl12anc	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to s \cdot_{D} t = s \circ t$
54	49 53	eqtrd	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to s \underset{˙}{+} t = s \circ t$
55	3 1 4 5 7	tendoconid	$⊢ ((K \in HL \land W \in H) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to s \circ t \neq \underset{˙}{0}$
56	55	3adant1r	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to s \circ t \neq \underset{˙}{0}$
57	54 56	eqnetrd	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0}) \land (t \in E \land t \neq \underset{˙}{0})) \to s \underset{˙}{+} t \neq \underset{˙}{0}$
58	3 1 4 5 7	tendo1ne0	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \neq \underset{˙}{0}$
59	58	adantr	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \to {I ↾}_{T} \neq \underset{˙}{0}$
60		simpll	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to (K \in HL \land W \in H)$
61		simplrl	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to h \in T$
62		simpr	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to (s \in E \land s \neq \underset{˙}{0})$
63	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 \underset{˙}{0})) \to (U \in E \land U (s (h)) = h)$
64	63	simpld	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to U \in E$
65	60 61 62 64	syl3anc	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to U \in E$
66	24	oveqd	$⊢ (K \in HL \land W \in H) \to U \underset{˙}{+} s = U \cdot_{D} s$
67	66	ad2antrr	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to U \underset{˙}{+} s = U \cdot_{D} s$
68		simprl	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to s \in E$
69	1 4 5 2 22	erngmul	$⊢ ((K \in HL \land W \in H) \land (U \in E \land s \in E)) \to U \cdot_{D} s = U \circ s$
70	60 65 68 69	syl12anc	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to U \cdot_{D} s = U \circ s$
71	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 \underset{˙}{0})) \to U \circ s = {I ↾}_{T}$
72	71	3expa	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to U \circ s = {I ↾}_{T}$
73	67 70 72	3eqtrd	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B})) \land (s \in E \land s \neq \underset{˙}{0})) \to U \underset{˙}{+} s = {I ↾}_{T}$
74	21 25 41 45 46 57 59 65 73	isdrngd	$⊢ ((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

Proof