dicvaddcl

Description: Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014)

	Ref	Expression
Hypotheses	dicvaddcl.l	⊢ ≤ = ( le ‘ 𝐾 )
	dicvaddcl.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dicvaddcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dicvaddcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dicvaddcl.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
	dicvaddcl.p	⊢ + = ( +_g ‘ 𝑈 )
Assertion	dicvaddcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝐼 ‘ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		dicvaddcl.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dicvaddcl.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		dicvaddcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dicvaddcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		dicvaddcl.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
6		dicvaddcl.p	⊢ + = ( +_g ‘ 𝑈 )
7		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
9	1 2 3 5 4 8	dicssdvh	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) ⊆ ( Base ‘ 𝑈 ) )
10		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
11		eqid	⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
12	3 10 11 4 8	dvhvbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
13	12	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ 𝑈 ) )
14	13	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ 𝑈 ) )
15	9 14	sseqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
16	15	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝐼 ‘ 𝑄 ) ⊆ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
17		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) )
18	16 17	sseldd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → 𝑋 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
19		simp3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) )
20	16 19	sseldd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → 𝑌 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
21		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
22		eqid	⊢ ( +_g ‘ ( Scalar ‘ 𝑈 ) ) = ( +_g ‘ ( Scalar ‘ 𝑈 ) )
23	3 10 11 4 21 6 22	dvhvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ 𝑌 ∈ ( ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( 𝑋 + 𝑌 ) = ⟨ ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) , ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ⟩ )
24	7 18 20 23	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 + 𝑌 ) = ⟨ ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) , ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ⟩ )
25	1 2 3 11 5	dicelval2nd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 2^nd ‘ 𝑋 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
26	25	3adant3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 2^nd ‘ 𝑋 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
27	1 2 3 11 5	dicelval2nd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 2^nd ‘ 𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
28	27	3adant3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 2^nd ‘ 𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
29		eqid	⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
30	1 29 2 3	lhpocnel	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) )
31	30	3ad2ant1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) )
32		simp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
33		eqid	⊢ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) = ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 )
34	1 2 3 10 33	ltrniotacl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ 𝐴 ∧ ¬ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
35	7 31 32 34	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
36		eqid	⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) )
37	10 36	tendospdi2	⊢ ( ( ( 2^nd ‘ 𝑋 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 2^nd ‘ 𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( 2^nd ‘ 𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( ( ( 2^nd ‘ 𝑋 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∘ ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
38	26 28 35 37	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( ( 2^nd ‘ 𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( ( ( 2^nd ‘ 𝑋 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∘ ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
39	3 10 11 4 21 36 22	dvhfplusr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +_g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) )
40	39	3ad2ant1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( +_g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) )
41	40	oveqd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) = ( ( 2^nd ‘ 𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( 2^nd ‘ 𝑌 ) ) )
42	41	fveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) = ( ( ( 2^nd ‘ 𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
43		eqid	⊢ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
44	1 2 3 43 10 5	dicelval1sta	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 1^st ‘ 𝑋 ) = ( ( 2^nd ‘ 𝑋 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
45	44	3adant3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 1^st ‘ 𝑋 ) = ( ( 2^nd ‘ 𝑋 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
46	1 2 3 43 10 5	dicelval1sta	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) → ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
47	46	3adant3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 1^st ‘ 𝑌 ) = ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
48	45 47	coeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) = ( ( ( 2^nd ‘ 𝑋 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∘ ( ( 2^nd ‘ 𝑌 ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ) )
49	38 42 48	3eqtr4rd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) = ( ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) )
50	3 10 11 36	tendoplcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 2^nd ‘ 𝑌 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 2^nd ‘ 𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( 2^nd ‘ 𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
51	7 26 28 50	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( 2^nd ‘ 𝑋 ) ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ( 𝑠 ‘ ℎ ) ∘ ( 𝑡 ‘ ℎ ) ) ) ) ( 2^nd ‘ 𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
52	41 51	eqeltrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
53		fvex	⊢ ( 1^st ‘ 𝑋 ) ∈ V
54		fvex	⊢ ( 1^st ‘ 𝑌 ) ∈ V
55	53 54	coex	⊢ ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) ∈ V
56		ovex	⊢ ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ∈ V
57	1 2 3 43 10 11 5 55 56	dicopelval	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) , ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) = ( ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∧ ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
58	57	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( ⟨ ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) , ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) ↔ ( ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) = ( ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ‘ ( ℩ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑔 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑄 ) ) ∧ ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
59	49 52 58	mpbir2and	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ⟨ ( ( 1^st ‘ 𝑋 ) ∘ ( 1^st ‘ 𝑌 ) ) , ( ( 2^nd ‘ 𝑋 ) ( +_g ‘ ( Scalar ‘ 𝑈 ) ) ( 2^nd ‘ 𝑌 ) ) ⟩ ∈ ( 𝐼 ‘ 𝑄 ) )
60	24 59	eqeltrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑋 ∈ ( 𝐼 ‘ 𝑄 ) ∧ 𝑌 ∈ ( 𝐼 ‘ 𝑄 ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝐼 ‘ 𝑄 ) )

Metamath Proof Explorer

Theorem dicvaddcl

Proof