Theorem erngdvlem3 40979

Description: Lemma for eringring 40981. (Contributed by NM, 6-Aug-2013.)

Hypotheses

Ref	Expression
ernggrp.h	⊢ 𝐻 = (LHyp‘𝐾)
ernggrp.d	⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)
erngdv.b	⊢ 𝐵 = (Base‘𝐾)
erngdv.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
erngdv.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
erngdv.p	⊢ 𝑃 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓))))
erngdv.o	⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))
erngdv.i	⊢ 𝐼 = (𝑎 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑎‘𝑓)))
erngrnglem.m	⊢ + = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑎 ∘ 𝑏))

Assertion

Ref	Expression
erngdvlem3	⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ Ring)

Distinct variable groups:   𝐵,𝑓   𝑎,𝑏,𝐸   𝑓,𝑎,𝐾,𝑏   𝑓,𝐻   𝑇,𝑎,𝑏,𝑓   𝑊,𝑎,𝑏,𝑓

Allowed substitution hints:   𝐵(𝑎,𝑏)   𝐷(𝑓,𝑎,𝑏)   𝑃(𝑓,𝑎,𝑏)   + (𝑓,𝑎,𝑏)   𝐸(𝑓)   𝐻(𝑎,𝑏)   𝐼(𝑓,𝑎,𝑏)   0 (𝑓,𝑎,𝑏)

Proof of Theorem erngdvlem3

Dummy variables 𝑡 𝑠 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ernggrp.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
2		erngdv.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
3		erngdv.e	. . . 4 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
4		ernggrp.d	. . . 4 ⊢ 𝐷 = ((EDRing‘𝐾)‘𝑊)
5		eqid 2729	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
6	1, 2, 3, 4, 5	erngbase 40790	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝐷) = 𝐸)
7	6	eqcomd 2735	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐸 = (Base‘𝐷))
8		erngdv.p	. . 3 ⊢ 𝑃 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓))))
9		eqid 2729	. . . 4 ⊢ (+g‘𝐷) = (+g‘𝐷)
10	1, 2, 3, 4, 9	erngfplus 40791	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+g‘𝐷) = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑎‘𝑓) ∘ (𝑏‘𝑓)))))
11	8, 10	eqtr4id 2783	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑃 = (+g‘𝐷))
12		erngrnglem.m	. . 3 ⊢ + = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑎 ∘ 𝑏))
13		eqid 2729	. . . 4 ⊢ (.r‘𝐷) = (.r‘𝐷)
14	1, 2, 3, 4, 13	erngfmul 40794	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (.r‘𝐷) = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑎 ∘ 𝑏)))
15	12, 14	eqtr4id 2783	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → + = (.r‘𝐷))
16		erngdv.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
17		erngdv.o	. . 3 ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵))
18		erngdv.i	. . 3 ⊢ 𝐼 = (𝑎 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑎‘𝑓)))
19	1, 4, 16, 2, 3, 8, 17, 18	erngdvlem1 40977	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ Grp)
20	15	oveqd 7366	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑠 + 𝑡) = (𝑠(.r‘𝐷)𝑡))
21	20	3ad2ant1 1133	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 + 𝑡) = (𝑠(.r‘𝐷)𝑡))
22	1, 2, 3, 4, 13	erngmul 40795	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸)) → (𝑠(.r‘𝐷)𝑡) = (𝑠 ∘ 𝑡))
23	22	3impb 1114	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠(.r‘𝐷)𝑡) = (𝑠 ∘ 𝑡))
24	21, 23	eqtrd 2764	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 + 𝑡) = (𝑠 ∘ 𝑡))
25	1, 3	tendococl 40761	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 ∘ 𝑡) ∈ 𝐸)
26	24, 25	eqeltrd 2828	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠 + 𝑡) ∈ 𝐸)
27		coass 6214	. . 3 ⊢ ((𝑠 ∘ 𝑡) ∘ 𝑢) = (𝑠 ∘ (𝑡 ∘ 𝑢))
28	15	oveqd 7366	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((𝑠 + 𝑡) + 𝑢) = ((𝑠 + 𝑡)(.r‘𝐷)𝑢))
29	28	adantr 480	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠 + 𝑡) + 𝑢) = ((𝑠 + 𝑡)(.r‘𝐷)𝑢))
30		simpl 482	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
31	26	3adant3r3 1185	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + 𝑡) ∈ 𝐸)
32		simpr3 1197	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → 𝑢 ∈ 𝐸)
33	1, 2, 3, 4, 13	erngmul 40795	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠 + 𝑡) ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠 + 𝑡)(.r‘𝐷)𝑢) = ((𝑠 + 𝑡) ∘ 𝑢))
34	30, 31, 32, 33	syl12anc 836	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠 + 𝑡)(.r‘𝐷)𝑢) = ((𝑠 + 𝑡) ∘ 𝑢))
35	15	oveqdr 7377	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + 𝑡) = (𝑠(.r‘𝐷)𝑡))
36	22	3adantr3 1172	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠(.r‘𝐷)𝑡) = (𝑠 ∘ 𝑡))
37	35, 36	eqtrd 2764	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + 𝑡) = (𝑠 ∘ 𝑡))
38	37	coeq1d 5804	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠 + 𝑡) ∘ 𝑢) = ((𝑠 ∘ 𝑡) ∘ 𝑢))
39	29, 34, 38	3eqtrd 2768	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠 + 𝑡) + 𝑢) = ((𝑠 ∘ 𝑡) ∘ 𝑢))
40	15	oveqd 7366	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑠 + (𝑡 + 𝑢)) = (𝑠(.r‘𝐷)(𝑡 + 𝑢)))
41	40	adantr 480	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + (𝑡 + 𝑢)) = (𝑠(.r‘𝐷)(𝑡 + 𝑢)))
42		simpr1 1195	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → 𝑠 ∈ 𝐸)
43	15	oveqdr 7377	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑡 + 𝑢) = (𝑡(.r‘𝐷)𝑢))
44	1, 2, 3, 4, 13	erngmul 40795	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑡(.r‘𝐷)𝑢) = (𝑡 ∘ 𝑢))
45	44	3adantr1 1170	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑡(.r‘𝐷)𝑢) = (𝑡 ∘ 𝑢))
46	43, 45	eqtrd 2764	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑡 + 𝑢) = (𝑡 ∘ 𝑢))
47	1, 3	tendococl 40761	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸) → (𝑡 ∘ 𝑢) ∈ 𝐸)
48	47	3adant3r1 1183	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑡 ∘ 𝑢) ∈ 𝐸)
49	46, 48	eqeltrd 2828	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑡 + 𝑢) ∈ 𝐸)
50	1, 2, 3, 4, 13	erngmul 40795	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑡 + 𝑢) ∈ 𝐸)) → (𝑠(.r‘𝐷)(𝑡 + 𝑢)) = (𝑠 ∘ (𝑡 + 𝑢)))
51	30, 42, 49, 50	syl12anc 836	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠(.r‘𝐷)(𝑡 + 𝑢)) = (𝑠 ∘ (𝑡 + 𝑢)))
52	46	coeq2d 5805	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 ∘ (𝑡 + 𝑢)) = (𝑠 ∘ (𝑡 ∘ 𝑢)))
53	41, 51, 52	3eqtrd 2768	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + (𝑡 + 𝑢)) = (𝑠 ∘ (𝑡 ∘ 𝑢)))
54	27, 39, 53	3eqtr4a 2790	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠 + 𝑡) + 𝑢) = (𝑠 + (𝑡 + 𝑢)))
55	1, 2, 3, 8	tendodi1 40773	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 ∘ (𝑡𝑃𝑢)) = ((𝑠 ∘ 𝑡)𝑃(𝑠 ∘ 𝑢)))
56	15	oveqd 7366	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑠 + (𝑡𝑃𝑢)) = (𝑠(.r‘𝐷)(𝑡𝑃𝑢)))
57	56	adantr 480	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + (𝑡𝑃𝑢)) = (𝑠(.r‘𝐷)(𝑡𝑃𝑢)))
58	1, 2, 3, 8	tendoplcl 40770	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸) → (𝑡𝑃𝑢) ∈ 𝐸)
59	58	3adant3r1 1183	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑡𝑃𝑢) ∈ 𝐸)
60	1, 2, 3, 4, 13	erngmul 40795	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ (𝑡𝑃𝑢) ∈ 𝐸)) → (𝑠(.r‘𝐷)(𝑡𝑃𝑢)) = (𝑠 ∘ (𝑡𝑃𝑢)))
61	30, 42, 59, 60	syl12anc 836	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠(.r‘𝐷)(𝑡𝑃𝑢)) = (𝑠 ∘ (𝑡𝑃𝑢)))
62	57, 61	eqtrd 2764	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + (𝑡𝑃𝑢)) = (𝑠 ∘ (𝑡𝑃𝑢)))
63	15	oveqdr 7377	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + 𝑢) = (𝑠(.r‘𝐷)𝑢))
64	1, 2, 3, 4, 13	erngmul 40795	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠(.r‘𝐷)𝑢) = (𝑠 ∘ 𝑢))
65	64	3adantr2 1171	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠(.r‘𝐷)𝑢) = (𝑠 ∘ 𝑢))
66	63, 65	eqtrd 2764	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + 𝑢) = (𝑠 ∘ 𝑢))
67	37, 66	oveq12d 7367	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠 + 𝑡)𝑃(𝑠 + 𝑢)) = ((𝑠 ∘ 𝑡)𝑃(𝑠 ∘ 𝑢)))
68	55, 62, 67	3eqtr4d 2774	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠 + (𝑡𝑃𝑢)) = ((𝑠 + 𝑡)𝑃(𝑠 + 𝑢)))
69	1, 2, 3, 8	tendodi2 40774	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠𝑃𝑡) ∘ 𝑢) = ((𝑠 ∘ 𝑢)𝑃(𝑡 ∘ 𝑢)))
70	15	oveqd 7366	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((𝑠𝑃𝑡) + 𝑢) = ((𝑠𝑃𝑡)(.r‘𝐷)𝑢))
71	70	adantr 480	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠𝑃𝑡) + 𝑢) = ((𝑠𝑃𝑡)(.r‘𝐷)𝑢))
72	1, 2, 3, 8	tendoplcl 40770	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸) → (𝑠𝑃𝑡) ∈ 𝐸)
73	72	3adant3r3 1185	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → (𝑠𝑃𝑡) ∈ 𝐸)
74	1, 2, 3, 4, 13	erngmul 40795	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑠𝑃𝑡) ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠𝑃𝑡)(.r‘𝐷)𝑢) = ((𝑠𝑃𝑡) ∘ 𝑢))
75	30, 73, 32, 74	syl12anc 836	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠𝑃𝑡)(.r‘𝐷)𝑢) = ((𝑠𝑃𝑡) ∘ 𝑢))
76	71, 75	eqtrd 2764	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠𝑃𝑡) + 𝑢) = ((𝑠𝑃𝑡) ∘ 𝑢))
77	66, 46	oveq12d 7367	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠 + 𝑢)𝑃(𝑡 + 𝑢)) = ((𝑠 ∘ 𝑢)𝑃(𝑡 ∘ 𝑢)))
78	69, 76, 77	3eqtr4d 2774	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ 𝑡 ∈ 𝐸 ∧ 𝑢 ∈ 𝐸)) → ((𝑠𝑃𝑡) + 𝑢) = ((𝑠 + 𝑢)𝑃(𝑡 + 𝑢)))
79	1, 2, 3	tendoidcl 40758	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ 𝐸)
80	15	oveqd 7366	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (( I ↾ 𝑇) + 𝑠) = (( I ↾ 𝑇)(.r‘𝐷)𝑠))
81	80	adantr 480	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (( I ↾ 𝑇) + 𝑠) = (( I ↾ 𝑇)(.r‘𝐷)𝑠))
82		simpl 482	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
83	79	adantr 480	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → ( I ↾ 𝑇) ∈ 𝐸)
84		simpr 484	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → 𝑠 ∈ 𝐸)
85	1, 2, 3, 4, 13	erngmul 40795	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (( I ↾ 𝑇) ∈ 𝐸 ∧ 𝑠 ∈ 𝐸)) → (( I ↾ 𝑇)(.r‘𝐷)𝑠) = (( I ↾ 𝑇) ∘ 𝑠))
86	82, 83, 84, 85	syl12anc 836	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (( I ↾ 𝑇)(.r‘𝐷)𝑠) = (( I ↾ 𝑇) ∘ 𝑠))
87	1, 2, 3	tendo1mul 40759	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (( I ↾ 𝑇) ∘ 𝑠) = 𝑠)
88	81, 86, 87	3eqtrd 2768	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (( I ↾ 𝑇) + 𝑠) = 𝑠)
89	15	oveqd 7366	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑠 + ( I ↾ 𝑇)) = (𝑠(.r‘𝐷)( I ↾ 𝑇)))
90	89	adantr 480	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (𝑠 + ( I ↾ 𝑇)) = (𝑠(.r‘𝐷)( I ↾ 𝑇)))
91	1, 2, 3, 4, 13	erngmul 40795	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑠 ∈ 𝐸 ∧ ( I ↾ 𝑇) ∈ 𝐸)) → (𝑠(.r‘𝐷)( I ↾ 𝑇)) = (𝑠 ∘ ( I ↾ 𝑇)))
92	82, 84, 83, 91	syl12anc 836	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (𝑠(.r‘𝐷)( I ↾ 𝑇)) = (𝑠 ∘ ( I ↾ 𝑇)))
93	1, 2, 3	tendo1mulr 40760	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (𝑠 ∘ ( I ↾ 𝑇)) = 𝑠)
94	90, 92, 93	3eqtrd 2768	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸) → (𝑠 + ( I ↾ 𝑇)) = 𝑠)
95	7, 11, 15, 19, 26, 54, 68, 78, 79, 88, 94	isringd 20176	1 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5173   I cid 5513  ^◡ccnv 5618   ↾ cres 5621   ∘ ccom 5623  ‘cfv 6482  (class class class)co 7349   ∈ cmpo 7351  Basecbs 17120  +_gcplusg 17161  ._rcmulr 17162  Ringcrg 20118  HLchlt 39339  LHypclh 39973  LTrncltrn 40090  TEndoctendo 40741  EDRingcedring 40742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-riotaBAD 38942

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4859  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-undef 8206  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-map 8755  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-2 12191  df-3 12192  df-n0 12385  df-z 12472  df-uz 12736  df-fz 13411  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-plusg 17174  df-mulr 17175  df-0g 17345  df-proset 18200  df-poset 18219  df-plt 18234  df-lub 18250  df-glb 18251  df-join 18252  df-meet 18253  df-p0 18329  df-p1 18330  df-lat 18338  df-clat 18405  df-mgm 18514  df-sgrp 18593  df-mnd 18609  df-grp 18815  df-mgp 20026  df-ring 20120  df-oposet 39165  df-ol 39167  df-oml 39168  df-covers 39255  df-ats 39256  df-atl 39287  df-cvlat 39311  df-hlat 39340  df-llines 39487  df-lplanes 39488  df-lvols 39489  df-lines 39490  df-psubsp 39492  df-pmap 39493  df-padd 39785  df-lhyp 39977  df-laut 39978  df-ldil 40093  df-ltrn 40094  df-trl 40148  df-tendo 40744  df-edring 40746

This theorem is referenced by:  erngdvlem4  40980  eringring  40981