Metamath Proof Explorer

Theorem diclspsn

Description: The value of isomorphism C is spanned by vector F . Part of proof of Lemma N of Crawley p. 121 line 29. (Contributed by NM, 21-Feb-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses diclspsn.l ⊢ ≤ = ( le ‘ 𝐾 )
diclspsn.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
diclspsn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
diclspsn.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
diclspsn.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
diclspsn.i ⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
diclspsn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
diclspsn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
diclspsn.f ⊢ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
Assertion diclspsn ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) )

Proof

Step Hyp Ref Expression
1 diclspsn.l ⊢ ≤ = ( le ‘ 𝐾 )
2 diclspsn.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 diclspsn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 diclspsn.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5 diclspsn.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 diclspsn.i ⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
7 diclspsn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 diclspsn.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
9 diclspsn.f ⊢ 𝐹 = ( ℩ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑃 ) = 𝑄 )
10 df-rab ⊢ { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } = { 𝑣 ∣ ( 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) }
11 relopabv ⊢ Rel { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 = ( 𝑧 ‘ 𝐹 ) ∧ 𝑧 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) }
12 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
13 1 2 3 4 5 12 6 9 dicval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 = ( 𝑧 ‘ 𝐹 ) ∧ 𝑧 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } )
14 13 releqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( Rel ( 𝐼 ‘ 𝑄 ) ↔ Rel { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 = ( 𝑧 ‘ 𝐹 ) ∧ 𝑧 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) } ) )
15 11 14 mpbiri ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → Rel ( 𝐼 ‘ 𝑄 ) )
16 ssrab2 ⊢ { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } ⊆ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
17 relxp ⊢ Rel ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
18 relss ⊢ ( { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } ⊆ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( Rel ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → Rel { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } ) )
19 16 17 18 mp2 ⊢ Rel { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) }
20 19 a1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → Rel { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } )
21 id ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
22 vex ⊢ 𝑔 ∈ V
23 vex ⊢ 𝑠 ∈ V
24 1 2 3 4 5 12 6 9 22 23 dicopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑔 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
25 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → 𝑔 = ( 𝑠 ‘ 𝐹 ) )
26 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
27 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
28 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
29 1 2 3 4 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
30 29 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
31 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
32 1 2 3 5 9 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
33 28 30 31 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
34 33 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → 𝐹 ∈ 𝑇 )
35 3 5 12 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
36 26 27 34 35 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑠 ‘ 𝐹 ) ∈ 𝑇 )
37 25 36 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → 𝑔 ∈ 𝑇 )
38 37 27 25 3jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
39 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) ) → 𝑔 = ( 𝑠 ‘ 𝐹 ) )
40 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) ) → 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
41 39 40 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) ) → ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
42 38 41 impbida ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) ) )
43 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
44 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
45 3 12 7 43 44 dvhbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
46 45 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
47 46 rexeqdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) )
48 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
49 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
50 33 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
51 3 5 12 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
52 51 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
53 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
54 3 5 12 7 53 dvhopvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) = ⟨ ( 𝑥 ‘ 𝐹 ) , ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ⟩ )
55 48 49 50 52 54 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) = ⟨ ( 𝑥 ‘ 𝐹 ) , ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ⟩ )
56 55 eqeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ⟨ 𝑔 , 𝑠 ⟩ = ⟨ ( 𝑥 ‘ 𝐹 ) , ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ⟩ ) )
57 22 23 opth ⊢ ( ⟨ 𝑔 , 𝑠 ⟩ = ⟨ ( 𝑥 ‘ 𝐹 ) , ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ⟩ ↔ ( 𝑔 = ( 𝑥 ‘ 𝐹 ) ∧ 𝑠 = ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ) )
58 56 57 bitrdi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ( 𝑔 = ( 𝑥 ‘ 𝐹 ) ∧ 𝑠 = ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ) ) )
59 3 5 12 tendo1mulr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ∘ ( I ↾ 𝑇 ) ) = 𝑥 )
60 59 adantlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ∘ ( I ↾ 𝑇 ) ) = 𝑥 )
61 60 eqeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑠 = ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ↔ 𝑠 = 𝑥 ) )
62 equcom ⊢ ( 𝑠 = 𝑥 ↔ 𝑥 = 𝑠 )
63 61 62 bitrdi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑠 = ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ↔ 𝑥 = 𝑠 ) )
64 63 anbi2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑔 = ( 𝑥 ‘ 𝐹 ) ∧ 𝑠 = ( 𝑥 ∘ ( I ↾ 𝑇 ) ) ) ↔ ( 𝑔 = ( 𝑥 ‘ 𝐹 ) ∧ 𝑥 = 𝑠 ) ) )
65 58 64 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ( 𝑔 = ( 𝑥 ‘ 𝐹 ) ∧ 𝑥 = 𝑠 ) ) )
66 ancom ⊢ ( ( 𝑔 = ( 𝑥 ‘ 𝐹 ) ∧ 𝑥 = 𝑠 ) ↔ ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) )
67 65 66 bitrdi ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) )
68 67 rexbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) )
69 47 68 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) )
70 69 3anbi3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) ↔ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) ) )
71 fveq1 ⊢ ( 𝑥 = 𝑠 → ( 𝑥 ‘ 𝐹 ) = ( 𝑠 ‘ 𝐹 ) )
72 71 eqeq2d ⊢ ( 𝑥 = 𝑠 → ( 𝑔 = ( 𝑥 ‘ 𝐹 ) ↔ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
73 72 ceqsrexv ⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) → ( ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ↔ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
74 73 pm5.32i ⊢ ( ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) ↔ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
75 74 anbi2i ⊢ ( ( 𝑔 ∈ 𝑇 ∧ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) ) ↔ ( 𝑔 ∈ 𝑇 ∧ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) ) )
76 3anass ⊢ ( ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) ↔ ( 𝑔 ∈ 𝑇 ∧ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) ) )
77 3anass ⊢ ( ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) ↔ ( 𝑔 ∈ 𝑇 ∧ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) ) )
78 75 76 77 3bitr4i ⊢ ( ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑥 = 𝑠 ∧ 𝑔 = ( 𝑥 ‘ 𝐹 ) ) ) ↔ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
79 70 78 bitr2di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) ↔ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) ) )
80 42 79 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) ) )
81 eqeq1 ⊢ ( 𝑣 = ⟨ 𝑔 , 𝑠 ⟩ → ( 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) )
82 81 rexbidv ⊢ ( 𝑣 = ⟨ 𝑔 , 𝑠 ⟩ → ( ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) )
83 82 rabxp ⊢ { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } = { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) }
84 83 eleq2i ⊢ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } ↔ ⟨ 𝑔 , 𝑠 ⟩ ∈ { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) } )
85 opabidw ⊢ ( ⟨ 𝑔 , 𝑠 ⟩ ∈ { ⟨ 𝑔 , 𝑠 ⟩ ∣ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) } ↔ ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) )
86 84 85 bitr2i ⊢ ( ( 𝑔 ∈ 𝑇 ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ⟨ 𝑔 , 𝑠 ⟩ = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) ↔ ⟨ 𝑔 , 𝑠 ⟩ ∈ { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } )
87 80 86 bitrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑔 = ( 𝑠 ‘ 𝐹 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ⟨ 𝑔 , 𝑠 ⟩ ∈ { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } ) )
88 24 87 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑔 , 𝑠 ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ⟨ 𝑔 , 𝑠 ⟩ ∈ { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } ) )
89 88 eqrelrdv2 ⊢ ( ( ( Rel ( 𝐼 ‘ 𝑄 ) ∧ Rel { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } ) ∧ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐼 ‘ 𝑄 ) = { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } )
90 15 20 21 89 syl21anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } )
91 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
92 46 eleq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ↔ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
93 92 biimpa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
94 51 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
95 opelxpi ⊢ ( ( 𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
96 33 94 95 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
97 96 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
98 3 5 12 7 53 dvhvscacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
99 91 93 97 98 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
100 eleq1a ⊢ ( ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) → 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
101 99 100 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) ) → ( 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) → 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
102 101 rexlimdva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) → 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
103 102 pm4.71rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ↔ ( 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) ) )
104 103 abbidv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → { 𝑣 ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } = { 𝑣 ∣ ( 𝑣 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) ) } )
105 10 90 104 3eqtr4a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { 𝑣 ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } )
106 3 7 28 dvhlmod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑈 ∈ LMod )
107 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
108 3 5 12 7 107 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( Base ‘ 𝑈 ) )
109 28 33 94 108 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( Base ‘ 𝑈 ) )
110 43 44 107 53 8 lspsn ⊢ ( ( 𝑈 ∈ LMod ∧ ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( Base ‘ 𝑈 ) ) → ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) = { 𝑣 ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } )
111 106 109 110 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) = { 𝑣 ∣ ∃ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑣 = ( 𝑥 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ) } )
112 105 111 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) )