Theorem mapdrvallem2

Description: Lemma for mapdrval . TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015)

	Ref	Expression
Hypotheses	mapdrval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdrval.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	mapdrval.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdrval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapdrval.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	mapdrval.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	mapdrval.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	mapdrval.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	mapdrval.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
	mapdrval.c	⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
	mapdrval.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapdrval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
	mapdrval.e	⊢ ( 𝜑 → 𝑅 ⊆ 𝐶 )
	mapdrval.q	⊢ 𝑄 = ∪ ℎ ∈ 𝑅 ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) )
	mapdrval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	mapdrvallem2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
	mapdrvallem2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	mapdrvallem2.z	⊢ 0 = ( 0g ‘ 𝑈 )
	mapdrvallem2.y	⊢ 𝑌 = ( 0g ‘ 𝐷 )
Assertion	mapdrvallem2	⊢ ( 𝜑 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 } ⊆ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		mapdrval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdrval.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		mapdrval.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
4		mapdrval.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		mapdrval.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6		mapdrval.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		mapdrval.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
8		mapdrval.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
9		mapdrval.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
10		mapdrval.c	⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
11		mapdrval.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		mapdrval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
13		mapdrval.e	⊢ ( 𝜑 → 𝑅 ⊆ 𝐶 )
14		mapdrval.q	⊢ 𝑄 = ∪ ℎ ∈ 𝑅 ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) )
15		mapdrval.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
16		mapdrvallem2.a	⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
17		mapdrvallem2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
18		mapdrvallem2.z	⊢ 0 = ( 0g ‘ 𝑈 )
19		mapdrvallem2.y	⊢ 𝑌 = ( 0g ‘ 𝐷 )
20		eleq1	⊢ ( 𝑓 = 𝑌 → ( 𝑓 ∈ 𝑅 ↔ 𝑌 ∈ 𝑅 ) )
21	11	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
22	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23		simpl2	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ∈ 𝐶 )
24		simpr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ≠ 𝑌 )
25		eldifsn	⊢ ( 𝑓 ∈ ( 𝐶 ∖ { 𝑌 } ) ↔ ( 𝑓 ∈ 𝐶 ∧ 𝑓 ≠ 𝑌 ) )
26	23 24 25	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ∈ ( 𝐶 ∖ { 𝑌 } ) )
27	1 2 4 15 17 18 6 7 8 19 10 22 26	lcfl8b	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) )
28		simp1l3	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 )
29		eqimss2	⊢ ( ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
30	29	3ad2ant3	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
31	1 4 11	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
32	31	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑈 ∈ LMod )
33	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑈 ∈ LMod )
34	33	3ad2ant1	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑈 ∈ LMod )
35	22	3ad2ant1	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
36	10	lcfl1lem	⊢ ( 𝑓 ∈ 𝐶 ↔ ( 𝑓 ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) )
37	36	simplbi	⊢ ( 𝑓 ∈ 𝐶 → 𝑓 ∈ 𝐹 )
38	37	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑓 ∈ 𝐹 )
39	38	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ∈ 𝐹 )
40	39	3ad2ant1	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑓 ∈ 𝐹 )
41	15 6 7 34 40	lkrssv	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝐿 ‘ 𝑓 ) ⊆ 𝑉 )
42	1 4 15 5 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝑓 ) ⊆ 𝑉 ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ 𝑆 )
43	35 41 42	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ∈ 𝑆 )
44		eldifi	⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) → 𝑥 ∈ 𝑉 )
45	44	3ad2ant2	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑉 )
46	15 5 17 34 43 45	lspsnel5	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
47	30 46	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
48	28 47	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑄 )
49	48 14	eleqtrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑥 ∈ ∪ ℎ ∈ 𝑅 ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
50		eliun	⊢ ( 𝑥 ∈ ∪ ℎ ∈ 𝑅 ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ↔ ∃ ℎ ∈ 𝑅 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
51	49 50	sylib	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ∃ ℎ ∈ 𝑅 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
52		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
53		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
54		eqid	⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
55	1 4 11	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
56	55	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑈 ∈ LVec )
57	56	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑈 ∈ LVec )
58	57	3ad2ant1	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑈 ∈ LVec )
59	58	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑈 ∈ LVec )
60		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ℎ ∈ 𝑅 )
61		simp1l1	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝜑 )
62	61	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → 𝜑 )
63	62 13	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → 𝑅 ⊆ 𝐶 )
64	63	sseld	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ( ℎ ∈ 𝑅 → ℎ ∈ 𝐶 ) )
65	10	lcfl1lem	⊢ ( ℎ ∈ 𝐶 ↔ ( ℎ ∈ 𝐹 ∧ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) = ( 𝐿 ‘ ℎ ) ) )
66	65	simplbi	⊢ ( ℎ ∈ 𝐶 → ℎ ∈ 𝐹 )
67	64 66	syl6	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ( ℎ ∈ 𝑅 → ℎ ∈ 𝐹 ) )
68	60 67	mpd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ℎ ∈ 𝐹 )
69	68	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ℎ ∈ 𝐹 )
70	40	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑓 ∈ 𝐹 )
71		simpll3	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) )
72	34	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑈 ∈ LMod )
73	35	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
74	15 6 7 72 69	lkrssv	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐿 ‘ ℎ ) ⊆ 𝑉 )
75	1 4 15 5 2	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ ℎ ) ⊆ 𝑉 ) → ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ∈ 𝑆 )
76	73 74 75	syl2anc	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ∈ 𝑆 )
77		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
78	5 17 72 76 77	lspsnel5a	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
79		simpll2	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑥 ∈ ( 𝑉 ∖ { 0 } ) )
80	15 17 18 16 72 79	lsatlspsn	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑁 ‘ { 𝑥 } ) ∈ 𝐴 )
81	1 2 4 18 16 6 7 73 69	dochsat0	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ∈ 𝐴 ∨ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) = { 0 } ) )
82	18 16 59 80 81	lsatcmp2	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( ( 𝑁 ‘ { 𝑥 } ) ⊆ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ↔ ( 𝑁 ‘ { 𝑥 } ) = ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) )
83	78 82	mpbid	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑁 ‘ { 𝑥 } ) = ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) )
84	71 83	eqtr2d	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
85		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
86	61 13	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑅 ⊆ 𝐶 )
87	86	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ℎ ∈ 𝐶 )
88	87	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ℎ ∈ 𝐶 )
89	1 85 2 4 6 7 10 73 69	lcfl5	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( ℎ ∈ 𝐶 ↔ ( 𝐿 ‘ ℎ ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
90	88 89	mpbid	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐿 ‘ ℎ ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
91		simp1l2	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑓 ∈ 𝐶 )
92	91	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → 𝑓 ∈ 𝐶 )
93	1 85 2 4 6 7 10 73 70	lcfl5	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝑓 ∈ 𝐶 ↔ ( 𝐿 ‘ 𝑓 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
94	92 93	mpbid	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐿 ‘ 𝑓 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
95	1 85 2 73 90 94	doch11	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ↔ ( 𝐿 ‘ ℎ ) = ( 𝐿 ‘ 𝑓 ) ) )
96	84 95	mpbid	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ( 𝐿 ‘ ℎ ) = ( 𝐿 ‘ 𝑓 ) )
97	52 53 6 7 8 54 59 69 70 96	eqlkr4	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) ∧ 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) )
98	97	ex	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) ∧ ℎ ∈ 𝑅 ) → ( 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ) )
99	98	reximdva	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( ∃ ℎ ∈ 𝑅 𝑥 ∈ ( 𝑂 ‘ ( 𝐿 ‘ ℎ ) ) → ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ) )
100	51 99	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) )
101		eleq1	⊢ ( 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) → ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) )
102	101	reximi	⊢ ( ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) )
103	102	reximi	⊢ ( ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) → ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) )
104		rexcom	⊢ ( ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ↔ ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ∈ 𝑅 ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) )
105		df-rex	⊢ ( ∃ ℎ ∈ 𝑅 ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ↔ ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
106	105	rexbii	⊢ ( ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ∈ 𝑅 ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ↔ ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
107	104 106	bitri	⊢ ( ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ↔ ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
108	103 107	sylib	⊢ ( ∃ ℎ ∈ 𝑅 ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑓 = ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
109	100 108	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) )
110	33	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → 𝑈 ∈ LMod )
111	12	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑅 ∈ 𝑇 )
112	111	adantr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑅 ∈ 𝑇 )
113	112	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → 𝑅 ∈ 𝑇 )
114		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
115		simprl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → ℎ ∈ 𝑅 )
116	52 53 8 54 9 110 113 114 115	ldualssvscl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 )
117		biimpr	⊢ ( ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 → 𝑓 ∈ 𝑅 ) )
118	117	ad2antll	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 → 𝑓 ∈ 𝑅 ) )
119	116 118	mpd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) ∧ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) ) → 𝑓 ∈ 𝑅 )
120	119	ex	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) → 𝑓 ∈ 𝑅 ) )
121	120	exlimdv	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ( ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) → 𝑓 ∈ 𝑅 ) )
122	121	rexlimdva	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → ( ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) → 𝑓 ∈ 𝑅 ) )
123	122	3ad2ant1	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → ( ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ∃ ℎ ( ℎ ∈ 𝑅 ∧ ( 𝑓 ∈ 𝑅 ↔ ( 𝑟 ( ·𝑠 ‘ 𝐷 ) ℎ ) ∈ 𝑅 ) ) → 𝑓 ∈ 𝑅 ) )
124	109 123	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) ) → 𝑓 ∈ 𝑅 )
125	124	rexlimdv3a	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) = ( 𝑁 ‘ { 𝑥 } ) → 𝑓 ∈ 𝑅 ) )
126	27 125	mpd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) ∧ 𝑓 ≠ 𝑌 ) → 𝑓 ∈ 𝑅 )
127	8 31	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
128	127	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝐷 ∈ LMod )
129	19 9	lss0cl	⊢ ( ( 𝐷 ∈ LMod ∧ 𝑅 ∈ 𝑇 ) → 𝑌 ∈ 𝑅 )
130	128 111 129	syl2anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑌 ∈ 𝑅 )
131	20 126 130	pm2.61ne	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐶 ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 ) → 𝑓 ∈ 𝑅 )
132	131	rabssdv	⊢ ( 𝜑 → { 𝑓 ∈ 𝐶 ∣ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑄 } ⊆ 𝑅 )