Theorem dih1dimatlem 42123

Description: Lemma for dih1dimat 42124. (Contributed by NM, 10-Apr-2014.)

Hypotheses

Ref	Expression
dih1dimat.h	⊢ 𝐻 = (LHyp‘𝐾)
dih1dimat.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dih1dimat.i	⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dih1dimat.a	⊢ 𝐴 = (LSAtoms‘𝑈)
dih1dimat.b	⊢ 𝐵 = (Base‘𝐾)
dih1dimat.l	⊢ ≤ = (le‘𝐾)
dih1dimat.c	⊢ 𝐶 = (Atoms‘𝐾)
dih1dimat.p	⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
dih1dimat.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
dih1dimat.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
dih1dimat.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
dih1dimat.o	⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
dih1dimat.d	⊢ 𝐹 = (Scalar‘𝑈)
dih1dimat.j	⊢ 𝐽 = (invr‘𝐹)
dih1dimat.v	⊢ 𝑉 = (Base‘𝑈)
dih1dimat.m	⊢ · = ( ·𝑠 ‘𝑈)
dih1dimat.s	⊢ 𝑆 = (LSubSp‘𝑈)
dih1dimat.n	⊢ 𝑁 = (LSpan‘𝑈)
dih1dimat.z	⊢ 0 = (0g‘𝑈)
dih1dimat.g	⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = (((𝐽‘𝑠)‘𝑓)‘𝑃))

Assertion

Ref	Expression
dih1dimatlem	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝐴) → 𝐷 ∈ ran 𝐼)

Distinct variable groups:   ≤ ,ℎ   𝐵,ℎ   𝑓,𝑠,𝐸   𝐶,ℎ   ℎ,𝐽   𝑓,𝑁,𝑠   𝑓,ℎ,𝐾,𝑠   𝑇,𝑓,ℎ,𝑠   𝑈,𝑓,ℎ,𝑠   𝑓,𝐻,ℎ,𝑠   𝑓,𝑉,𝑠   𝑓,𝑊,ℎ,𝑠   𝑓,𝐼,𝑠   𝑃,ℎ

Allowed substitution hints:   𝐴(𝑓,ℎ,𝑠)   𝐵(𝑓,𝑠)   𝐶(𝑓,𝑠)   𝐷(𝑓,ℎ,𝑠)   𝑃(𝑓,𝑠)   𝑅(𝑓,ℎ,𝑠)   𝑆(𝑓,ℎ,𝑠)   · (𝑓,ℎ,𝑠)   𝐸(ℎ)   𝐹(𝑓,ℎ,𝑠)   𝐺(𝑓,ℎ,𝑠)   𝐼(ℎ)   𝐽(𝑓,𝑠)   ≤ (𝑓,𝑠)   𝑁(ℎ)   𝑂(𝑓,ℎ,𝑠)   𝑉(ℎ)   0 (𝑓,ℎ,𝑠)

Proof of Theorem dih1dimatlem

Dummy variables 𝑣 𝑔 𝑖 𝑝 𝑟 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dih1dimat.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
2		dih1dimat.u	. . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
3		id 23	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4	1, 2, 3	dvhlvec 41903	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec)
5		dih1dimat.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
6		dih1dimat.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
7		dih1dimat.z	. . . . 5 ⊢ 0 = (0g‘𝑈)
8		dih1dimat.a	. . . . 5 ⊢ 𝐴 = (LSAtoms‘𝑈)
9	5, 6, 7, 8	islsat 39785	. . . 4 ⊢ (𝑈 ∈ LVec → (𝐷 ∈ 𝐴 ↔ ∃𝑣 ∈ (𝑉 ∖ { 0 })𝐷 = (𝑁‘{𝑣})))
10	4, 9	syl 18	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐷 ∈ 𝐴 ↔ ∃𝑣 ∈ (𝑉 ∖ { 0 })𝐷 = (𝑁‘{𝑣})))
11	10	biimpa 481	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝐴) → ∃𝑣 ∈ (𝑉 ∖ { 0 })𝐷 = (𝑁‘{𝑣}))
12		eldifi 4085	. . . . . . . 8 ⊢ (𝑣 ∈ (𝑉 ∖ { 0 }) → 𝑣 ∈ 𝑉)
13		dih1dimat.t	. . . . . . . . . 10 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
14		dih1dimat.e	. . . . . . . . . 10 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
15	1, 13, 14, 2, 5	dvhvbase 41881	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑉 = (𝑇 × 𝐸))
16	15	eleq2d 2849	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ (𝑇 × 𝐸)))
17	12, 16	imbitrid 247	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑣 ∈ (𝑉 ∖ { 0 }) → 𝑣 ∈ (𝑇 × 𝐸)))
18	17	imp 411	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑣 ∈ (𝑉 ∖ { 0 })) → 𝑣 ∈ (𝑇 × 𝐸))
19		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 = 𝑂) → 𝑠 = 𝑂)
20	19	opeq2d 4845	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 = 𝑂) → ⟨𝑓, 𝑠⟩ = ⟨𝑓, 𝑂⟩)
21	20	sneqd 4601	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 = 𝑂) → {⟨𝑓, 𝑠⟩} = {⟨𝑓, 𝑂⟩})
22	21	fveq2d 6885	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 = 𝑂) → (𝑁‘{⟨𝑓, 𝑠⟩}) = (𝑁‘{⟨𝑓, 𝑂⟩}))
23		simpl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
24		dih1dimat.b	. . . . . . . . . . . . . . . . 17 ⊢ 𝐵 = (Base‘𝐾)
25		dih1dimat.r	. . . . . . . . . . . . . . . . 17 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
26	24, 1, 13, 25	trlcl 40958	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → (𝑅‘𝑓) ∈ 𝐵)
27		dih1dimat.l	. . . . . . . . . . . . . . . . 17 ⊢ ≤ = (le‘𝐾)
28	27, 1, 13, 25	trlle 40978	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → (𝑅‘𝑓) ≤ 𝑊)
29		dih1dimat.i	. . . . . . . . . . . . . . . . 17 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊)
30		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ ((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊)
31	24, 27, 1, 29, 30	dihvalb 42031	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑅‘𝑓) ∈ 𝐵 ∧ (𝑅‘𝑓) ≤ 𝑊)) → (𝐼‘(𝑅‘𝑓)) = (((DIsoB‘𝐾)‘𝑊)‘(𝑅‘𝑓)))
32	23, 26, 28, 31	syl12anc 849	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → (𝐼‘(𝑅‘𝑓)) = (((DIsoB‘𝐾)‘𝑊)‘(𝑅‘𝑓)))
33		dih1dimat.o	. . . . . . . . . . . . . . . 16 ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
34	24, 1, 13, 25, 33, 2, 30, 6	dib1dim2 41962	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → (((DIsoB‘𝐾)‘𝑊)‘(𝑅‘𝑓)) = (𝑁‘{⟨𝑓, 𝑂⟩}))
35	32, 34	eqtr2d 2799	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → (𝑁‘{⟨𝑓, 𝑂⟩}) = (𝐼‘(𝑅‘𝑓)))
36		dih1dimat.s	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (LSubSp‘𝑈)
37	24, 1, 29, 2, 36	dihf11 42061	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:𝐵–1-1→𝑆)
38	37	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → 𝐼:𝐵–1-1→𝑆)
39		f1fn 6775	. . . . . . . . . . . . . . . 16 ⊢ (𝐼:𝐵–1-1→𝑆 → 𝐼 Fn 𝐵)
40	38, 39	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → 𝐼 Fn 𝐵)
41		fnfvelrn 7075	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 Fn 𝐵 ∧ (𝑅‘𝑓) ∈ 𝐵) → (𝐼‘(𝑅‘𝑓)) ∈ ran 𝐼)
42	40, 26, 41	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → (𝐼‘(𝑅‘𝑓)) ∈ ran 𝐼)
43	35, 42	eqeltrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑓 ∈ 𝑇) → (𝑁‘{⟨𝑓, 𝑂⟩}) ∈ ran 𝐼)
44	43	adantrr 729	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑁‘{⟨𝑓, 𝑂⟩}) ∈ ran 𝐼)
45	44	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 = 𝑂) → (𝑁‘{⟨𝑓, 𝑂⟩}) ∈ ran 𝐼)
46	22, 45	eqeltrd 2863	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 = 𝑂) → (𝑁‘{⟨𝑓, 𝑠⟩}) ∈ ran 𝐼)
47		simpll 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
48		dih1dimat.d	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (Scalar‘𝑈)
49		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝐹) = (Base‘𝐹)
50	1, 14, 2, 48, 49	dvhbase 41877	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝐹) = 𝐸)
51	47, 50	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (Base‘𝐹) = 𝐸)
52	51	rexeqdv 3324	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (∃𝑡 ∈ (Base‘𝐹)𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩) ↔ ∃𝑡 ∈ 𝐸 𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩)))
53		simplll 786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
54		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → 𝑡 ∈ 𝐸)
55		opelxpi 5698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) → ⟨𝑓, 𝑠⟩ ∈ (𝑇 × 𝐸))
56	55	ad3antlr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → ⟨𝑓, 𝑠⟩ ∈ (𝑇 × 𝐸))
57		dih1dimat.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ · = ( ·𝑠 ‘𝑈)
58	1, 13, 14, 2, 57	dvhvscacl 41897	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ ⟨𝑓, 𝑠⟩ ∈ (𝑇 × 𝐸))) → (𝑡 · ⟨𝑓, 𝑠⟩) ∈ (𝑇 × 𝐸))
59	53, 54, 56, 58	syl12anc 849	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → (𝑡 · ⟨𝑓, 𝑠⟩) ∈ (𝑇 × 𝐸))
60		eleq1a 2858	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 · ⟨𝑓, 𝑠⟩) ∈ (𝑇 × 𝐸) → (𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩) → 𝑢 ∈ (𝑇 × 𝐸)))
61	59, 60	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → (𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩) → 𝑢 ∈ (𝑇 × 𝐸)))
62	61	rexlimdva 3166	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (∃𝑡 ∈ 𝐸 𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩) → 𝑢 ∈ (𝑇 × 𝐸)))
63	62	pm4.71rd 571	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (∃𝑡 ∈ 𝐸 𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩) ↔ (𝑢 ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩))))
64		simplrl 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝑓 ∈ 𝑇)
65	64	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → 𝑓 ∈ 𝑇)
66		simplrr 789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝑠 ∈ 𝐸)
67	66	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → 𝑠 ∈ 𝐸)
68	1, 13, 14, 2, 57	dvhopvsca 41896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑡 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑡 · ⟨𝑓, 𝑠⟩) = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩)
69	53, 54, 65, 67, 68	syl13anc 1399	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → (𝑡 · ⟨𝑓, 𝑠⟩) = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩)
70	69	eqeq2d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) ∧ 𝑡 ∈ 𝐸) → (𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩) ↔ 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩))
71	70	rexbidva 3187	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (∃𝑡 ∈ 𝐸 𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩) ↔ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩))
72	71	anbi2d 641	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → ((𝑢 ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩)) ↔ (𝑢 ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩)))
73	52, 63, 72	3bitrd 308	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (∃𝑡 ∈ (Base‘𝐹)𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩) ↔ (𝑢 ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩)))
74	73	abbidv 2829	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → {𝑢 ∣ ∃𝑡 ∈ (Base‘𝐹)𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩)} = {𝑢 ∣ (𝑢 ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩)})
75		df-rab 3417	. . . . . . . . . . . . . 14 ⊢ {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩} = {𝑢 ∣ (𝑢 ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩)}
76	74, 75	eqtr4di 2816	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → {𝑢 ∣ ∃𝑡 ∈ (Base‘𝐹)𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩)} = {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩})
77		ssrab2 4034	. . . . . . . . . . . . . . 15 ⊢ {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩} ⊆ (𝑇 × 𝐸)
78		relxp 5679	. . . . . . . . . . . . . . 15 ⊢ Rel (𝑇 × 𝐸)
79		relss 5768	. . . . . . . . . . . . . . 15 ⊢ ({𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩} ⊆ (𝑇 × 𝐸) → (Rel (𝑇 × 𝐸) → Rel {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩}))
80	77, 78, 79	mp2 9	. . . . . . . . . . . . . 14 ⊢ Rel {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩}
81		relopabv 5808	. . . . . . . . . . . . . 14 ⊢ Rel {⟨𝑔, 𝑟⟩ ∣ (𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)}
82		vex 3459	. . . . . . . . . . . . . . . 16 ⊢ 𝑖 ∈ V
83		vex 3459	. . . . . . . . . . . . . . . 16 ⊢ 𝑝 ∈ V
84		eqeq1 2767	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝑖 → (𝑔 = (𝑟‘𝐺) ↔ 𝑖 = (𝑟‘𝐺)))
85	84	anbi1d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = 𝑖 → ((𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸) ↔ (𝑖 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)))
86		fveq1 6880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑝 → (𝑟‘𝐺) = (𝑝‘𝐺))
87	86	eqeq2d 2774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑝 → (𝑖 = (𝑟‘𝐺) ↔ 𝑖 = (𝑝‘𝐺)))
88		eleq1w 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑝 → (𝑟 ∈ 𝐸 ↔ 𝑝 ∈ 𝐸))
89	87, 88	anbi12d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑝 → ((𝑖 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸) ↔ (𝑖 = (𝑝‘𝐺) ∧ 𝑝 ∈ 𝐸)))
90	82, 83, 85, 89	opelopab 5527	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑖, 𝑝⟩ ∈ {⟨𝑔, 𝑟⟩ ∣ (𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)} ↔ (𝑖 = (𝑝‘𝐺) ∧ 𝑝 ∈ 𝐸))
91		dih1dimat.c	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐶 = (Atoms‘𝐾)
92		dih1dimat.p	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
93		dih1dimat.j	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐽 = (invr‘𝐹)
94		dih1dimat.g	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = (((𝐽‘𝑠)‘𝑓)‘𝑃))
95	1, 2, 29, 8, 24, 27, 91, 92, 13, 25, 14, 33, 48, 93, 5, 57, 36, 6, 7, 94	dih1dimatlem0 42122	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ 𝑠 ≠ 𝑂) → ((𝑖 = (𝑝‘𝐺) ∧ 𝑝 ∈ 𝐸) ↔ ((𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸) ∧ ∃𝑡 ∈ 𝐸 (𝑖 = (𝑡‘𝑓) ∧ 𝑝 = (𝑡 ∘ 𝑠)))))
96	95	3expa 1136	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → ((𝑖 = (𝑝‘𝐺) ∧ 𝑝 ∈ 𝐸) ↔ ((𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸) ∧ ∃𝑡 ∈ 𝐸 (𝑖 = (𝑡‘𝑓) ∧ 𝑝 = (𝑡 ∘ 𝑠)))))
97		opelxp 5697	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑖, 𝑝⟩ ∈ (𝑇 × 𝐸) ↔ (𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸))
98	82, 83	opth 5458	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑖, 𝑝⟩ = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩ ↔ (𝑖 = (𝑡‘𝑓) ∧ 𝑝 = (𝑡 ∘ 𝑠)))
99	98	rexbii 3112	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑡 ∈ 𝐸 ⟨𝑖, 𝑝⟩ = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩ ↔ ∃𝑡 ∈ 𝐸 (𝑖 = (𝑡‘𝑓) ∧ 𝑝 = (𝑡 ∘ 𝑠)))
100	97, 99	anbi12i 639	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑖, 𝑝⟩ ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 ⟨𝑖, 𝑝⟩ = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩) ↔ ((𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸) ∧ ∃𝑡 ∈ 𝐸 (𝑖 = (𝑡‘𝑓) ∧ 𝑝 = (𝑡 ∘ 𝑠))))
101	96, 100	bitr4di 292	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → ((𝑖 = (𝑝‘𝐺) ∧ 𝑝 ∈ 𝐸) ↔ (⟨𝑖, 𝑝⟩ ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 ⟨𝑖, 𝑝⟩ = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩)))
102		eqeq1 2767	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = ⟨𝑖, 𝑝⟩ → (𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩ ↔ ⟨𝑖, 𝑝⟩ = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩))
103	102	rexbidv 3189	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = ⟨𝑖, 𝑝⟩ → (∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩ ↔ ∃𝑡 ∈ 𝐸 ⟨𝑖, 𝑝⟩ = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩))
104	103	elrab 3650	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑖, 𝑝⟩ ∈ {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩} ↔ (⟨𝑖, 𝑝⟩ ∈ (𝑇 × 𝐸) ∧ ∃𝑡 ∈ 𝐸 ⟨𝑖, 𝑝⟩ = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩))
105	101, 104	bitr4di 292	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → ((𝑖 = (𝑝‘𝐺) ∧ 𝑝 ∈ 𝐸) ↔ ⟨𝑖, 𝑝⟩ ∈ {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩}))
106	90, 105	bitr2id 287	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (⟨𝑖, 𝑝⟩ ∈ {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩} ↔ ⟨𝑖, 𝑝⟩ ∈ {⟨𝑔, 𝑟⟩ ∣ (𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)}))
107	80, 81, 106	eqrelrdv 5778	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → {𝑢 ∈ (𝑇 × 𝐸) ∣ ∃𝑡 ∈ 𝐸 𝑢 = ⟨(𝑡‘𝑓), (𝑡 ∘ 𝑠)⟩} = {⟨𝑔, 𝑟⟩ ∣ (𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)})
108	76, 107	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → {𝑢 ∣ ∃𝑡 ∈ (Base‘𝐹)𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩)} = {⟨𝑔, 𝑟⟩ ∣ (𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)})
109	1, 2, 47	dvhlmod 41904	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝑈 ∈ LMod)
110	1, 13, 14, 2, 5	dvhelvbasei 41882	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → ⟨𝑓, 𝑠⟩ ∈ 𝑉)
111	110	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → ⟨𝑓, 𝑠⟩ ∈ 𝑉)
112	48, 49, 5, 57, 6	lspsn 21123	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ LMod ∧ ⟨𝑓, 𝑠⟩ ∈ 𝑉) → (𝑁‘{⟨𝑓, 𝑠⟩}) = {𝑢 ∣ ∃𝑡 ∈ (Base‘𝐹)𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩)})
113	109, 111, 112	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝑁‘{⟨𝑓, 𝑠⟩}) = {𝑢 ∣ ∃𝑡 ∈ (Base‘𝐹)𝑢 = (𝑡 · ⟨𝑓, 𝑠⟩)})
114		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝑠 ≠ 𝑂)
115	24, 1, 13, 14, 33, 2, 48, 93	tendoinvcl 41898	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂) → ((𝐽‘𝑠) ∈ 𝐸 ∧ (𝐽‘𝑠) ≠ 𝑂))
116	115	simpld 499	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐸 ∧ 𝑠 ≠ 𝑂) → (𝐽‘𝑠) ∈ 𝐸)
117	47, 66, 114, 116	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝐽‘𝑠) ∈ 𝐸)
118	1, 13, 14	tendocl 41561	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐽‘𝑠) ∈ 𝐸 ∧ 𝑓 ∈ 𝑇) → ((𝐽‘𝑠)‘𝑓) ∈ 𝑇)
119	47, 117, 64, 118	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → ((𝐽‘𝑠)‘𝑓) ∈ 𝑇)
120	27, 91, 1, 92	lhpocnel2 40813	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊))
121	47, 120	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊))
122	27, 91, 1, 13	ltrnel 40933	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐽‘𝑠)‘𝑓) ∈ 𝑇 ∧ (𝑃 ∈ 𝐶 ∧ ¬ 𝑃 ≤ 𝑊)) → ((((𝐽‘𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽‘𝑠)‘𝑓)‘𝑃) ≤ 𝑊))
123	47, 119, 121, 122	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → ((((𝐽‘𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽‘𝑠)‘𝑓)‘𝑃) ≤ 𝑊))
124		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ((DIsoC‘𝐾)‘𝑊) = ((DIsoC‘𝐾)‘𝑊)
125	27, 91, 1, 124, 29	dihvalcqat 42033	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((((𝐽‘𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽‘𝑠)‘𝑓)‘𝑃) ≤ 𝑊)) → (𝐼‘(((𝐽‘𝑠)‘𝑓)‘𝑃)) = (((DIsoC‘𝐾)‘𝑊)‘(((𝐽‘𝑠)‘𝑓)‘𝑃)))
126	47, 123, 125	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝐼‘(((𝐽‘𝑠)‘𝑓)‘𝑃)) = (((DIsoC‘𝐾)‘𝑊)‘(((𝐽‘𝑠)‘𝑓)‘𝑃)))
127	27, 91, 1, 92, 13, 14, 124, 94	dicval2 41973	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((((𝐽‘𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽‘𝑠)‘𝑓)‘𝑃) ≤ 𝑊)) → (((DIsoC‘𝐾)‘𝑊)‘(((𝐽‘𝑠)‘𝑓)‘𝑃)) = {⟨𝑔, 𝑟⟩ ∣ (𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)})
128	47, 123, 127	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (((DIsoC‘𝐾)‘𝑊)‘(((𝐽‘𝑠)‘𝑓)‘𝑃)) = {⟨𝑔, 𝑟⟩ ∣ (𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)})
129	126, 128	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝐼‘(((𝐽‘𝑠)‘𝑓)‘𝑃)) = {⟨𝑔, 𝑟⟩ ∣ (𝑔 = (𝑟‘𝐺) ∧ 𝑟 ∈ 𝐸)})
130	108, 113, 129	3eqtr4d 2808	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝑁‘{⟨𝑓, 𝑠⟩}) = (𝐼‘(((𝐽‘𝑠)‘𝑓)‘𝑃)))
131	24, 1, 29	dihfn 42062	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼 Fn 𝐵)
132	131	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → 𝐼 Fn 𝐵)
133	132	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝐼 Fn 𝐵)
134		simplll 786	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝐾 ∈ HL)
135		hlop 40156	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
136	134, 135	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝐾 ∈ OP)
137	24, 1	lhpbase 40792	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
138	137	ad3antlr 743	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝑊 ∈ 𝐵)
139		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (oc‘𝐾) = (oc‘𝐾)
140	24, 139	opoccl 39988	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵) → ((oc‘𝐾)‘𝑊) ∈ 𝐵)
141	136, 138, 140	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → ((oc‘𝐾)‘𝑊) ∈ 𝐵)
142	92, 141	eqeltrid 2867	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → 𝑃 ∈ 𝐵)
143	24, 1, 13	ltrncl 40919	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐽‘𝑠)‘𝑓) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (((𝐽‘𝑠)‘𝑓)‘𝑃) ∈ 𝐵)
144	47, 119, 142, 143	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (((𝐽‘𝑠)‘𝑓)‘𝑃) ∈ 𝐵)
145		fnfvelrn 7075	. . . . . . . . . . . 12 ⊢ ((𝐼 Fn 𝐵 ∧ (((𝐽‘𝑠)‘𝑓)‘𝑃) ∈ 𝐵) → (𝐼‘(((𝐽‘𝑠)‘𝑓)‘𝑃)) ∈ ran 𝐼)
146	133, 144, 145	syl2anc 595	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝐼‘(((𝐽‘𝑠)‘𝑓)‘𝑃)) ∈ ran 𝐼)
147	130, 146	eqeltrd 2863	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) ∧ 𝑠 ≠ 𝑂) → (𝑁‘{⟨𝑓, 𝑠⟩}) ∈ ran 𝐼)
148	46, 147	pm2.61dane 3045	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸)) → (𝑁‘{⟨𝑓, 𝑠⟩}) ∈ ran 𝐼)
149	148	ralrimivva 3208	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∀𝑓 ∈ 𝑇 ∀𝑠 ∈ 𝐸 (𝑁‘{⟨𝑓, 𝑠⟩}) ∈ ran 𝐼)
150		sneq 4599	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑓, 𝑠⟩ → {𝑣} = {⟨𝑓, 𝑠⟩})
151	150	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑓, 𝑠⟩ → (𝑁‘{𝑣}) = (𝑁‘{⟨𝑓, 𝑠⟩}))
152	151	eleq1d 2848	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑓, 𝑠⟩ → ((𝑁‘{𝑣}) ∈ ran 𝐼 ↔ (𝑁‘{⟨𝑓, 𝑠⟩}) ∈ ran 𝐼))
153	152	ralxp 5827	. . . . . . . 8 ⊢ (∀𝑣 ∈ (𝑇 × 𝐸)(𝑁‘{𝑣}) ∈ ran 𝐼 ↔ ∀𝑓 ∈ 𝑇 ∀𝑠 ∈ 𝐸 (𝑁‘{⟨𝑓, 𝑠⟩}) ∈ ran 𝐼)
154	149, 153	sylibr 237	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∀𝑣 ∈ (𝑇 × 𝐸)(𝑁‘{𝑣}) ∈ ran 𝐼)
155	154	r19.21bi 3257	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑣 ∈ (𝑇 × 𝐸)) → (𝑁‘{𝑣}) ∈ ran 𝐼)
156	18, 155	syldan 602	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑣 ∈ (𝑉 ∖ { 0 })) → (𝑁‘{𝑣}) ∈ ran 𝐼)
157		eleq1a 2858	. . . . 5 ⊢ ((𝑁‘{𝑣}) ∈ ran 𝐼 → (𝐷 = (𝑁‘{𝑣}) → 𝐷 ∈ ran 𝐼))
158	156, 157	syl 18	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑣 ∈ (𝑉 ∖ { 0 })) → (𝐷 = (𝑁‘{𝑣}) → 𝐷 ∈ ran 𝐼))
159	158	rexlimdva 3166	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (∃𝑣 ∈ (𝑉 ∖ { 0 })𝐷 = (𝑁‘{𝑣}) → 𝐷 ∈ ran 𝐼))
160	159	adantr 485	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝐴) → (∃𝑣 ∈ (𝑉 ∖ { 0 })𝐷 = (𝑁‘{𝑣}) → 𝐷 ∈ ran 𝐼))
161	11, 160	mpd 16	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝐴) → 𝐷 ∈ ran 𝐼)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  {cab 2741   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  {crab 3416   ∖ cdif 3902   ⊆ wss 3905  {csn 4589  ⟨cop 4595   class class class wbr 5109  {copab 5173   ↦ cmpt 5192   I cid 5555   × cxp 5659  ran crn 5662   ↾ cres 5663   ∘ ccom 5665  Rel wrel 5666   Fn wfn 6531  –1-1→wf1 6533  ‘cfv 6536  ℩crio 7366  (class class class)co 7410  Basecbs 17264  Scalarcsca 17308   ·_𝑠 cvsca 17309  lecple 17312  occoc 17313  0_gc0g 17487  inv_rcinvr 20465  LModclmod 20981  LSubSpclss 21052  LSpanclspn 21092  LVecclvec 21223  LSAtomsclsa 39768  OPcops 39966  Atomscatm 40057  HLchlt 40144  LHypclh 40778  LTrncltrn 40895  trLctrl 40952  TEndoctendo 41546  DVecHcdvh 41872  DIsoBcdib 41932  DIsoCcdic 41966  DIsoHcdih 42022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-riotaBAD 39747

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-tpos 8218  df-undef 8265  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-er 8690  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-n0 12500  df-z 12587  df-uz 12858  df-fz 13531  df-struct 17202  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-ress 17286  df-plusg 17318  df-mulr 17319  df-sca 17321  df-vsca 17322  df-0g 17489  df-proset 18345  df-poset 18364  df-plt 18379  df-lub 18395  df-glb 18396  df-join 18397  df-meet 18398  df-p0 18474  df-p1 18475  df-lat 18483  df-clat 18550  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-submnd 18837  df-grp 18998  df-minusg 18999  df-sbg 19000  df-subg 19184  df-cntz 19382  df-lsm 19701  df-cmn 19847  df-abl 19848  df-mgp 20212  df-rng 20226  df-ur 20259  df-ring 20312  df-oppr 20415  df-dvdsr 20435  df-unit 20436  df-invr 20466  df-dvr 20479  df-drng 20829  df-lmod 20983  df-lss 21053  df-lsp 21093  df-lvec 21224  df-lsatoms 39770  df-oposet 39970  df-ol 39972  df-oml 39973  df-covers 40060  df-ats 40061  df-atl 40092  df-cvlat 40116  df-hlat 40145  df-llines 40292  df-lplanes 40293  df-lvols 40294  df-lines 40295  df-psubsp 40297  df-pmap 40298  df-padd 40590  df-lhyp 40782  df-laut 40783  df-ldil 40898  df-ltrn 40899  df-trl 40953  df-tendo 41549  df-edring 41551  df-disoa 41823  df-dvech 41873  df-dib 41933  df-dic 41967  df-dih 42023

This theorem is referenced by:  dih1dimat  42124