Metamath Proof Explorer

Theorem cdlemn4a

Description: Part of proof of Lemma N of Crawley p. 121 line 32. (Contributed by NM, 24-Feb-2014)

Ref Expression
Hypotheses cdlemn4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cdlemn4.l ⊢ ≤ = ( le ‘ 𝐾 )
cdlemn4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdlemn4.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
cdlemn4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdlemn4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemn4.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
cdlemn4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
cdlemn4.f ⊢ 𝐹 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑄 )
cdlemn4.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑅 )
cdlemn4.j ⊢ 𝐽 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑄 ) = 𝑅 )
cdlemn4a.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
cdlemn4a.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
Assertion cdlemn4a ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑁 ‘ { ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ } ) ⊆ ( ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) ⊕ ( 𝑁 ‘ { ⟨ 𝐽 , 𝑂 ⟩ } ) ) )

Proof

Step Hyp Ref Expression
1 cdlemn4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cdlemn4.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cdlemn4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemn4.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5 cdlemn4.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdlemn4.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 cdlemn4.o ⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
8 cdlemn4.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemn4.f ⊢ 𝐹 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑄 )
10 cdlemn4.g ⊢ 𝐺 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑃 ) = 𝑅 )
11 cdlemn4.j ⊢ 𝐽 = ( ℩ ℎ ∈ 𝑇 ( ℎ ‘ 𝑄 ) = 𝑅 )
12 cdlemn4a.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
13 cdlemn4a.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
14 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
15 1 2 3 4 5 6 7 8 9 10 11 14 cdlemn4 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ = ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ( +g ‘ 𝑈 ) ⟨ 𝐽 , 𝑂 ⟩ ) )
16 15 sneqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → { ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ } = { ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ( +g ‘ 𝑈 ) ⟨ 𝐽 , 𝑂 ⟩ ) } )
17 16 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑁 ‘ { ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ } ) = ( 𝑁 ‘ { ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ( +g ‘ 𝑈 ) ⟨ 𝐽 , 𝑂 ⟩ ) } ) )
18 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19 5 8 18 dvhlmod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝑈 ∈ LMod )
20 2 3 5 4 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
21 20 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
22 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
23 2 3 5 6 9 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
24 18 21 22 23 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
25 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
26 5 6 25 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
27 26 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
28 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
29 5 6 25 8 28 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( Base ‘ 𝑈 ) )
30 18 24 27 29 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( Base ‘ 𝑈 ) )
31 2 3 5 6 11 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝐽 ∈ 𝑇 )
32 1 5 6 25 7 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
33 32 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
34 5 6 25 8 28 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐽 ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ 𝐽 , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) )
35 18 31 33 34 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ⟨ 𝐽 , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) )
36 28 14 12 13 lspsntri ⊢ ( ( 𝑈 ∈ LMod ∧ ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ∈ ( Base ‘ 𝑈 ) ∧ ⟨ 𝐽 , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) ) → ( 𝑁 ‘ { ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ( +g ‘ 𝑈 ) ⟨ 𝐽 , 𝑂 ⟩ ) } ) ⊆ ( ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) ⊕ ( 𝑁 ‘ { ⟨ 𝐽 , 𝑂 ⟩ } ) ) )
37 19 30 35 36 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑁 ‘ { ( ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ ( +g ‘ 𝑈 ) ⟨ 𝐽 , 𝑂 ⟩ ) } ) ⊆ ( ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) ⊕ ( 𝑁 ‘ { ⟨ 𝐽 , 𝑂 ⟩ } ) ) )
38 17 37 eqsstrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑁 ‘ { ⟨ 𝐺 , ( I ↾ 𝑇 ) ⟩ } ) ⊆ ( ( 𝑁 ‘ { ⟨ 𝐹 , ( I ↾ 𝑇 ) ⟩ } ) ⊕ ( 𝑁 ‘ { ⟨ 𝐽 , 𝑂 ⟩ } ) ) )