This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐷 = ( ( EDRingR ‘ 𝐾 ) ‘ 𝑊 )
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 ⊢ 𝐷 = ( ( EDRingR ‘ 𝐾 ) ‘ 𝑊 )
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 ⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
37 18 28 36 isgrpid2 ⊢ ( 𝐷 ∈ Grp → ( ( 𝑂 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝑂 ( +g ‘ 𝐷 ) 𝑂 ) = 𝑂 ) ↔ ( 0g ‘ 𝐷 ) = 𝑂 ) )
38 35 37 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑂 ∈ ( Base ‘ 𝐷 ) ∧ ( 𝑂 ( +g ‘ 𝐷 ) 𝑂 ) = 𝑂 ) ↔ ( 0g ‘ 𝐷 ) = 𝑂 ) )
39 27 34 38 mpbi2and ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ 𝐷 ) = 𝑂 )
40 39 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 = ( 0g ‘ 𝐷 ) )
41 40 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝑂 = ( 0g ‘ 𝐷 ) )
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 ⊢ ( 1r ‘ 𝐷 ) = ( 1r ‘ 𝐷 )
62 18 22 61 isringid ⊢ ( 𝐷 ∈ Ring → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝐷 ) ( ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) ↔ ( 1r ‘ 𝐷 ) = ( I ↾ 𝑇 ) ) )
63 60 62 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ∀ 𝑢 ∈ ( Base ‘ 𝐷 ) ( ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) 𝑢 ) = 𝑢 ∧ ( 𝑢 ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = 𝑢 ) ) ↔ ( 1r ‘ 𝐷 ) = ( I ↾ 𝑇 ) ) )
64 43 59 63 mpbi2and ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1r ‘ 𝐷 ) = ( I ↾ 𝑇 ) )
65 64 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) = ( 1r ‘ 𝐷 ) )
66 65 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → ( I ↾ 𝑇 ) = ( 1r ‘ 𝐷 ) )
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 24 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑠 𝑀 𝑈 ) = ( 𝑠 ( .r ‘ 𝐷 ) 𝑈 ) )
90 89 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 𝑀 𝑈 ) = ( 𝑠 ( .r ‘ 𝐷 ) 𝑈 ) )
91 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → 𝑠 ∈ 𝐸 )
92 1 4 5 2 22 erngmul-rN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑈 ∈ 𝐸 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑈 ) = ( 𝑈 ∘ 𝑠 ) )
93 83 91 88 92 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑈 ) = ( 𝑈 ∘ 𝑠 ) )
94 3 10 11 1 4 12 13 14 15 16 17 5 7 cdleml8 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑈 ∘ 𝑠 ) = ( I ↾ 𝑇 ) )
95 94 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑈 ∘ 𝑠 ) = ( I ↾ 𝑇 ) )
96 93 95 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 ( .r ‘ 𝐷 ) 𝑈 ) = ( I ↾ 𝑇 ) )
97 90 96 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂 ) ) → ( 𝑠 𝑀 𝑈 ) = ( I ↾ 𝑇 ) )
98 21 25 41 66 67 80 82 88 97 isdrngrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ℎ ∈ 𝑇 ∧ ℎ ≠ ( I ↾ 𝐵 ) ) ) → 𝐷 ∈ DivRing )