Theorem tendospcanN

Description: Cancellation law for trace-preserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	tendospcan.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	tendospcan.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	tendospcan.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	tendospcan.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	tendospcan.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion	tendospcanN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ↔ 𝐹 = 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		tendospcan.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		tendospcan.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		tendospcan.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		tendospcan.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5		tendospcan.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6	2 3 4	tendocnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐺 ) = ( 𝑆 ‘ ◡ 𝐺 ) )
7	6	3adant3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ◡ ( 𝑆 ‘ 𝐺 ) = ( 𝑆 ‘ ◡ 𝐺 ) )
8	7	coeq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐺 ) ) )
9		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		simp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝑆 ∈ 𝐸 )
11		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐹 ∈ 𝑇 )
12		simp3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐺 ∈ 𝑇 )
13	2 3	ltrncnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ◡ 𝐺 ∈ 𝑇 )
14	9 12 13	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ◡ 𝐺 ∈ 𝑇 )
15	2 3 4	tendospdi1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ ◡ 𝐺 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐺 ) ) )
16	9 10 11 14 15	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( ( 𝑆 ‘ 𝐹 ) ∘ ( 𝑆 ‘ ◡ 𝐺 ) ) )
17	8 16	eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) )
18	17	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) )
19	18	eqeq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( I ↾ 𝐵 ) ) )
20		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21		simpl2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → 𝑆 ∈ 𝐸 )
22		simpl3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → 𝐹 ∈ 𝑇 )
23	2 3 4	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 )
24	20 21 22 23	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 )
25		simpl3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → 𝐺 ∈ 𝑇 )
26	2 3 4	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 )
27	20 21 25 26	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 )
28	1 2 3	ltrncoidN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ) → ( ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) )
29	20 24 27 28	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( ( 𝑆 ‘ 𝐹 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) )
30	20 25 13	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ◡ 𝐺 ∈ 𝑇 )
31	2 3	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ◡ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ ◡ 𝐺 ) ∈ 𝑇 )
32	20 22 30 31	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝐹 ∘ ◡ 𝐺 ) ∈ 𝑇 )
33		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) )
34	1 2 3 4 5	tendoid0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( ( 𝐹 ∘ ◡ 𝐺 ) ∈ 𝑇 ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ 𝑆 = 𝑂 ) )
35	20 21 32 33 34	syl112anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑆 ‘ ( 𝐹 ∘ ◡ 𝐺 ) ) = ( I ↾ 𝐵 ) ↔ 𝑆 = 𝑂 ) )
36	19 29 35	3bitr3d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ↔ 𝑆 = 𝑂 ) )
37	36	biimpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → 𝑆 = 𝑂 ) )
38	37	impancom	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( ( 𝐹 ∘ ◡ 𝐺 ) ≠ ( I ↾ 𝐵 ) → 𝑆 = 𝑂 ) )
39	38	necon1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( 𝑆 ≠ 𝑂 → ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ) )
40		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
41		simpl3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → 𝐹 ∈ 𝑇 )
42		simpl3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → 𝐺 ∈ 𝑇 )
43	1 2 3	ltrncoidN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ↔ 𝐹 = 𝐺 ) )
44	40 41 42 43	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( ( 𝐹 ∘ ◡ 𝐺 ) = ( I ↾ 𝐵 ) ↔ 𝐹 = 𝐺 ) )
45	39 44	sylibd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) ∧ ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ) → ( 𝑆 ≠ 𝑂 → 𝐹 = 𝐺 ) )
46	45	3exp1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑆 ∈ 𝐸 → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → ( 𝑆 ≠ 𝑂 → 𝐹 = 𝐺 ) ) ) ) )
47	46	com24	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ∈ 𝐸 → ( 𝑆 ≠ 𝑂 → 𝐹 = 𝐺 ) ) ) ) )
48	47	imp5a	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → 𝐹 = 𝐺 ) ) ) )
49	48	com24	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → 𝐹 = 𝐺 ) ) ) )
50	49	3imp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) → 𝐹 = 𝐺 ) )
51		fveq2	⊢ ( 𝐹 = 𝐺 → ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) )
52	50 51	impbid1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑆 ‘ 𝐹 ) = ( 𝑆 ‘ 𝐺 ) ↔ 𝐹 = 𝐺 ) )