Metamath Proof Explorer

Theorem tendoconid

Description: The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013)

Ref Expression
Hypotheses tendoid0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendoid0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoid0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion tendoconid ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) → ( 𝑈 ∘ 𝑉 ) ≠ 𝑂 )

Proof

Step Hyp Ref Expression
1 tendoid0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 tendoid0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 tendoid0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendoid0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 tendoid0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6 1 2 3 cdlemftr0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑔 ∈ 𝑇 𝑔 ≠ ( I ↾ 𝐵 ) )
7 6 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) → ∃ 𝑔 ∈ 𝑇 𝑔 ≠ ( I ↾ 𝐵 ) )
8 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑉 ∈ 𝐸 )
10 2 3 4 tendof ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ 𝐸 ) → 𝑉 : 𝑇 ⟶ 𝑇 )
11 8 9 10 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑉 : 𝑇 ⟶ 𝑇 )
12 simprl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑔 ∈ 𝑇 )
13 fvco3 ⊢ ( ( 𝑉 : 𝑇 ⟶ 𝑇 ∧ 𝑔 ∈ 𝑇 ) → ( ( 𝑈 ∘ 𝑉 ) ‘ 𝑔 ) = ( 𝑈 ‘ ( 𝑉 ‘ 𝑔 ) ) )
14 11 12 13 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈 ∘ 𝑉 ) ‘ 𝑔 ) = ( 𝑈 ‘ ( 𝑉 ‘ 𝑔 ) ) )
15 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑈 ≠ 𝑂 )
16 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑈 ∈ 𝐸 )
17 2 3 4 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇 ) → ( 𝑉 ‘ 𝑔 ) ∈ 𝑇 )
18 8 9 12 17 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑉 ‘ 𝑔 ) ∈ 𝑇 )
19 simpl3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → 𝑉 ≠ 𝑂 )
20 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) )
21 1 2 3 4 5 tendoid0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ 𝐸 ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑉 ‘ 𝑔 ) = ( I ↾ 𝐵 ) ↔ 𝑉 = 𝑂 ) )
22 8 9 20 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑉 ‘ 𝑔 ) = ( I ↾ 𝐵 ) ↔ 𝑉 = 𝑂 ) )
23 22 necon3bid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑉 ‘ 𝑔 ) ≠ ( I ↾ 𝐵 ) ↔ 𝑉 ≠ 𝑂 ) )
24 19 23 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑉 ‘ 𝑔 ) ≠ ( I ↾ 𝐵 ) )
25 1 2 3 4 5 tendoid0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ ( ( 𝑉 ‘ 𝑔 ) ∈ 𝑇 ∧ ( 𝑉 ‘ 𝑔 ) ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈 ‘ ( 𝑉 ‘ 𝑔 ) ) = ( I ↾ 𝐵 ) ↔ 𝑈 = 𝑂 ) )
26 8 16 18 24 25 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈 ‘ ( 𝑉 ‘ 𝑔 ) ) = ( I ↾ 𝐵 ) ↔ 𝑈 = 𝑂 ) )
27 26 necon3bid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈 ‘ ( 𝑉 ‘ 𝑔 ) ) ≠ ( I ↾ 𝐵 ) ↔ 𝑈 ≠ 𝑂 ) )
28 15 27 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑈 ‘ ( 𝑉 ‘ 𝑔 ) ) ≠ ( I ↾ 𝐵 ) )
29 14 28 eqnetrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈 ∘ 𝑉 ) ‘ 𝑔 ) ≠ ( I ↾ 𝐵 ) )
30 2 4 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 ∘ 𝑉 ) ∈ 𝐸 )
31 8 16 9 30 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑈 ∘ 𝑉 ) ∈ 𝐸 )
32 1 2 3 4 5 tendoid0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∘ 𝑉 ) ∈ 𝐸 ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( ( 𝑈 ∘ 𝑉 ) ‘ 𝑔 ) = ( I ↾ 𝐵 ) ↔ ( 𝑈 ∘ 𝑉 ) = 𝑂 ) )
33 8 31 20 32 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( ( 𝑈 ∘ 𝑉 ) ‘ 𝑔 ) = ( I ↾ 𝐵 ) ↔ ( 𝑈 ∘ 𝑉 ) = 𝑂 ) )
34 33 necon3bid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( ( ( 𝑈 ∘ 𝑉 ) ‘ 𝑔 ) ≠ ( I ↾ 𝐵 ) ↔ ( 𝑈 ∘ 𝑉 ) ≠ 𝑂 ) )
35 29 34 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) ∧ ( 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑈 ∘ 𝑉 ) ≠ 𝑂 )
36 7 35 rexlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑈 ≠ 𝑂 ) ∧ ( 𝑉 ∈ 𝐸 ∧ 𝑉 ≠ 𝑂 ) ) → ( 𝑈 ∘ 𝑉 ) ≠ 𝑂 )