Metamath Proof Explorer

Theorem lcfrlem40

Description: Lemma for lcfr . Eliminate B and I . (Contributed by NM, 11-Mar-2015)

Ref Expression
Hypotheses lcfrlem38.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
lcfrlem38.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem38.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem38.p ⊢ + = ( +g ‘ 𝑈 )
lcfrlem38.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
lcfrlem38.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
lcfrlem38.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
lcfrlem38.q ⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
lcfrlem38.c ⊢ 𝐶 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
lcfrlem38.e ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
lcfrlem38.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
lcfrlem38.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
lcfrlem38.gs ⊢ ( 𝜑 → 𝐺 ⊆ 𝐶 )
lcfrlem38.xe ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
lcfrlem38.ye ⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
lcfrlem38.z ⊢ 0 = ( 0g ‘ 𝑈 )
lcfrlem38.x ⊢ ( 𝜑 → 𝑋 ≠ 0 )
lcfrlem38.y ⊢ ( 𝜑 → 𝑌 ≠ 0 )
lcfrlem38.sp ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
lcfrlem38.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
Assertion lcfrlem40 ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 lcfrlem38.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfrlem38.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfrlem38.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfrlem38.p ⊢ + = ( +g ‘ 𝑈 )
5 lcfrlem38.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6 lcfrlem38.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
7 lcfrlem38.d ⊢ 𝐷 = ( LDual ‘ 𝑈 )
8 lcfrlem38.q ⊢ 𝑄 = ( LSubSp ‘ 𝐷 )
9 lcfrlem38.c ⊢ 𝐶 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
10 lcfrlem38.e ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
11 lcfrlem38.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 lcfrlem38.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑄 )
13 lcfrlem38.gs ⊢ ( 𝜑 → 𝐺 ⊆ 𝐶 )
14 lcfrlem38.xe ⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
15 lcfrlem38.ye ⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
16 lcfrlem38.z ⊢ 0 = ( 0g ‘ 𝑈 )
17 lcfrlem38.x ⊢ ( 𝜑 → 𝑋 ≠ 0 )
18 lcfrlem38.y ⊢ ( 𝜑 → 𝑌 ≠ 0 )
19 lcfrlem38.sp ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
20 lcfrlem38.ne ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
21 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
22 1 3 11 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
23 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
24 1 2 3 23 6 7 8 10 11 12 14 lcfrlem4 ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑈 ) )
25 eldifsn ⊢ ( 𝑋 ∈ ( ( Base ‘ 𝑈 ) ∖ { 0 } ) ↔ ( 𝑋 ∈ ( Base ‘ 𝑈 ) ∧ 𝑋 ≠ 0 ) )
26 24 17 25 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝑈 ) ∖ { 0 } ) )
27 1 2 3 23 6 7 8 10 11 12 15 lcfrlem4 ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑈 ) )
28 eldifsn ⊢ ( 𝑌 ∈ ( ( Base ‘ 𝑈 ) ∖ { 0 } ) ↔ ( 𝑌 ∈ ( Base ‘ 𝑈 ) ∧ 𝑌 ≠ 0 ) )
29 27 18 28 sylanbrc ⊢ ( 𝜑 → 𝑌 ∈ ( ( Base ‘ 𝑈 ) ∖ { 0 } ) )
30 1 2 3 23 4 16 19 21 11 26 29 20 lcfrlem21 ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
31 16 21 22 30 lsateln0 ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) 𝑖 ≠ 0 )
32 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → 𝐺 ∈ 𝑄 )
34 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → 𝐺 ⊆ 𝐶 )
35 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → 𝑋 ∈ 𝐸 )
36 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → 𝑌 ∈ 𝐸 )
37 17 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → 𝑋 ≠ 0 )
38 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → 𝑌 ≠ 0 )
39 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
40 eqid ⊢ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) )
41 simp2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) )
42 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → 𝑖 ≠ 0 )
43 1 2 3 4 5 6 7 8 9 10 32 33 34 35 36 16 37 38 19 39 40 41 42 lcfrlem39 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ 𝑖 ≠ 0 ) → ( 𝑋 + 𝑌 ) ∈ 𝐸 )
44 43 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ⊥ ‘ { ( 𝑋 + 𝑌 ) } ) ) 𝑖 ≠ 0 → ( 𝑋 + 𝑌 ) ∈ 𝐸 ) )
45 31 44 mpd ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐸 )