erngdvlem4-rN

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

	Ref	Expression
Hypotheses	ernggrp.h-r	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	ernggrp.d-r	⊢ 𝐷 = ( ( EDRing_R ‘ 𝐾 ) ‘ 𝑊 )
	ernggrplem.b-r	⊢ 𝐵 = ( Base ‘ 𝐾 )
	ernggrplem.t-r	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	ernggrplem.e-r	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	ernggrplem.p-r	⊢ 𝑃 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) )
	ernggrplem.o-r	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	ernggrplem.i-r	⊢ 𝐼 = ( 𝑎 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑎 ‘ 𝑓 ) ) )
	erngrnglem.m-r	⊢ 𝑀 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑏 ∘ 𝑎 ) )
	edlemk6.j-r	⊢ ∨ = ( join ‘ 𝐾 )
	edlemk6.m-r	⊢ ∧ = ( meet ‘ 𝐾 )
	edlemk6.r-r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	edlemk6.p-r	⊢ 𝑄 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
	edlemk6.z-r	⊢ 𝑍 = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝑏 ) ) ∧ ( ( ℎ ‘ 𝑄 ) ∨ ( 𝑅 ‘ ( 𝑏 ∘ ^◡ ( 𝑠 ‘ ℎ ) ) ) ) )
	edlemk6.y-r	⊢ 𝑌 = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝑔 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝑔 ∘ ^◡ 𝑏 ) ) ) )
	edlemk6.x-r	⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ ( 𝑠 ‘ ℎ ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑔 ) ) → ( 𝑧 ‘ 𝑄 ) = 𝑌 ) )
	edlemk6.u-r	⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( ( 𝑠 ‘ ℎ ) = ℎ , 𝑔 , 𝑋 ) )
Assertion	erngdvlem4-rN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐷 ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		ernggrp.h-r	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		ernggrp.d-r	⊢ 𝐷 = ( ( EDRing_R ‘ 𝐾 ) ‘ 𝑊 )
3		ernggrplem.b-r	⊢ 𝐵 = ( Base ‘ 𝐾 )
4		ernggrplem.t-r	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		ernggrplem.e-r	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6		ernggrplem.p-r	⊢ 𝑃 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) )
7		ernggrplem.o-r	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
8		ernggrplem.i-r	⊢ 𝐼 = ( 𝑎 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ^◡ ( 𝑎 ‘ 𝑓 ) ) )
9		erngrnglem.m-r	⊢ 𝑀 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑏 ∘ 𝑎 ) )
10		edlemk6.j-r	⊢ ∨ = ( join ‘ 𝐾 )
11		edlemk6.m-r	⊢ ∧ = ( meet ‘ 𝐾 )
12		edlemk6.r-r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
13		edlemk6.p-r	⊢ 𝑄 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
14		edlemk6.z-r	⊢ 𝑍 = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝑏 ) ) ∧ ( ( ℎ ‘ 𝑄 ) ∨ ( 𝑅 ‘ ( 𝑏 ∘ ^◡ ( 𝑠 ‘ ℎ ) ) ) ) )
15		edlemk6.y-r	⊢ 𝑌 = ( ( 𝑄 ∨ ( 𝑅 ‘ 𝑔 ) ) ∧ ( 𝑍 ∨ ( 𝑅 ‘ ( 𝑔 ∘ ^◡ 𝑏 ) ) ) )
16		edlemk6.x-r	⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 ∀ 𝑏 ∈ 𝑇 ( ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ ( 𝑠 ‘ ℎ ) ) ∧ ( 𝑅 ‘ 𝑏 ) ≠ ( 𝑅 ‘ 𝑔 ) ) → ( 𝑧 ‘ 𝑄 ) = 𝑌 ) )
17		edlemk6.u-r	⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( ( 𝑠 ‘ ℎ ) = ℎ , 𝑔 , 𝑋 ) )
18		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
19	1 4 5 2 18	erngbase-rN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
20	19	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐸 = ( Base ‘ 𝐷 ) )
21	20	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐸 = ( Base ‘ 𝐷 ) )
22		eqid	⊢ ( ._r ‘ 𝐷 ) = ( ._r ‘ 𝐷 )
23	1 4 5 2 22	erngfmul-rN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ._r ‘ 𝐷 ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑏 ∘ 𝑎 ) ) )
24	9 23	eqtr4id	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( ._r ‘ 𝐷 ) )
25	24	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝑀 = ( ._r ‘ 𝐷 ) )
26	3 1 4 5 7	tendo0cl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ 𝐸 )
27	26 19	eleqtrrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ ( Base ‘ 𝐷 ) )
28		eqid	⊢ ( +_g ‘ 𝐷 ) = ( +_g ‘ 𝐷 )
29	1 4 5 2 28	erngfplus-rN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +_g ‘ 𝐷 ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑓 ) ∘ ( 𝑏 ‘ 𝑓 ) ) ) ) )
30	6 29	eqtr4id	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑃 = ( +_g ‘ 𝐷 ) )
31	30	oveqd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑂 𝑃 𝑂 ) = ( 𝑂 ( +_g ‘ 𝐷 ) 𝑂 ) )
32	3 1 4 5 7 6	tendo0pl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑂 ∈ 𝐸 ) → ( 𝑂 𝑃 𝑂 ) = 𝑂 )
33	26 32	mpdan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑂 𝑃 𝑂 ) = 𝑂 )
34	31 33	eqtr3d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑂 ( +_g ‘ 𝐷 ) 𝑂 ) = 𝑂 )
35	1 2 3 4 5 6 7 8	erngdvlem1-rN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Grp )
36		eqid	⊢ ( 0_g ‘ 𝐷 ) = ( 0_g ‘ 𝐷 )
37	18 28 36	isgrpid2	⊢ ( 𝐷 ∈ Grp → ( ( 𝑂 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝑂 ( +_g ‘ 𝐷 ) 𝑂 ) = 𝑂 ) ↔ ( 0_g ‘ 𝐷 ) = 𝑂 ) )
38	35 37	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑂 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝑂 ( +_g ‘ 𝐷 ) 𝑂 ) = 𝑂 ) ↔ ( 0_g ‘ 𝐷 ) = 𝑂 ) )
39	27 34 38	mpbi2and	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0_g ‘ 𝐷 ) = 𝑂 )
40	39	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 = ( 0_g ‘ 𝐷 ) )
41	40	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝑂 = ( 0_g ‘ 𝐷 ) )
42	1 4 5	tendoidcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
43	42 19	eleqtrrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) )
44	19	eleq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑢 ∈ ( Base ‘ 𝐷 ) ↔ 𝑢 ∈ 𝐸 ) )
45		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
46	42	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( I ↾ 𝑇 ) ∈ 𝐸 )
47		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → 𝑢 ∈ 𝐸 )
48	1 4 5 2 22	erngmul-rN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ 𝐸 ∧ 𝑢 ∈ 𝐸 ) ) → ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ ( I ↾ 𝑇 ) ) )
49	45 46 47 48	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = ( 𝑢 ∘ ( I ↾ 𝑇 ) ) )
50	1 4 5	tendo1mulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( 𝑢 ∘ ( I ↾ 𝑇 ) ) = 𝑢 )
51	49 50	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = 𝑢 )
52	1 4 5 2 22	erngmul-rN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑢 ∈ 𝐸 ∧ ( I ↾ 𝑇 ) ∈ 𝐸 ) ) → ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( ( I ↾ 𝑇 ) ∘ 𝑢 ) )
53	45 47 46 52	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( ( I ↾ 𝑇 ) ∘ 𝑢 ) )
54	1 4 5	tendo1mul	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( ( I ↾ 𝑇 ) ∘ 𝑢 ) = 𝑢 )
55	53 54	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 )
56	51 55	jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑢 ∈ 𝐸 ) → ( ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) )
57	56	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑢 ∈ 𝐸 → ( ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) )
58	44 57	sylbid	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑢 ∈ ( Base ‘ 𝐷 ) → ( ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) )
59	58	ralrimiv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑢 ∈ ( Base ‘ 𝐷 ) ( ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) )
60	1 2 3 4 5 6 7 8 9	erngdvlem3-rN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Ring )
61		eqid	⊢ ( 1_r ‘ 𝐷 ) = ( 1_r ‘ 𝐷 )
62	18 22 61	isringid	⊢ ( 𝐷 ∈ Ring → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝐷 ) ( ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) ↔ ( 1_r ‘ 𝐷 ) = ( I ↾ 𝑇 ) ) )
63	60 62	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝐷 ) ( ( ( I ↾ 𝑇 ) ( ._r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( ._r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) ↔ ( 1_r ‘ 𝐷 ) = ( I ↾ 𝑇 ) ) )
64	43 59 63	mpbi2and	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1_r ‘ 𝐷 ) = ( I ↾ 𝑇 ) )
65	64	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) = ( 1_r ‘ 𝐷 ) )
66	65	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → ( I ↾ 𝑇 ) = ( 1_r ‘ 𝐷 ) )
67	60	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐷 ∈ Ring )
68		simp1l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
69	24	oveqd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 𝑀 𝑡 ) = ( 𝑠 ( ._r ‘ 𝐷 ) 𝑡 ) )
70	68 69	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → ( 𝑠 𝑀 𝑡 ) = ( 𝑠 ( ._r ‘ 𝐷 ) 𝑡 ) )
71		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → 𝑠 ∈ 𝐸 )
72		simp3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → 𝑡 ∈ 𝐸 )
73	1 4 5 2 22	erngmul-rN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ) ) → ( 𝑠 ( ._r ‘ 𝐷 ) 𝑡 ) = ( 𝑡 ∘ 𝑠 ) )
74	68 71 72 73	syl12anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → ( 𝑠 ( ._r ‘ 𝐷 ) 𝑡 ) = ( 𝑡 ∘ 𝑠 ) )
75	70 74	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → ( 𝑠 𝑀 𝑡 ) = ( 𝑡 ∘ 𝑠 ) )
76		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) )
77		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) )
78	3 1 4 5 7	tendoconid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑡 ∘ 𝑠 ) ≠ 𝑂 )
79	68 76 77 78	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → ( 𝑡 ∘ 𝑠 ) ≠ 𝑂 )
80	75 79	eqnetrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ∧ ( 𝑡 ∈ 𝐸 ∧ 𝑡 ≠ 𝑂 ) ) → ( 𝑠 𝑀 𝑡 ) ≠ 𝑂 )
81	3 1 4 5 7	tendo1ne0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ 𝑂 )
82	81	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → ( I ↾ 𝑇 ) ≠ 𝑂 )
83		simpll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
84		simplrl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ℎ ∈ 𝑇 )
85		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) )
86	3 10 11 1 4 12 13 14 15 16 17 5 7	cdleml6	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ℎ ∈ 𝑇 ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑈 ∈ 𝐸 ∧ ( 𝑈 ‘ ( 𝑠 ‘ ℎ ) ) = ℎ ) )
87	86	simpld	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ℎ ∈ 𝑇 ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → 𝑈 ∈ 𝐸 )
88	83 84 85 87	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → 𝑈 ∈ 𝐸 )
89	3 10 11 1 4 12 13 14 15 16 17 5 7	cdleml9	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → 𝑈 ≠ 𝑂 )
90	89	3expa	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → 𝑈 ≠ 𝑂 )
91	24	oveqd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 𝑀 𝑈 ) = ( 𝑠 ( ._r ‘ 𝐷 ) 𝑈 ) )
92	91	ad2antrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 𝑀 𝑈 ) = ( 𝑠 ( ._r ‘ 𝐷 ) 𝑈 ) )
93		simprl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → 𝑠 ∈ 𝐸 )
94	1 4 5 2 22	erngmul-rN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑠 ( ._r ‘ 𝐷 ) 𝑈 ) = ( 𝑈 ∘ 𝑠 ) )
95	83 93 88 94	syl12anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 ( ._r ‘ 𝐷 ) 𝑈 ) = ( 𝑈 ∘ 𝑠 ) )
96	3 10 11 1 4 12 13 14 15 16 17 5 7	cdleml8	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑈 ∘ 𝑠 ) = ( I ↾ 𝑇 ) )
97	96	3expa	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑈 ∘ 𝑠 ) = ( I ↾ 𝑇 ) )
98	95 97	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 ( ._r ‘ 𝐷 ) 𝑈 ) = ( I ↾ 𝑇 ) )
99	92 98	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 𝑀 𝑈 ) = ( I ↾ 𝑇 ) )
100	21 25 41 66 67 80 82 88 90 99	isdrngrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐷 ∈ DivRing )

Metamath Proof Explorer

Theorem erngdvlem4-rN

Proof