Step |
Hyp |
Ref |
Expression |
1 |
|
lindfmm.b |
|- B = ( Base ` S ) |
2 |
|
lindfmm.c |
|- C = ( Base ` T ) |
3 |
|
rellindf |
|- Rel LIndF |
4 |
3
|
brrelex1i |
|- ( F LIndF S -> F e. _V ) |
5 |
|
simp3 |
|- ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F : I --> B ) -> F : I --> B ) |
6 |
|
dmfex |
|- ( ( F e. _V /\ F : I --> B ) -> I e. _V ) |
7 |
4 5 6
|
syl2anr |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F : I --> B ) /\ F LIndF S ) -> I e. _V ) |
8 |
7
|
ex |
|- ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F : I --> B ) -> ( F LIndF S -> I e. _V ) ) |
9 |
3
|
brrelex1i |
|- ( ( G o. F ) LIndF T -> ( G o. F ) e. _V ) |
10 |
|
f1f |
|- ( G : B -1-1-> C -> G : B --> C ) |
11 |
|
fco |
|- ( ( G : B --> C /\ F : I --> B ) -> ( G o. F ) : I --> C ) |
12 |
10 11
|
sylan |
|- ( ( G : B -1-1-> C /\ F : I --> B ) -> ( G o. F ) : I --> C ) |
13 |
12
|
3adant1 |
|- ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F : I --> B ) -> ( G o. F ) : I --> C ) |
14 |
|
dmfex |
|- ( ( ( G o. F ) e. _V /\ ( G o. F ) : I --> C ) -> I e. _V ) |
15 |
9 13 14
|
syl2anr |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F : I --> B ) /\ ( G o. F ) LIndF T ) -> I e. _V ) |
16 |
15
|
ex |
|- ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F : I --> B ) -> ( ( G o. F ) LIndF T -> I e. _V ) ) |
17 |
|
eldifi |
|- ( k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) -> k e. ( Base ` ( Scalar ` S ) ) ) |
18 |
|
simpllr |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> G : B -1-1-> C ) |
19 |
|
lmhmlmod1 |
|- ( G e. ( S LMHom T ) -> S e. LMod ) |
20 |
19
|
ad3antrrr |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> S e. LMod ) |
21 |
|
simprr |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> k e. ( Base ` ( Scalar ` S ) ) ) |
22 |
|
simprl |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> F : I --> B ) |
23 |
|
simpl |
|- ( ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) -> x e. I ) |
24 |
|
ffvelrn |
|- ( ( F : I --> B /\ x e. I ) -> ( F ` x ) e. B ) |
25 |
22 23 24
|
syl2an |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( F ` x ) e. B ) |
26 |
|
eqid |
|- ( Scalar ` S ) = ( Scalar ` S ) |
27 |
|
eqid |
|- ( .s ` S ) = ( .s ` S ) |
28 |
|
eqid |
|- ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) ) |
29 |
1 26 27 28
|
lmodvscl |
|- ( ( S e. LMod /\ k e. ( Base ` ( Scalar ` S ) ) /\ ( F ` x ) e. B ) -> ( k ( .s ` S ) ( F ` x ) ) e. B ) |
30 |
20 21 25 29
|
syl3anc |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( k ( .s ` S ) ( F ` x ) ) e. B ) |
31 |
|
imassrn |
|- ( F " ( I \ { x } ) ) C_ ran F |
32 |
|
frn |
|- ( F : I --> B -> ran F C_ B ) |
33 |
32
|
adantr |
|- ( ( F : I --> B /\ I e. _V ) -> ran F C_ B ) |
34 |
31 33
|
sstrid |
|- ( ( F : I --> B /\ I e. _V ) -> ( F " ( I \ { x } ) ) C_ B ) |
35 |
34
|
ad2antlr |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( F " ( I \ { x } ) ) C_ B ) |
36 |
|
eqid |
|- ( LSpan ` S ) = ( LSpan ` S ) |
37 |
1 36
|
lspssv |
|- ( ( S e. LMod /\ ( F " ( I \ { x } ) ) C_ B ) -> ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) C_ B ) |
38 |
20 35 37
|
syl2anc |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) C_ B ) |
39 |
|
f1elima |
|- ( ( G : B -1-1-> C /\ ( k ( .s ` S ) ( F ` x ) ) e. B /\ ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) C_ B ) -> ( ( G ` ( k ( .s ` S ) ( F ` x ) ) ) e. ( G " ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) <-> ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) ) |
40 |
18 30 38 39
|
syl3anc |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( ( G ` ( k ( .s ` S ) ( F ` x ) ) ) e. ( G " ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) <-> ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) ) |
41 |
|
simplll |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> G e. ( S LMHom T ) ) |
42 |
|
eqid |
|- ( .s ` T ) = ( .s ` T ) |
43 |
26 28 1 27 42
|
lmhmlin |
|- ( ( G e. ( S LMHom T ) /\ k e. ( Base ` ( Scalar ` S ) ) /\ ( F ` x ) e. B ) -> ( G ` ( k ( .s ` S ) ( F ` x ) ) ) = ( k ( .s ` T ) ( G ` ( F ` x ) ) ) ) |
44 |
41 21 25 43
|
syl3anc |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( G ` ( k ( .s ` S ) ( F ` x ) ) ) = ( k ( .s ` T ) ( G ` ( F ` x ) ) ) ) |
45 |
|
ffn |
|- ( F : I --> B -> F Fn I ) |
46 |
45
|
ad2antrl |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> F Fn I ) |
47 |
|
fvco2 |
|- ( ( F Fn I /\ x e. I ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) ) |
48 |
46 23 47
|
syl2an |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) ) |
49 |
48
|
oveq2d |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( k ( .s ` T ) ( ( G o. F ) ` x ) ) = ( k ( .s ` T ) ( G ` ( F ` x ) ) ) ) |
50 |
44 49
|
eqtr4d |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( G ` ( k ( .s ` S ) ( F ` x ) ) ) = ( k ( .s ` T ) ( ( G o. F ) ` x ) ) ) |
51 |
|
eqid |
|- ( LSpan ` T ) = ( LSpan ` T ) |
52 |
1 36 51
|
lmhmlsp |
|- ( ( G e. ( S LMHom T ) /\ ( F " ( I \ { x } ) ) C_ B ) -> ( G " ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) = ( ( LSpan ` T ) ` ( G " ( F " ( I \ { x } ) ) ) ) ) |
53 |
41 35 52
|
syl2anc |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( G " ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) = ( ( LSpan ` T ) ` ( G " ( F " ( I \ { x } ) ) ) ) ) |
54 |
|
imaco |
|- ( ( G o. F ) " ( I \ { x } ) ) = ( G " ( F " ( I \ { x } ) ) ) |
55 |
54
|
fveq2i |
|- ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) = ( ( LSpan ` T ) ` ( G " ( F " ( I \ { x } ) ) ) ) |
56 |
53 55
|
eqtr4di |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( G " ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) = ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) |
57 |
50 56
|
eleq12d |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( ( G ` ( k ( .s ` S ) ( F ` x ) ) ) e. ( G " ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) <-> ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
58 |
40 57
|
bitr3d |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) <-> ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
59 |
58
|
notbid |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ ( x e. I /\ k e. ( Base ` ( Scalar ` S ) ) ) ) -> ( -. ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) <-> -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
60 |
59
|
anassrs |
|- ( ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ x e. I ) /\ k e. ( Base ` ( Scalar ` S ) ) ) -> ( -. ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) <-> -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
61 |
17 60
|
sylan2 |
|- ( ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ x e. I ) /\ k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) ) -> ( -. ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) <-> -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
62 |
61
|
ralbidva |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ x e. I ) -> ( A. k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) -. ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) <-> A. k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
63 |
|
eqid |
|- ( Scalar ` T ) = ( Scalar ` T ) |
64 |
26 63
|
lmhmsca |
|- ( G e. ( S LMHom T ) -> ( Scalar ` T ) = ( Scalar ` S ) ) |
65 |
64
|
fveq2d |
|- ( G e. ( S LMHom T ) -> ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` S ) ) ) |
66 |
64
|
fveq2d |
|- ( G e. ( S LMHom T ) -> ( 0g ` ( Scalar ` T ) ) = ( 0g ` ( Scalar ` S ) ) ) |
67 |
66
|
sneqd |
|- ( G e. ( S LMHom T ) -> { ( 0g ` ( Scalar ` T ) ) } = { ( 0g ` ( Scalar ` S ) ) } ) |
68 |
65 67
|
difeq12d |
|- ( G e. ( S LMHom T ) -> ( ( Base ` ( Scalar ` T ) ) \ { ( 0g ` ( Scalar ` T ) ) } ) = ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) ) |
69 |
68
|
ad3antrrr |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ x e. I ) -> ( ( Base ` ( Scalar ` T ) ) \ { ( 0g ` ( Scalar ` T ) ) } ) = ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) ) |
70 |
69
|
raleqdv |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ x e. I ) -> ( A. k e. ( ( Base ` ( Scalar ` T ) ) \ { ( 0g ` ( Scalar ` T ) ) } ) -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) <-> A. k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
71 |
62 70
|
bitr4d |
|- ( ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) /\ x e. I ) -> ( A. k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) -. ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) <-> A. k e. ( ( Base ` ( Scalar ` T ) ) \ { ( 0g ` ( Scalar ` T ) ) } ) -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
72 |
71
|
ralbidva |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> ( A. x e. I A. k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) -. ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) <-> A. x e. I A. k e. ( ( Base ` ( Scalar ` T ) ) \ { ( 0g ` ( Scalar ` T ) ) } ) -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
73 |
19
|
ad2antrr |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> S e. LMod ) |
74 |
|
simprr |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> I e. _V ) |
75 |
|
eqid |
|- ( 0g ` ( Scalar ` S ) ) = ( 0g ` ( Scalar ` S ) ) |
76 |
1 27 36 26 28 75
|
islindf2 |
|- ( ( S e. LMod /\ I e. _V /\ F : I --> B ) -> ( F LIndF S <-> A. x e. I A. k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) -. ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) ) |
77 |
73 74 22 76
|
syl3anc |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> ( F LIndF S <-> A. x e. I A. k e. ( ( Base ` ( Scalar ` S ) ) \ { ( 0g ` ( Scalar ` S ) ) } ) -. ( k ( .s ` S ) ( F ` x ) ) e. ( ( LSpan ` S ) ` ( F " ( I \ { x } ) ) ) ) ) |
78 |
|
lmhmlmod2 |
|- ( G e. ( S LMHom T ) -> T e. LMod ) |
79 |
78
|
ad2antrr |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> T e. LMod ) |
80 |
12
|
ad2ant2lr |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> ( G o. F ) : I --> C ) |
81 |
|
eqid |
|- ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) ) |
82 |
|
eqid |
|- ( 0g ` ( Scalar ` T ) ) = ( 0g ` ( Scalar ` T ) ) |
83 |
2 42 51 63 81 82
|
islindf2 |
|- ( ( T e. LMod /\ I e. _V /\ ( G o. F ) : I --> C ) -> ( ( G o. F ) LIndF T <-> A. x e. I A. k e. ( ( Base ` ( Scalar ` T ) ) \ { ( 0g ` ( Scalar ` T ) ) } ) -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
84 |
79 74 80 83
|
syl3anc |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> ( ( G o. F ) LIndF T <-> A. x e. I A. k e. ( ( Base ` ( Scalar ` T ) ) \ { ( 0g ` ( Scalar ` T ) ) } ) -. ( k ( .s ` T ) ( ( G o. F ) ` x ) ) e. ( ( LSpan ` T ) ` ( ( G o. F ) " ( I \ { x } ) ) ) ) ) |
85 |
72 77 84
|
3bitr4d |
|- ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) /\ ( F : I --> B /\ I e. _V ) ) -> ( F LIndF S <-> ( G o. F ) LIndF T ) ) |
86 |
85
|
exp32 |
|- ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C ) -> ( F : I --> B -> ( I e. _V -> ( F LIndF S <-> ( G o. F ) LIndF T ) ) ) ) |
87 |
86
|
3impia |
|- ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F : I --> B ) -> ( I e. _V -> ( F LIndF S <-> ( G o. F ) LIndF T ) ) ) |
88 |
8 16 87
|
pm5.21ndd |
|- ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F : I --> B ) -> ( F LIndF S <-> ( G o. F ) LIndF T ) ) |