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	$⊢ B = {Base}_{K}$
	tendoid0.h	$⊢ H = LHyp (K)$
	tendoid0.t	$⊢ T = LTrn (K) (W)$
	tendoid0.e	$⊢ E = TEndo (K) (W)$
	tendoid0.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
Assertion	tendoconid	$⊢ ((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \to U \circ V \neq O$

Proof

Step	Hyp	Ref	Expression
1		tendoid0.b	$⊢ B = {Base}_{K}$
2		tendoid0.h	$⊢ H = LHyp (K)$
3		tendoid0.t	$⊢ T = LTrn (K) (W)$
4		tendoid0.e	$⊢ E = TEndo (K) (W)$
5		tendoid0.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
6	1 2 3	cdlemftr0	$⊢ (K \in HL \land W \in H) \to \exists g \in T g \neq {I ↾}_{B}$
7	6	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \to \exists g \in T g \neq {I ↾}_{B}$
8		simpl1	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to (K \in HL \land W \in H)$
9		simpl3l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to V \in E$
10	2 3 4	tendof	$⊢ ((K \in HL \land W \in H) \land V \in E) \to V : T ⟶ T$
11	8 9 10	syl2anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to V : T ⟶ T$
12		simprl	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to g \in T$
13		fvco3	$⊢ (V : T ⟶ T \land g \in T) \to (U \circ V) (g) = U (V (g))$
14	11 12 13	syl2anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to (U \circ V) (g) = U (V (g))$
15		simpl2r	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to U \neq O$
16		simpl2l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to U \in E$
17	2 3 4	tendocl	$⊢ ((K \in HL \land W \in H) \land V \in E \land g \in T) \to V (g) \in T$
18	8 9 12 17	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to V (g) \in T$
19		simpl3r	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to V \neq O$
20		simpr	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to (g \in T \land g \neq {I ↾}_{B})$
21	1 2 3 4 5	tendoid0	$⊢ ((K \in HL \land W \in H) \land V \in E \land (g \in T \land g \neq {I ↾}_{B})) \to (V (g) = {I ↾}_{B} \leftrightarrow V = O)$
22	8 9 20 21	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to (V (g) = {I ↾}_{B} \leftrightarrow V = O)$
23	22	necon3bid	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to (V (g) \neq {I ↾}_{B} \leftrightarrow V \neq O)$
24	19 23	mpbird	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to V (g) \neq {I ↾}_{B}$
25	1 2 3 4 5	tendoid0	$⊢ ((K \in HL \land W \in H) \land U \in E \land (V (g) \in T \land V (g) \neq {I ↾}_{B})) \to (U (V (g)) = {I ↾}_{B} \leftrightarrow U = O)$
26	8 16 18 24 25	syl112anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to (U (V (g)) = {I ↾}_{B} \leftrightarrow U = O)$
27	26	necon3bid	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to (U (V (g)) \neq {I ↾}_{B} \leftrightarrow U \neq O)$
28	15 27	mpbird	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to U (V (g)) \neq {I ↾}_{B}$
29	14 28	eqnetrd	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to (U \circ V) (g) \neq {I ↾}_{B}$
30	2 4	tendococl	$⊢ ((K \in HL \land W \in H) \land U \in E \land V \in E) \to U \circ V \in E$
31	8 16 9 30	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to U \circ V \in E$
32	1 2 3 4 5	tendoid0	$⊢ ((K \in HL \land W \in H) \land U \circ V \in E \land (g \in T \land g \neq {I ↾}_{B})) \to ((U \circ V) (g) = {I ↾}_{B} \leftrightarrow U \circ V = O)$
33	8 31 20 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to ((U \circ V) (g) = {I ↾}_{B} \leftrightarrow U \circ V = O)$
34	33	necon3bid	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to ((U \circ V) (g) \neq {I ↾}_{B} \leftrightarrow U \circ V \neq O)$
35	29 34	mpbid	$⊢ (((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \land (g \in T \land g \neq {I ↾}_{B})) \to U \circ V \neq O$
36	7 35	rexlimddv	$⊢ ((K \in HL \land W \in H) \land (U \in E \land U \neq O) \land (V \in E \land V \neq O)) \to U \circ V \neq O$

Metamath Proof Explorer

Theorem tendoconid

Proof