Theorem tendoeq2 41242

Description: Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 41292, we show that we only need to consider a single non-identity translation. (Contributed by NM, 21-Jun-2013.)

Hypotheses

Ref	Expression
tendoeq2.b	⊢ 𝐵 = (Base‘𝐾)
tendoeq2.h	⊢ 𝐻 = (LHyp‘𝐾)
tendoeq2.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
tendoeq2.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)

Assertion

Ref	Expression
tendoeq2	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) → 𝑈 = 𝑉)

Distinct variable groups:   𝑓,𝐸   𝑓,𝐻   𝑓,𝐾   𝑇,𝑓   𝑓,𝑊   𝑈,𝑓   𝑓,𝑉

Allowed substitution hint:   𝐵(𝑓)

Proof of Theorem tendoeq2

Step	Hyp	Ref	Expression
1		tendoeq2.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐾)
2		tendoeq2.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
3		tendoeq2.e	. . . . . . . 8 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
4	1, 2, 3	tendoid 41241	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸) → (𝑈‘( I ↾ 𝐵)) = ( I ↾ 𝐵))
5	4	adantrr 718	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈‘( I ↾ 𝐵)) = ( I ↾ 𝐵))
6	1, 2, 3	tendoid 41241	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑉 ∈ 𝐸) → (𝑉‘( I ↾ 𝐵)) = ( I ↾ 𝐵))
7	6	adantrl 717	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑉‘( I ↾ 𝐵)) = ( I ↾ 𝐵))
8	5, 7	eqtr4d 2775	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑈‘( I ↾ 𝐵)) = (𝑉‘( I ↾ 𝐵)))
9		fveq2 6838	. . . . . 6 ⊢ (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑈‘( I ↾ 𝐵)))
10		fveq2 6838	. . . . . 6 ⊢ (𝑓 = ( I ↾ 𝐵) → (𝑉‘𝑓) = (𝑉‘( I ↾ 𝐵)))
11	9, 10	eqeq12d 2753	. . . . 5 ⊢ (𝑓 = ( I ↾ 𝐵) → ((𝑈‘𝑓) = (𝑉‘𝑓) ↔ (𝑈‘( I ↾ 𝐵)) = (𝑉‘( I ↾ 𝐵))))
12	8, 11	syl5ibrcom 247	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)))
13	12	ralrimivw 3134	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ∀𝑓 ∈ 𝑇 (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)))
14		r19.26 3098	. . . . 5 ⊢ (∀𝑓 ∈ 𝑇 ((𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) ↔ (∀𝑓 ∈ 𝑇 (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))))
15		jaob 964	. . . . . . 7 ⊢ (((𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) → (𝑈‘𝑓) = (𝑉‘𝑓)) ↔ ((𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))))
16		exmidne 2943	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵))
17		pm5.5 361	. . . . . . . 8 ⊢ ((𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) → (((𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) → (𝑈‘𝑓) = (𝑉‘𝑓)) ↔ (𝑈‘𝑓) = (𝑉‘𝑓)))
18	16, 17	ax-mp 5	. . . . . . 7 ⊢ (((𝑓 = ( I ↾ 𝐵) ∨ 𝑓 ≠ ( I ↾ 𝐵)) → (𝑈‘𝑓) = (𝑉‘𝑓)) ↔ (𝑈‘𝑓) = (𝑉‘𝑓))
19	15, 18	bitr3i 277	. . . . . 6 ⊢ (((𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) ↔ (𝑈‘𝑓) = (𝑉‘𝑓))
20	19	ralbii 3084	. . . . 5 ⊢ (∀𝑓 ∈ 𝑇 ((𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) ↔ ∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓))
21	14, 20	bitr3i 277	. . . 4 ⊢ ((∀𝑓 ∈ 𝑇 (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) ↔ ∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓))
22		tendoeq2.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
23	2, 22, 3	tendoeq1 41232	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓)) → 𝑈 = 𝑉)
24	23	3expia 1122	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (∀𝑓 ∈ 𝑇 (𝑈‘𝑓) = (𝑉‘𝑓) → 𝑈 = 𝑉))
25	21, 24	biimtrid 242	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → ((∀𝑓 ∈ 𝑇 (𝑓 = ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) → 𝑈 = 𝑉))
26	13, 25	mpand 696	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸)) → (∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓)) → 𝑈 = 𝑉))
27	26	3impia 1118	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ∀𝑓 ∈ 𝑇 (𝑓 ≠ ( I ↾ 𝐵) → (𝑈‘𝑓) = (𝑉‘𝑓))) → 𝑈 = 𝑉)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052   I cid 5522   ↾ cres 5630  ‘cfv 6496  Basecbs 17176  HLchlt 39818  LHypclh 40452  LTrncltrn 40569  TEndoctendo 41220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-map 8772  df-proset 18257  df-poset 18276  df-plt 18291  df-lub 18307  df-glb 18308  df-join 18309  df-meet 18310  df-p0 18386  df-p1 18387  df-lat 18395  df-clat 18462  df-oposet 39644  df-ol 39646  df-oml 39647  df-covers 39734  df-ats 39735  df-atl 39766  df-cvlat 39790  df-hlat 39819  df-lhyp 40456  df-laut 40457  df-ldil 40572  df-ltrn 40573  df-trl 40627  df-tendo 41223

This theorem is referenced by:  tendocan  41292